Forma clausale ( forma normale congiuntiva o CNF )
La forma clausale è una rappresentazione della logica che consente di formalizzare le proposizioni del linguaggio naturale. La forma clausale è anche conosciuta come CNF ( Conjunctive Normal Form ) ed è traducibile in forma normale congiuntiva. Una clausola è una disgiunzione finita di zero o più letterali ( insieme di letterali ). Ogni letterale è una formula atomica ( p ) o la negazione di una formula atomica ( ¬p ) . Una formula in forma normale congiunta o congiuntiva ( CNF ) è la seguente:
( ¬A ∨ C ) ∧ ( ¬B ∨ C )
La forma CNF coincide con la forma DNF / FND ( forma normale disgiuntiva ) quando è composta da una disgiunzione di letterali anziché di clausole. Ad esempio la seguente forma è una rappresentazione DNF poiché ogni clausola è composta da un singolo letterale.
( ¬A ∨ C )
Ogni formula nella forma clausale ( CNF ) equivale logicamente alla forma di una formula scritta secondo le regole della logica proposizionale, in quanto ogni formula della logica proposizionale ( forma standard della logica ) può essere riscritta sotto forma di una congiunzione di clausole. A differenza della logica proposizionale, a parità di completezza e di equivalenza logica, la forma clausale è la più idonea all'elaborazione informatica e al ragionamento automatico.
Conversione di una proposizione logica in clausola. Ad esempio, la seguente formula ( A ∨ B ) ⇔ C è inizialmente rappresentata secondo la logica proposizionale e può essere trasformata nella sua equivalente forma clausale con i seguenti passaggi logico-matematici.
( A ∨ B ) ⇔ C
Sostituendo il bicondizionale ⇔ con altri simboli di implicazione ⇒ è possibile trasformare la formula nella seguente forma:
( ( A ∨ B ) ⇒ C ) ∧ ( C ⇒ ( A ∨ B ) )
E' ora possibile sostituire il simbolo di implicazione ⇒ trasformando la formula ( α⇒β ) nella forma logica ( ¬α ∨ β ).
¬( A ∨ B ) ∨ C ∧ ¬C ∨ ( A ∨ B )
E' ora necessario spostare i simboli di negazione davanti a ogni singolo letterale ( formula atomica ). In base alle leggi di Morgan, nel caso del nostro esempio, la forma ¬( α ∨ β ) equivale a ( ¬α ∧ ¬β ). È quindi possibile riscrivere l'intera formula nel seguente modo:
( ¬A ∧ ¬B ) ∨ C ∧ ¬C ∨ ( A ∨ B )
La formula è ora rappresentata come una sequenza di letterali e operatori logici nidificati. Per trasformarla in una forma clausale più comprensibile è necessario raggruppare gli operatori ∨ separando le clausole, quando possibile, dagli operatori ∧. Questa operazione consente di separare tra loro le clausole della formula.
( ( ¬A ∨ C ) ∧ ( ¬B ∨ C ) ) ∧ ( ¬C ∨ A ∨ B )
Eliminando le parentesi non necessarie, è possibile ottenere una formula in forma clausale come congiunzione di tre distinte clausole.
( ¬A ∨ C ) ∧ ( ¬B ∨ C ) ∧ ( ¬C ∨ A ∨ B )
Se C è vera allora anche A ( oppure B ) è vera. Se A è vera allora anche C deve essere vera. Se B è vera allora anche C deve essere vera. In conclusione, la forma clausale si avvicina più al formalismo di un linguaggio di programmazione informatica ( es. Prolog ) che a quello della logica matematica ( metodo della risoluzione ). È quindi più facile da elaborare in un computer. La forma clausale è utilizzata nella programmazione logica e nella logica matematica.
Inferenza logica. Il formalismo clausale consente di applicare delle regole di inferenza automatiche ( es. metodo della risoluzione ) per dimostrare la veridicità o meno di una proposizione logica ( ipotesi ) rispetto a un sistema logico di riferimento ( base di conoscenza ). È quindi un strumento molto versatile per la realizzazione dei software risolutori di problemi, dei sistemi esperti e di intelligenza artificiale.
