Clausola di Horn

La clausola di Horn è una disgiunzione di letterali in cui al massimo un letterale è positivo. È un caso particolare della logica proposizionale. Data una clausola e tre letterali (a, b, c) sono clausole di Horn le seguenti:

¬a ∨ b ∨ c
¬a ∨ ¬b ∨ ¬c

Tutte le clausole definite sono clausole di Horn. L'insieme delle clausole di Horn è, tuttavia, molto più vasto e generale poiché comprende anche le clausole composte da tutti i letterali negativi ( clausole obiettivo ). Ad esempio, la clausola ( ¬a ∨ ¬b ∨ ¬c ) è una clausola di Horn ma non è una clausola definita in quanto manca il letterale positivo. Come le clausole definite anche le clausole di Horn possono essere rappresentate sotto forma di implicazione logica. Dati i letterali negativi (a, b), detta "premessa" o "corpo", si implica come conseguenza logica il terzo letterale (c), detto "conclusione" o "testa", che può essere positivo o negativo.

(a ∧ b ) ⇒ c

Una clausola di Horn senza letterali positivi può essere rappresentata come un'implicazione la cui conclusione è falsa.

(a ∧ b ) ⇒ ¬c

Le clausole di Horn sono alla base della programmazione logica e dei vincoli di integrità di un database.

Complessità temporale. Uno dei principali vantaggi delle clausole di Horn è la caratteristica di risolvere un problema facendo crescere la complessità temporale in modo lineare rispetto alla dimensione della base di conoscenza. Date due clausole di Horn, la risoluzione delle stesse dà come risultato un'altra clausola di Horn. Ad esempio, date le clausole ( ¬a ∨ ¬b ∨ ¬c ) e ( ¬a ∨ ¬b ∨ c ), risolvendo le stesse si ottiene la clausola ( ¬a ∨ ¬b ) che è anch'essa una clausola di Horn.