Clauză Horn

O clauză Horn este o disjuncție logică de literali, în care cel mult unul dintre literali este pozitiv, iar toți ceilalți sunt negativi. Este denumită astfel după Alfred Horn, care a descris-o într-un articol din 1951.

O clauză Horn cu exact un literal pozitiv este o clauză definită; o clauză definită fără literali negativi se numește uneori "fapt"; iar o clauză Horn fără un literal pozitiv se numește uneori clauză obiectiv. Aceste trei tipuri de clauze Horn sunt ilustrate în următorul exemplu propozițional:

clauză definită: ¬ p ∨ ¬ q ∨ ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

fapt: u {\displaystyle u} $u$

clauza obiectivului: ¬ p ∨ ¬ q ∨ ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\neg p\lor \neg q\vee \cdots \vee \neg t$

În cazul nepropozițional, toate variabilele dintr-o propoziție sunt implicit cuantificate universal, cu domeniul de aplicare al întregii propoziții. Astfel, de exemplu:

¬ human ( X ) ∨ mortal ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)\lor {\text{mortal}}(X)} $\neg {\text{human}}(X)\lor {\text{mortal}}(X)$

reprezintă:

∀ X ( ¬ uman ( X ) ∨ muritor ( X ) ) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))} $\forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))$

care este logic echivalent cu:

∀ X ( uman ( X ) → muritor ( X ) ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). } $\forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).$

Clauzele Horn joacă un rol de bază în logica constructivă și în logica computațională. Ele sunt importante în demonstrarea automată a teoremelor prin rezoluția de ordinul întâi, deoarece rezolvarea a două clauze Horn este ea însăși o clauză Horn, iar rezolvarea unei clauze obiectiv și a unei clauze definite este o clauză obiectiv. Aceste proprietăți ale clauzelor Horn pot duce la o eficiență mai mare în demonstrarea unei teoreme (reprezentată ca negație a unei clauze de scop).

Clauzele Horn stau, de asemenea, la baza programării logice, unde este obișnuit să se scrie clauze definite sub forma unei implicații:

( p ∧ q ∧ ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u} $(p\wedge q\wedge \cdots \wedge t)\rightarrow u$

De fapt, rezolvarea unei clauze de scop cu o clauză definită pentru a produce o nouă clauză de scop reprezintă baza regulii de inferență de rezolvare SLD, utilizată pentru implementarea programării logice și a limbajului de programare Prolog.

În programarea logică, o clauză definită se comportă ca o procedură de reducere a obiectivelor. De exemplu, clauza Horn scrisă mai sus se comportă ca o procedură:

pentru a arăta u {\displaystyle u} $u$ , arată p {\displaystyle p} $p$ și arată q {\displaystyle q} și ⋯ {\displaystyle \cdots } $\cdots$ și show t {\displaystyle t} $t$ .

Pentru a sublinia această utilizare inversă a clauzei, aceasta este adesea scrisă în forma inversă:

u ← ( p ∧ q ∧ ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} $u\leftarrow (p\land q\land \cdots \land t)$

În Prolog acest lucru se scrie ca:

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

Notația Prolog este, de fapt, ambiguă, iar termenul "clauză de scop" este, de asemenea, utilizat uneori în mod ambiguu. Variabilele dintr-o clauză de scop pot fi citite ca fiind cuantificate universal sau existențial, iar derivarea "fals" poate fi interpretată fie ca derivare a unei contradicții, fie ca derivare a unei soluții reușite a problemei care trebuie rezolvată.

Van Emden și Kowalski (1976) au investigat proprietățile teoretice ale modelului clauzelor Horn în contextul programării logice, arătând că fiecare set de clauze definite D are un model minim unic M. O formulă atomică A este implicată logic de D dacă și numai dacă A este adevărată în M. Rezultă că o problemă P reprezentată de o conjuncție existențial cuantificată de literali pozitivi este implicată logic de D dacă și numai dacă P este adevărată în M. Semantica modelului minim al clauzelor Horn este baza pentru semantica modelului stabil al programelor logice.

Clauzele propoziționale Horn prezintă, de asemenea, interes în domeniul complexității computaționale, unde problema de a găsi atribuiri de valori de adevăr care să facă adevărată o conjuncție de clauze propoziționale Horn este o problemă P-completă (de fapt, rezolvabilă în timp liniar), denumită uneori HORNSAT. (Cu toate acestea, problema satisfiabilității booleene nerestricționate este o problemă NP-completă). Satisfiabilitatea clauzelor Horn de ordinul întâi este nedecisă.

Întrebări și răspunsuri

Î: Ce este o clauză de corn?

R: O clauză Horn este o disjuncție logică de literali, în care cel mult unul dintre literali este pozitiv și toți ceilalți sunt negativi.

Î: Cine le-a descris prima dată?

R: Alfred Horn le-a descris pentru prima dată într-un articol din 1951.

Î: Ce este o clauză definită?

R: O clauză Horn cu exact un literal pozitiv se numește clauză definită.

Î: Ce este un fapt?

R: O clauză definită fără literali negativi este denumită uneori "fapt".

Î: Ce este o clauză goal?

R: O clauză Horn fără un literal pozitiv se numește uneori clauză de scop.

Î: Cum funcționează variabilele în cazurile nepropoziționale?

R: În cazul nepropozițional, toate variabilele dintr-o clauză sunt implicit cuantificate universal cu domeniul de aplicare întreaga clauză. Aceasta înseamnă că se aplică la fiecare parte a enunțului.

Î: Ce rol joacă clauzele Horn în logica constructivă și în logica computațională? R: Clauzele Horn joacă un rol important în demonstrarea automată a teoremelor prin rezoluția de ordinul întâi, deoarece rezolvarea dintre două clauze Horn sau dintre o clauză scop și o clauză definită poate fi utilizată pentru a crea o eficiență mai mare atunci când se demonstrează ceva reprezentat ca negație a clauzei sale scop. Ele sunt, de asemenea, utilizate ca bază pentru limbaje de programare logică, cum ar fi Prolog, unde se comportă ca proceduri de reducere a obiectivelor.