Sistemi deduttivi

Note

La finalità di un sistema deduttivo, o un metodo formale, è di avere un metodo automatico per verificare che .
Quindi partendo dall'insieme e da un insieme di assiomi , con delle regole di riscrittura, dette di inferenza, cerchiamo di generare una sequenza di FBF tale che: I sistemi formali possono essere:

  • Corretti:
  • Completi:

Teoria L

Note

Ha come sintassi una FBF contenenti solo e . Gli assiomi sono: Questi in realtà sono schemi di assiomi poiché sono FBF. Inoltre consideriamo come regola d'inferenza la "modus ponens":

Quindi se da un insieme di formula , usando gli assiomi e il modus ponens ottengo una sequenza di FBF tale che: Allora si dice che è un teorema della teoria L che ha premesse e è una dimostrazione di , e scriviamo

Teorema di correttezza e completezza forte

La teoria L è:

  • Corretta:
  • Completa:

Nel caso , il teorema si riduce a , cioè è una tautologia.

Risoluzione

Note

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

  • Letterale: una lettera enunciativa o una sua negata ( o )
  • Clausola: È un insieme di letterali, anche dette stringhe privilegiate. La clausola vuota è indicata come , mentre l'insieme di clausole di è
  • Regola d'inferenza: diciamo che la clausola è una risolvente delle clausole e scriviamo se:
Warning

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

Sia l'insieme di clausole, una derivazione per risoluzione della clausola da è una sequenza di clausole tale che e:

Tip

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