Sistemi deduttivi

Note

La finalità di un sistema deduttivo, o un metodo formale, è di avere un metodo automatico per verificare che $\Gamma \models A$. Quindi partendo dall’insieme $\Gamma$ e da un insieme di assiomi $\text{Ax}$, con delle regole di riscrittura, dette di inferenza, cerchiamo di generare una sequenza di FBF tale che:

$$\Gamma \cup \text{Ax}⊢D_0\Gamma \cup \text{Ax}\cup \{D_0\}⊢D_1\cdots \Gamma \cup \text{Ax}\cup \{D_0,\cdots ,D_{n-1}\}⊢A$$

I sistemi formali possono essere:

• Corretti: $\Gamma ⊢A\Rightarrow \Gamma \models A$
• Completi: $\Gamma \models A\Rightarrow \Gamma ⊢A$

Teoria L

Note

Ha come sintassi una FBF contenenti solo $\neg$ e $\Rightarrow$. Gli assiomi sono:

$$\text{Ax}:\{\begin{array}{ll}{A}_1:& A\Rightarrow (B\Rightarrow A)\\ A_2:& (A\Rightarrow (B\Rightarrow C))\Rightarrow ((A\Rightarrow B)\Rightarrow (A\Rightarrow C))\\ A_3:& (\neg A\Rightarrow \neg B)\Rightarrow ((\neg A\Rightarrow B)\Rightarrow A)\end{array}$$

Questi in realtà sono schemi di assiomi poiché $A,B,C$ sono FBF. Inoltre consideriamo come regola d’inferenza la “modus ponens”:

$$A,A\Rightarrow B{⊢}_{L}B$$

Quindi se da un insieme di formula $\Gamma$, usando gli assiomi $\text{Ax}$ e il modus ponens ottengo una sequenza di FBF $D_1,\cdots ,D_n$ tale che:

$$\Gamma \cup \text{Ax}{⊢}_L{D}_0\Gamma \cup \text{Ax}\cup \{D_0\}{⊢}_L{D}_1\cdots \Gamma \cup \text{Ax}\cup \{D_0,\cdots ,D_{n-1}\}{⊢}_L{D}_n$$

Allora si dice che $D_n$ è un teorema della teoria L che ha $x$ premesse $\Gamma$ e $D_1,\cdots ,D_n$ è una dimostrazione di $D_n$, e scriviamo $\Gamma {⊢}_L{D}_n$

Teorema di correttezza e completezza forte

La teoria L è:

• Corretta: $\Gamma {⊢}_{L}A\Rightarrow \Gamma \models A$
• Completa: $\Gamma \models A\Rightarrow \Gamma {⊢}_{L}A$

Nel caso $\Gamma =\varnothing$, il teorema si riduce a ${⊢}_{L}A\iff \models A$, cioè $A$ è una tautologia.

Risoluzione

Note

A differenza della teoria L, non ha assiomi propri e funziona per refutazione. La risoluzione verifica se un insieme $\Lambda$ di formule è insoddisfacibile. Quindi:

$$\Lambda \text{ eˋ insoddisfacibile se }{\Lambda }^C{⊢}_R\square$$

Definiamo:

• Letterale: una lettera enunciativa o una sua negata ($A$ o $\neg A$)
• Clausola: È un insieme di letterali, anche dette stringhe privilegiate. La clausola vuota è indicata come $\square$, mentre l’insieme di clausole di $\Lambda$ è ${\Lambda }^C$
• Regola d’inferenza: diciamo che la clausola $R$ è una risolvente delle clausole $C_1,C_2$ e scriviamo $C_1,C_2{⊢}_{R}R$ se:

$$A\in C_1\neg A\in C_{2}R=(C_1\setminus \{A\})\cup (C_2\setminus \{\neg A\})$$

Warning

La regola di inferenza si applica per un letterale e il suo negato alla volta.

Sia ${\Lambda }^C$ l’insieme di clausole, una derivazione per risoluzione della clausola $C$ da ${\Lambda }^C$ è una sequenza di clausole $D_1,\cdots ,D_n$ tale che $D_n=C$ e:

$${\Lambda }^C{⊢}_R{D}_1{\Lambda }^C\cup \{D_1\}{⊢}_R{D}_2\cdots {\Lambda }^C\cup \{D_1,\cdots ,D_{n-1}\}{⊢}_R=D_n$$

Tip

Le clausole, in generale, si possono utilizzare più di una volta.