Risoluzione (logica)

In logica matematica e dimostrazione automatica di teoremi, la risoluzione è una regola d'inferenza che porta a una tecnica di dimostrazione completa per refutazione per enunciati in logica proposizionale e logica del primo ordine. Nella logica proposizionale, l'applicazione sistematica della regola di risoluzione costituisce una procedura di decisione per l'insoddisfacibilità, il che risolve il (complemento del) problema di soddisfacibilità booleana. Nella logica del primo ordine, si può usare la risoluzione come base per un algoritmo parziale per il problema di insoddisfacibilità della logica del primo ordine, il che fornisce un metodo più pratico rispetto ad uno che segua dal teorema di completezza di Gödel.

La regola di risoluzione può essere ricondotta al lavoro di Davis e Putnam (1960); tuttavia, il loro algoritmo richiedeva di provare tutte le istanze ground della formula data. Questa fonte di esplosione combinatoria è stata eliminata nel 1965 dall'algoritmo di unificazione sintattica^[1], dovuto a John A. Robinson, il quale permette di istanziare la formula nel corso della dimostrazione ove richiesto al fine di preservare la completezza per refutazione.

Una forma di risoluzione su clausole di Horn del primo ordine è alla base del funzionamento degli interpreti del linguaggio di programmazione Prolog.

La regola di risoluzione in logica proposizionale è una regola d'inferenza valida che produce una nuova clausola, i.e. una disgiunzione di letterali, implicata da due clausole che contengono letterali complementari. Un letterale è costituito da una variabile proposizionale ${\displaystyle a}$ o la sua negazione ${\displaystyle \neg a}$. Due letterali sono detti complementari se uno è la negazione dell'altro (come ${\displaystyle \lnot a}$ per ${\displaystyle a}$ e viceversa). La clausola risultante detta risolvente contiene tutti i letterali che non abbiano complementari. Formalmente:

${\displaystyle {\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}}$

dove tutti gli ${\displaystyle a_{i}}$, ${\displaystyle b_{i}}$, e ${\displaystyle c}$ sono letterali e la riga separa le premesse dalle conseguenze.

La regola può essere scritta anche come segue:

${\displaystyle {\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}}$

La clausola prodotta dalla regola di risoluzione si chiama risolvente delle due clausole in premessa.

Quando le clausole in premessa contengono più letterali complementari, si può applicare la regola di risoluzione a ogni coppia in modo indipendente; il risultato è sempre una tautologia.

La regola del modus ponens può essere considerata un caso speciale di risoluzione (di una clausola con un solo letterale e una con due letterali). Infatti:

${\displaystyle {\frac {p\rightarrow q,\quad p}{q}}}$

è equivalente a

${\displaystyle {\frac {\lnot p\lor q,\quad p}{q}}}$

Nel caso delle clausole del primo ordine, rappresentando equivalentemente le disgiunzioni di letterali del primo ordine come insiemi di atomi o loro negazioni, la regola di risoluzione può essere definita come segue:

${\displaystyle {\frac {\Gamma _{1}\cup \left\{L_{1}\right\}\,\,\,\,\Gamma _{2}\cup \left\{L_{2}\right\}}{(\Gamma _{1}\cup \Gamma _{2})\mu }}\mu }$

dove le premesse sono clausole che non hanno variabili comuni e ${\displaystyle \mu }$ è un unificatore più generale dei letterali complementari ${\displaystyle L_{1}=\neg A_{1}}$ e ${\displaystyle L_{2}=A_{2}}$, i.e. una sostituzione (di variabili con termini) tale che ${\displaystyle A_{1}\mu =A_{2}\mu }$.

Applicando la regola alle clausole ${\textstyle \{P(x),Q(x)\}}$ e ${\textstyle \{R(b,y),\neg P(b)\}}$ con l'unificatore ${\textstyle [b/x]}$ (dove ${\textstyle x}$ e ${\textstyle y}$ sono variabili e ${\textstyle b}$ è una costante):

${\displaystyle {\frac {\{P(x),Q(x)\}\quad \{R(b,y),\neg P(b)\}}{\{Q(b),R(b,y)\}}}[b/x]}$

nomenclatura:

• le clausole ${\textstyle \{P(x),Q(x)\}}$ e ${\textstyle \{R(b,y),\neg P(b)\}}$ sono le premesse dell'inferenza
• ${\displaystyle \{Q(b),R(b,y)\}}$, clausola risolvente delle premesse, è la conclusione
• si risolve sul predicato ${\displaystyle P}$ detto pivot
• ${\displaystyle P(x)}$ è il letterale risolto a sinistra, ${\displaystyle \neg P(b)}$ è il letterale risolto a destra
• ${\displaystyle [b/x]}$ è un unificatore più generale dei letterali risolti

In logica del primo ordine, la risoluzione riassume in un'unica regola i sillogismi classici dell'inferenza logica.

Si consideri il seguente esempio:

Tutti i greci sono europei.

Omero è un greco.

Quindi Omero è un europeo.

In formule generali:

${\displaystyle \forall x.P(x)\Rightarrow Q(x)}$

${\displaystyle P(a)}$

pertanto, ${\displaystyle Q(a)}$

Sono state proposte diverse generalizzazioni della regola sopra descritta in cui non si richiede che le premesse siano in forma di clausola.^[2][3][4][5]

1. ^ Robinson, J. Alan, A Machine-Oriented Logic Based on the Resolution Principle, in Journal of the ACM, vol. 12, n. 1, ACM, pp. 23–41, DOI:10.1145/321250.321253, S2CID: 14389185.
2. ^ Wilkins, D, QUEST: A Non-Clausal Theorem Proving System (Master's Thesis), University of Essex, 1973.
3. ^ Manna, Zohar and Waldinger, Richard, A Deductive Approach to Program Synthesis, in ACM Transactions on Programming Languages and Systems, vol. 2, Jan. 1980, pp. 90–121, DOI:10.1145/357084.357090.
4. ^ Murray, Neil V., A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic, in Technical report: Electrical Engineering and Computer Science, Syracuse University, vol. 39, feb. 1973.
5. ^ N.V. Murray, Completely Non-Clausal Theorem Proving, in Artificial Intelligence, vol. 18, 1982, pp. 67–85, DOI:10.1016/0004-3702(82)90011-x.

• Inferenza
• Modus ponens
• Programmazione logica
• Prolog

• (EN) resolution, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
• (EN) Eric W. Weisstein, Resolution Principle, su MathWorld, Wolfram Research.