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:
- ¬ A ∨ ¬ B ∨ 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:
- ¬ (A ∧ B) ∨ C
Dopodiché utiliziamo l'equivalenza logica:
- ¬ X ∨ Y ≡ X ⇒ Y
Ricaviamo quindi:
- (A ∧ B) ⇒ C
[modifica] Casi particolari
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.
Una clausola di Horn senza letterali positivi può essere scritta come una implicazione la cui conclusione vale falso. Esempio:
- ¬ A ∨ ¬ B ∨ ¬ C
- ¬ (A ∧ B ∧ C)
- ¬ (A ∧ B ∧ C) ∨ Falso
- (A ∧ B ∧ C) ⇒ Falso
Nel campo dei database, formule di questo tipo sono chiamate vincoli di integrità.