Sarve klausel — Horni lausete definitsioon, omadused ja Prologi rakendused

Sarve klausel on kirjete loogiline disjunktsioon, kus maksimaalselt üks kirjetele vastavatest literaalidest on positiivne (mitte negerdatud) ja kõik ülejäänud on negatiivsed (negerdatud). Nimetus tuleb Alfred Horni järgi, kes kirjeldas neid 1951. aastal. Sarve klausleid nimetatakse sageli ka Horni lauseteks.

Erinevaid Horni lausete alamliike nimetatakse tavaliselt järgmiselt:

kindel lause — Horni lause, kus on täpselt üks positiivne literaal ja üks või mitu negatiivset literaali;
fakt — kindel lause ilma negatiivsete literaalideta (s.o ainult üks positiivne literaal);
eesmärgiklausel (goal clause) — Horni lause ilma positiivse literaalita (s.o ainult negatiivsed literaalid), mida sageli kasutatakse eitusena teoreemide tõestamisel.

Propositsioonilise näitena illustreerivad neid kolme tüüpi järgmised laused:

kindel klausel: ¬ 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$

fakt: u {\displaystyle u} $u$

eesmärgiklausel: ¬ p ∨ ¬ q ∨ ∨ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\neg p\lor \neg q\vee \cdots \vee \neg t$

Horni laused esimese järjekorra loogikas

Kui Horni lausetes kasutatakse predikaate ja muutujad esinevad (st tegemist ei ole ainult propositsioonilise tasemega), siis oletatakse tavaliselt, et kõik lauses olevad muutujad on kogu lausega kaudselt universaalselt kvantifitseeritud. Näiteks lause

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

tähistab tegelikult

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

mis on loogiliselt samaväärne implikatsiooniga:

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

Roll automatiseeritud teoreemitõendamises ja arvutusloogikas

Sarve klauslid on konstruktiivses loogikas ja arvutusloogikas keskse tähtsusega. Oluline omadus on see, et Horni lausete hulgas tehtav resolutsioon (lahendamine) säilitab Horni lause kuju: kahe Horni lause resolvent on endiselt Horni lause; lisaks resolventeerituna kindla lause ja eesmärgiklausli vahel saadav tulemus on jälle eesmärgiklausel. See omadus lihtsustab ja kiirendab automatiseeritud teoreemitõendamist, sest otsinguruumi saab kitsendada ja resolutsioonireegleid optimeerida.

Seos loogilise programmeerimise ja Prologiga

Sarve klauslid on loogilise programmeerimise aluseks. Kindlaid klausleid on mugav kirjutada implikatsiooni kujul, kus negatiivsed literaalid esitatakse vasakul (eeldused / kehad) ja positiivne literaal paremal (järeldus / pea):

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

Praktilises loogilises programmeerimises kasutatakse eesmärgiklausli lahendamist kindla klausliga, et saada uus eesmärgiklausel — see on SLD-lahenduse (SLD-resolution) järeldusreegli tuum. See moodustab aluse loogilisele programmeerimisele ja Prologi rakendustele.

Kindel klausel toimib loogilises programmeerimises kui protseduur eelduste täitmiseks: lause (p ∧ q ∧ ... ∧ t) → u tähendab, et ettekirjutuse kohaselt saab järeldada u siis, kui on võimalik näidata (lahendada) kõik p, q, ..., t. Seda rõhutatakse sageli kirjutades klausli "tagurpidi" (proseduuriline) kujul:

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

Prologis kirjutatakse see lause tavaliselt nii:

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

Oluline on märkida, et Prologi süntaks ja semantika sisaldavad mitmesuguseid nüansse. Näiteks võib eesmärgiklausli muutujate kvantifitseerimist mõnikord tõlgendada kas universaalse või eksistentsiaalse kvantifikaatorina, ning lõpliku "vale" tuletamise tõlgendus võib sõltuda sellest, kas käsitleda seda vastuolu tuvastamisena või lahenduse leidmisena (näiteks negatsiooni failu kaudu, negation as failure).

Mudeliteoreetika ja minimaalne mudel

Van Emden ja Kowalski (1976) analüüsisid Horni lausete mudeliteooriat loogilise programmeerimise vaatenurgast. Nad näitasid, et iga kindlate lausete hulgaga D on seotud ainulaadne minimaalne mudel M (st selline mudel, mis sisaldab kõiki D-st loogiliselt tuletatavaid aatomeid ja ei sisalda ülearuseid aatomeid). Aatomivalem A on D-st loogiliselt järjepidevalt tuletatav siis ja ainult siis, kui A on tõene M-s. Sama kehtib ka probleemide puhul, mida esindavad eksistentsiaalselt kvantifitseeritud positiivsete kirjete konjunktsioonid: need on D-st loogiliselt seotud parajasti siis, kui need on tõestatavad minimaalses mudelis M.

See minimaalne mudelisemantika on aluseks ka keerukamatele semantilistele raamistikule nagu stabiilne mudelsemantika (stable model semantics) ja muud mitte-monotoonsed laiendused, mida kasutatakse deklaratiivsetes programmeerimiskeeltes (näiteks answer set programming).

Arvutuslik keerukus ja otsustatavus

Propositsiooniliste Horni lausete rahuldatavusprobleem on arvutusliku keerukuse mõttes lihtsam kui üldine Boole'i rahuldatavusprobleem (SAT). Konjunktsioonide tõeväärtuse määramine nii, et kõik propositsioonilised Horni laused oleksid tõesed, on P-aegne (lineaalse aja) ja seda mõnikord nimetatakse HORNSAT-iks. Seevastu piiranguteta Boole'i rahuldatavuse probleem on NP-täielik.

Kui liigume esimese järjekorra Horni lausete juurde (kus on predikaadid ja muutujad), siis rahuldatavusprobleem muutub keerulisemaks ja on üldjuhul otsustamatu — s.t. ei eksisteeri algoritmi, mis igal sisendil otsustab täpselt, kas antud esimese järjekorra Horni laused on rahuldavad.

Kasutusalad ja praktilised märkused

Loogilises programmeerimises (eriti Prologis) kasutatakse Horni klausleid teadmiste esindamiseks ja päringute lahendamiseks; optimeeritud lahendused kasutavad SLD-lahendust ja tagasipööramist (backtracking).
Automatiseeritud teoreemitõendites lubavad Horni lausete omadused kiiremat ja mälusäästlikumat tõestamist võrreldes üldiste lausetega.
Horni klausleid kasutatakse ka teadmistepõhistes süsteemides, ekspertprogrammides ning mõnedes loogikapõhistes andmebaasides ja reeglipõhistes masinõppe rakendustes.

Lõpetuseks tasub rõhutada, et Horni klauslid moodustavad praktilise ja teoreetiliselt hästi mõistetava alamklassifikatsiooni loogikast, mis ühendab tugeva mudeliteoreetilise aluse ja efektiivsed arvutusmeetodid — seetõttu on nad püsivalt olulised nii teadusuuringutes kui ka rakendustes.

näidata u {\displaystyle u} $u$ , näidata p {\displaystyle p} $p$ ja näidata q {\displaystyle q} ja ⋯ {\displaystyle \cdots } $\cdots$ ja show t {\displaystyle t} $t$

$u\leftarrow (p\land q\land \cdots \land t)$

Küsimused ja vastused

K: Mis on sarveklausel?

V: Sarve klausel on loogiline kirjavahemärkide disjunktsioon, kus kõige rohkem üks kirjavahemärkidest on positiivne ja kõik teised on negatiivsed.

K: Kes neid esimesena kirjeldas?

V: Alfred Horn kirjeldas neid esimest korda 1951. aastal avaldatud artiklis.

K: Mis on kindel klausel?

V: Horni lauset, milles on täpselt üks positiivne literaal, nimetatakse kindlasõnaliseks lauseks.

K: Mis on fakt?

V: Määratletud lauset, millel ei ole ühtegi negatiivset kirjavahemärki, nimetatakse mõnikord "faktiks".

K: Mis on eesmärgilause?

V: Sarve lauset, millel puudub positiivne literaal, nimetatakse mõnikord eesmärgilauseks.

K: Kuidas toimivad muutujad mittepropositsioonilistes juhtudel?

V: Mittepropositsioonilisel juhul on kõik muutujad lauses kaudselt universaalselt kvantifitseeritud kogu lause ulatusega. See tähendab, et need kehtivad avaldise iga osa suhtes.

K: Millist rolli mängivad Horni laused konstruktiivses loogikas ja arvutusloogikas? V: Horn-klauslid mängivad olulist rolli automatiseeritud teoreemitõendamises esimese järjekorra lahendamise teel, sest kahe Horn-klausli või ühe eesmärgi ja ühe kindla klausli vahelist resolventi saab kasutada suurema efektiivsuse loomiseks, kui tõestatakse midagi, mis on esitatud oma eesmärgi klausli eitusena. Neid kasutatakse ka loogiliste programmeerimiskeelte, näiteks Prologi alusena, kus nad käituvad nagu eesmärgi vähendamise protseduurid.