Risoluzione logica

Note

Troviamo le clausole di una FBF :

  • Se non è chiusa, chiuderla universalmente.
  • Portare in forma di Skolem .
  • Portare la matrice di in FNC.
  • Rinomino le variabili tar clausole in modo distinto, per avere il massimo grado di libertà per trovare .

Per risolvere due clausole utilizziamo la sostituzione.

Sostituzione

Note

Una sostituzione è una scrittura: Dove sono variabili distinte, mentre sono termini. Date delle espressioni del primo ordine e una sostituzione , con indico l'espressione ottenuta sostituendo alle variabili in i termini corrispondenti in . Se diciamo che è un unificatore di .

Date due sostituzioni: La sostituzione composizione è definita come:

Unificatore più generale

L'unificatore più generale delle espressioni è un unificatore tale che per ogni altro unificatore di esiste una sostituzione tale che: Cioè, unifica con meno vincoli di .

Risolvente

Note

Una risolvente tra le due clausole in cui supponiamo che abbiamo variabili distinte è la clausola ottenuta nel seguente modo: Se è un unificatore più generale di , (sostituendo tutto con )Allora: E scriviamo .

Derivazione

Note

Sia un insieme di clausole, una derivazione della clausola da (scritto ) è una sequenza delle clausole tale che:
Dove è una risolvente tra le due clausole .

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