Horn, clausola di
Horn, clausola di
Horn, clausola di in logica, → clausola avente una particolare struttura. In una clausola si distinguono letterali negativi, se sono espressi in forma negativa, cioè preceduti dal connettivo della negazione ￢, e positivi, se sono espressi altrimenti, e si definisce clausola di Horn, o formula di Horn, una clausola in cui al più un letterale è positivo (contiene, quindi, al più un letterale non negato). Un esempio di clausola di Horn è la seguente: A ∨ ￢B ∨ ￢C (si legge «A o non B o non C») in cui il primo letterale è in forma positiva mentre gli altri due sono in forma negativa, al contrario la formula A1 ∨ A2 ∨ ￢A3 ∨ ￢A4 non è una clausola di Horn perchè ci sono due letterali in forma positiva. Anche la formula ￢A ∨ ￢B ∨ ￢C, in cui non compaiono letterali positivi, è una clausola di Horn e lo stesso vale per una qualsiasi lettera proposizionale A. Ogni clausola di Horn può essere riscritta, in forma logicamente equivalente, come implicazione; per esempio:
• la clausola ￢A ∨ B è logicamente equivalente all’implicazione A ⇒ B (il simbolo ⇒ indica il connettivo di implicazione) come si deduce confrontando le rispettive tavole di verità;
• generalizzando, la clausola ￢A1 ∨ ￢A2 ∨ ￢A3 ∨ A4 è equivalente alla formula A1 ∧ A2 ∧ A3 ⇒ A4;
• anche una clausola del tipo ￢A ∨ ￢B ∨ ￢C può essere riscritta come implicazione nel modo seguente: A ∧ B ∧ C ⇒ ⊥ dove ⊥ è una qualsiasi contraddizione;
• una qualsiasi lettera proposizionale A è equivalente all’implicazione T ⇒ A dove T è una qualsiasi tautologia.
Su questa equivalenza si basa la possibilità di controllare la soddisfacibilità di un insieme di clausole di Horn (→ Horn-soddisfacibilità) in modo più efficiente, in termini di passi di calcolo e, quindi, di tempo, del ricorso alle tavole di verità. Per questo le clausole di Horn, introdotte dal logico di cui portano il nome nel 1951, trovano una peculiare applicazione nella logica matematica. Il loro impiego specifico è nei linguaggi di programmazione logica, utilizzati particolarmente per risolvere problemi legati all’intelligenza artificiale. Esse costituiscono, infatti, le istruzioni elementari su cui tali linguaggi si basano (→ prolog).