Clauza Horn

În logică și în special în calculul propozițional , o clauză Horn este o disjuncție a literelor în care cel mult unul dintre literali este pozitiv . Ele poartă numele lui Alfred Horn, care a subliniat pentru prima dată importanța lor (1951). ^[1]

Un exemplu de clauză Horn este după cum urmează:

\neg A\vee \neg B\vee C

{\ displaystyle \ neg A \ vee \ neg B \ vee C}

{\ displaystyle \ neg A \ vee \ neg B \ vee C}

Numărul literelor poate fi arbitrar (chiar zero); condiția ca cel mult unul să fie pozitiv permite clauzei să fie scrisă sub forma unei implicații.

Dacă numărul literalilor pozitivi este exact unul, clauzele lui Horn se spune că sunt „definite”, a căror premisă (corp) este o conjuncție de literali pozitivi și concluzia (capul) este un singur literal pozitiv.

Pornind de la exemplu, să aplicăm mai întâi De Morgan :

\neg (A\wedge B)\vee C

{\ displaystyle \ neg (A \ wedge B) \ vee C}

{\ displaystyle \ neg (A \ wedge B) \ vee C}

Apoi folosim echivalența logică:

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

{\ displaystyle \ neg X \ vee Y \ equiv X \ Rightarrow Y}

{\ displaystyle \ neg X \ vee Y \ equiv X \ Rightarrow Y}

Prin urmare, obținem:

(A\wedge B)\Rightarrow C

{\ displaystyle (A \ wedge B) \ Rightarrow C}

{\ displaystyle (A \ wedge B) \ Rightarrow C}

Cazuri speciale

O clauză Horn fără literale negative poate fi văzută ca o clauză Horn definită care afirmă doar o anumită propoziție și este uneori numită „fapt”.

LA

{\ displaystyle A}

LA

O clauză Horn fără literali pozitivi poate fi scrisă ca o implicație a cărei concluzie este falsă. Exemplu:

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

{\ displaystyle \ neg A \ vee \ neg B \ vee \ neg C}

{\ displaystyle \ neg A \ vee \ neg B \ vee \ neg C}

De Morgan :

\neg (A\wedge B\wedge C)

{\ displaystyle \ neg (A \ wedge B \ wedge C)}

{\ displaystyle \ neg (A \ wedge B \ wedge C)}

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

{\ displaystyle \ neg (A \ wedge B \ wedge C) \ vee False}

{\ displaystyle \ neg (A \ wedge B \ wedge C) \ vee False}

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

{\ displaystyle (A \ wedge B \ wedge C) \ Rightarrow False}

{\ displaystyle (A \ wedge B \ wedge C) \ Rightarrow False}

În câmpul bazei de date, astfel de formule se numesc constrângeri de integritate .

Corn-satisfacție

În teoria complexității , clauzele Horn sunt deosebit de interesante, deoarece problema satisfacibilității unei formule booleene în cazul particular în care clauzele formulei sunt toate clauzele Horn (numită problema Horn-satisfacție ) are complexitate polinomială . ^[2]

Programare logică

Clauzele Horn sunt baza programării logice , unde este obișnuit să scrieți clauze definite sub forma implicației logice :

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

{\ displaystyle (p \ land q \ land ... \ land t) \ to u}

{\ displaystyle (p \ land q \ land ... \ land t) \ to u}

Această implicație este de obicei scrisă înapoi, pentru a-i sublinia semantica:

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

{\ displaystyle u \ gets (p \ land q \ land ... \ land t)}

{\ displaystyle u \ gets (p \ land q \ land ... \ land t)}

De fapt, regula bazată pe această clauză are următorul sens:

a dovedi

tu

${\ displaystyle u}$ $tu$ , demonstrează

p

${\ displaystyle p}$ $p$ și demonstrează

q

${\ displaystyle q}$ $q$ și ... și demonstrează

t

${\ displaystyle t}$ $t$ .

În Prolog regula este scrisă după cum urmează:

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

Van Emden și Kowalski (1976) au investigat proprietățile clauzelor Horn în cadrul teoriei modelelor și al programării logice, arătând că orice set de clauze definite $D.$ ${\ displaystyle D}$ $D.$ are un singur model minim $M_{D}$ ${\ displaystyle M_ {D}}$ ${\ displaystyle M_ {D}}$ . O formulă atomică $LA$ ${\ displaystyle A}$ $LA$ este implicit logic de $D.$ ${\ displaystyle D}$ $D.$ dacă și numai dacă $M\vDash A$ ${\ displaystyle M \ vDash A}$ ${\ displaystyle M \ vDash A}$ , adică dacă $LA$ ${\ displaystyle A}$ $LA$ este adevărat în al doilea rând $M.$ ${\ displaystyle M}$ $M.$ . Conceptul de model minim pentru clauzele Horn stă la baza semanticii modelului stabil . ^[3]