Clausola di Horn

Da Wikipedia, l'enciclopedia libera.

In logica, e in particolare nel calcolo proposizionale, una clausola di Horn è una disgiunzione di letterali in cui al massimo uno dei letterali è positivo.

Un esempio di clausola di Horn è il seguente:

\neg A \vee \neg B \vee C

Il numero dei letterali può essere arbitrario (anche zero); la condizione che al massimo uno sia positivo permette di scrivere la clausola sotto forma di implicazione.

Se il numero di letterali positivi è esattamente uno, la clausole di Horn vengono dette "definite", la cui premessa (corpo) è una congiunzione di letterali positivi e la sua conclusione (testa) è un singolo letterale positivo.

Le clausole di Horn definite formano la base della programmazione logica.

Partendo dall'esempio, applichiamo prima De Morgan:

\neg (A \wedge B) \vee C

Dopodiché utilizziamo l'equivalenza logica:

\neg X \vee Y \equiv  X \Rightarrow Y

Ricaviamo quindi:

(A \wedge B) \Rightarrow C

Casi particolari[modifica | modifica wikitesto]

Una clausola di Horn senza letterali negativi, può essere vista come una clausola di Horn definita che si limita ad asserire una determinata proposizione, e talvolta viene chiamata "fatto".

 A

Una clausola di Horn senza letterali positivi può essere scritta come una implicazione la cui conclusione vale falso. Esempio:

\neg A \vee \neg B \vee \neg C

De Morgan:

\neg (A \wedge B \wedge C)
\neg (A \wedge B \wedge C) \vee Falso
(A \wedge B \wedge C) \Rightarrow Falso

Nel campo dei database, formule di questo tipo sono chiamate vincoli di integrità.

Horn-Soddisfacibilità[modifica | modifica wikitesto]

Le Clausole di Horn risultano essere particolarmente interessanti poiché il problema della soddisfacibilità di una formula booleana nel caso particolare in cui le clausole della formula siano tutte Clausole di Horn (detto problema della Horn-Soddisfacibilità) ha complessità polinomiale.

Voci correlate[modifica | modifica wikitesto]