Inferenza per risoluzione

L'inferenza per risoluzione è una regola di inferenza logica basata sull'applicazione del metodo della risoluzione. La regola di inferenza consente di comprendere se una proposizione consegue logicamente da un'altra o da altre proposizioni logiche. Un algoritmo di inferenza per risoluzione elabora tutte le proposizioni come clausole. Le clausole sono confrontate l'una con l'altra, unendo le clausole che hanno letterali opposti al loro interno, fin quando non viene a determinarsi una clausola vuota oppure fin quando tutte le clausole sono state elaborate. Quando si verifica il caso di una clausola vuota, l'insieme delle clausole è insoddisfacibile e la conseguenza logica è valida. La procedura di inferenza per risoluzione si basa sul principio della dimostrazione per assurdo. Per dimostrare una determinata conseguenza logica ( A B ), il metodo della risoluzione dimostra che l'insieme ( A ∧ ¬B ) è insoddisfacibile. Ad esempio, date tre proposizioni ( A∨¬B∨C ), ( ¬A∨B ) e (C), l'algoritmo deve determinare se la proposizione (C) consegue logicamente da ( A∨¬B∨C ), ( ¬A∨B ).

Il primo passo dell'algoritmo di inferenza consiste nella trasformazione delle formule in un problema di soddisfacibilità. L'ultima formula viene trasformata in un una clausola e aggiunta alle altre. Come si può notare, la proposizione C viene aggiunta nella sua forma opposta/complementare ( ¬C ), ciò consente di dimostrare l'esistenza o meno dell'inverso rispetto a quanto si vuole provare. Nell'esempio, due proposizioni hanno letterali complementari al loro interno, l'algoritmo le mette a confronto ottenendo una nuova clausola ( C ) , detta clausola risolvente, che a sua volta viene aggiunta all'insieme delle clausole. La nuova clausola è particolarmente utile poiché l'algoritmo può porre il confronto tra la clausola appena trovata ( C ) e l'altra clausola ( ¬C ). Essendo due clausole complementari, l'algoritmo restituisce una clausola vuota terminando l'esecuzione. Durante il ciclo di elaborazione l'algoritmo ha dimostrato così l'insoddisfacibilità dell'insieme { A∨¬B∨C , ¬A∨B , ¬C } e, pertanto, la validità della conseguenza logica ( A∨¬B∨C ), ( ¬A∨B ) C. Per ulteriore approfondimento sul funzionamento dell'algoritmo si rimanda alla lettera del metodo della risoluzione.