Risoluzione logica

Note

Troviamo le clausole di una FBF $F$:

• Se $F$ non è chiusa, chiuderla universalmente.
• Portare $F$ in forma di Skolem $F_{\text{SK}}$.
• Portare la matrice di $F_{\text{SK}}$ in FNC.
• Rinomino le variabili tar clausole in modo distinto, per avere il massimo grado di libertà per trovare $\square$.

Per risolvere due clausole utilizziamo la sostituzione.

Sostituzione

Note

Una sostituzione $\sigma$ è una scrittura:

$$\sigma =\{t_1/x_1,\cdots ,t_n/x_n\}$$

Dove $x_1,\cdots ,x_n$ sono variabili distinte, mentre $t_1,\cdots ,t_n$ sono termini. Date delle espressioni del primo ordine $E_1,\cdots ,E_m$ e una sostituzione $\sigma$, con $E_i\cdot \sigma$ indico l’espressione ottenuta sostituendo alle variabili in $E_1$ i termini corrispondenti in $\sigma$. Se $E_1\cdot \sigma =E_2\cdot \sigma =\cdots =E_m\cdot \sigma$ diciamo che $\sigma$ è un unificatore di $E_1,\cdots ,E_m$.

Date due sostituzioni:

$$\begin{array}{rl}\sigma & =\{t_1/x_1,\cdots ,t_k/x_k,\cdots ,t_n/x_n\}\\ \theta & =\{v_1/x_1,\cdots ,v_k/x_k,u_1/y_1,\cdots ,u_l/y_l\}\end{array}$$

La sostituzione composizione è definita come:

$$(\sigma \cdot \theta )=\{t_1\cdot \theta /x_1,\cdots ,t_n\cdot \theta /x_n,u_1/y_1,\cdots ,u_l/x_l\}$$

Unificatore più generale

L’unificatore più generale delle espressioni $E_1,\cdots ,E_m$ è un unificatore $\sigma$ tale che per ogni altro unificatore $\rho$ di $E_1,\cdots ,E_m$ esiste una sostituzione $\theta$ tale che:

$$\rho =\sigma \cdot \theta$$

Cioè, $\sigma$ unifica con meno vincoli di $\rho$.

Risolvente

Note

Una risolvente tra le due clausole $c_1,c_2$ in cui supponiamo che abbiamo variabili distinte è la clausola $R$ ottenuta nel seguente modo:

$$c_1=\{\cdots ,L_1,\cdots ,L_e,\cdots \}{c}_2=\{\cdots ,\neg S_1,\cdots ,\neg S_k,\cdots \}$$

Se $\sigma$ è un unificatore più generale di $L_1,\cdots ,L_e,S_1,\cdots ,S_k$, (sostituendo tutto con $L$)Allora:

$$R=c_1\cdot \sigma \setminus \{L\}\cup c_2\cdot \sigma \setminus \{\neg L\}$$

E scriviamo $c_1,c_2{⊢}_{R}R$.

Derivazione

Note

Sia ${\Lambda }^C$ un insieme di clausole, una derivazione della clausola $C$ da ${\Lambda }^C$ (scritto ${\Lambda }^C{⊢}_{R}C$) è una sequenza $C_1,\cdots ,C_k=C$ delle clausole tale che:

$${\Lambda }^C{⊢}_R{C}_1,{\Lambda }^C\cup \{C_1\}{⊢}_R{C}_2,\cdots ,{\Lambda }^C\cup \{C_1,\cdots ,C_k\}{⊢}_R{C}_k$$

Dove $C_i$ è una risolvente tra le due clausole ${\Lambda }^C\cup \{C_1,\cdots ,C_{k-1}\}{⊢}_R{C}_k$.

Per il teorema di correttezza e completezza per refutazione diciamo che:

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

Inoltre:

$$\Gamma \models A\text{ se e solo se }\Lambda =\Gamma \cup \{\neg A\}\text{ eˋ insoddisfacibile se e solo se}{\Lambda }^C{⊢}_R\square$$