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. Prendono il nome da Alfred Horn che per primo ne evidenziò l'importanza (1951).[1]

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.

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]

Nella teoria della complessità 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.[2]

Programmazione logica[modifica | modifica wikitesto]

Le clausole di Horn sono alla base della programmazione logica, dove è comune scrivere clausole definite in forma di implicazione logica:

(p \land q \land ... \land t) \to u

Tale implicazione viene solitamente scritta al contrario, per enfatizzarne la semantica:

u \gets (p \land q \land ... \land t)

La regola basata su tale clausola, infatti, ha il seguente significato:

per dimostrare u, dimostra p e dimostra q e ... e dimostra t.

In Prolog la regola è scritta nel modo seguente:

u :- p, q, ..., t.

Van Emden and Kowalski (1976) investigarono sulle proprietà delle clausole di Horn all'interno della teoria dei modelli e programmazione logica, dimostrando che ogni insieme di clausole definite D ha un unico modello minimale M_D. Una formula atomica A è logicamente implicata da D se e solo se M \vDash A, ovvero se A è vera secondo M. Il concetto di modello minimale per le clausole di Horn è alla base della semantica del modello stabile.[3]

Note[modifica | modifica wikitesto]

  1. ^ (EN) Alfred Horn, On sentences which are true of direct unions of algebras, in Journal of Symbolic Logic, vol. 16, nº 1, 1951, pp. 14–21, DOI:10.2307/2268661.
  2. ^ (EN) William F. Dowling e Jean H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, in Journal of Logic Programming, vol. 1, nº 3, 1984, pp. 267–284, DOI:10.1016/0743-1066(84)90014-1.
  3. ^ (EN) M. H. van Emden e R. A. Kowalski, The semantics of predicate logic as a programming language (PDF), in Journal of the ACM, vol. 23, nº 4, 1976, pp. 733–742, DOI:10.1145/321978.321991.

Voci correlate[modifica | modifica wikitesto]

Collegamenti esterni[modifica | modifica wikitesto]