CNF logica del primo ordine
La forma normale congiuntiva ( CNF ) della logica del primo ordine è composta dalla congiunzione di un insieme di formule, ognuna delle quali è formato da una disgiunzione di letterali ( variabili ). La forma CNF della logica del primo ordine è simile a quella della logica proposizionale. Mentre nella logica proposizionale le clausole sono composte da letterali che possono assumere soltanto valori booleani ( vero o falso ), nella logica del primo ordine le funzioni possono assumere un dominio di valori molto più ampio. Inoltre, nella logica del primo ordine le funzioni possono essere caratterizzate anche da quantificatori universali e/o esistenziali. Ogni formula della logica del primo ordine può essere trasformata in una formula CNF equivalente. La conversione alla forma CNF si ottiene eliminando i quantificatori esistenziali e le implicazioni. Un esempio di disgiunzione della forma normale congiuntiva del primo ordine è la seguente:
¬Caramella(x) ∨ Mangia ( Tom, x )
Le precedente disgiunzione è equivalente alla seguente espressione della logica del primo ordine che, a sua volta, equivale all'affermazione del linguaggio naturale ( "Tom mangia tutte le caramelle" ).
∀ x Caramella(x) ⇒ Mangia ( Tom, x )
La forma CNF non è facilmente leggibile per un essere umano. Ha però il vantaggio di essere facilmente elaborata in un computer ed è, pertanto, una forma più idonea per risolvere i problemi tramite il ragionamento automatico e per le procedure di inferenza logiche.
- Dimostrazioni per assurdo. Se una formula del primo ordine è insoddisfacibile, allora lo è anche la formula equivalente nella forma CNF del primo ordine. Ciò consente di utilizzare la logica del primo ordine nelle dimostrazioni per assurdo. Nel seguente esempio sono rappresentate due formule nella logica del primo ordine, una premessa e una conclusione. Le due formule sono trasformate nella forma CNF. Successivamente è possibile verificare se la conclusione è una conseguenza logica tramite il metodo della risoluzione. La conclusione viene negata ( ipotesi per assurdo ). Se l'ipotesi opposta ( assurda ) non è logicamente soddisfacibile dalla premessa ( clausola vuota ) allora è sicuramente vero il contrario, ossia la conclusione ( ipotesi di partenza ) è effettivamente una conseguenza logica dell premessa.
