Sarve klausel

Sarve klausel on kirjete loogiline disjunktsioon, kus kõige rohkem üks kirjetest on positiivne ja kõik teised on negatiivsed. See on nime saanud Alfred Horni järgi, kes kirjeldas neid 1951. aasta artiklis.

Täpselt ühe positiivse literaaliga Horni lause on kindel lause; kindlat lauset ilma negatiivsete literaalideta nimetatakse mõnikord "faktiks"; ja Horni lauset ilma positiivse literaalita nimetatakse mõnikord eesmärgilauseks. Neid kolme liiki Horn'i lauseid illustreerib järgmine propositsiooniline näide:

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$

Mittepropositsioonilisel juhul on kõik lauses olevad muutujad kaudselt universaalselt kvantifitseeritud kogu lausega. Seega näiteks:

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

tähistab:

∀ 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:

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

Sarve klauslid mängivad konstruktiivses loogikas ja arvutusloogikas põhilist rolli. Nad on olulised automatiseeritud teoreemitõendamisel esimese järjekorra lahendamise teel, sest kahe Horni lause resolvent on ise Horni lause ning eesmärgilause ja kindla lause resolvent on eesmärgilause. Need Horni lausete omadused võivad viia suurema efektiivsuse saavutamiseni teoreemi tõestamisel (mida kujutatakse eesmärgilause eitusena).

Sarve klauslid on ka loogilise programmeerimise aluseks, kus on tavaline kirjutada kindlaid klausleid implikatsiooni kujul:

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

Tegelikult on eesmärgiklausli lahendamine kindla klausliga uue eesmärgiklausli saamiseks aluseks SLD-lahendusjärelduse reeglile, mida kasutatakse loogilise programmeerimise ja programmeerimiskeele Prolog rakendamisel.

Loogilises programmeerimises käitub kindel klausel kui eesmärgi-reduktsiooni protseduur. Näiteks eespool kirjutatud Horni klausel käitub protseduurina:

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$

Selle tagurpidi kasutamise rõhutamiseks kirjutatakse see sageli tagurpidi 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 järgmiselt:

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

Prologi notatsioon on tegelikult mitmetähenduslik ja ka terminit "eesmärgiklausel" kasutatakse mõnikord mitmetähenduslikult. Muutujaid eesmärgiklauslis võib lugeda universaalselt või eksistentsiaalselt kvantifitseerituna ning "vale" tuletamist võib tõlgendada kas vastuolude tuletamisena või lahendatava probleemi eduka lahenduse tuletamisena.

Van Emden ja Kowalski (1976) uurisid Horni lausete mudeliteoreetilisi omadusi loogilise programmeerimise kontekstis, näidates, et igal kindla lausete hulgal D on unikaalne minimaalne mudel M. Aatomivalem A on loogiliselt kaudselt seotud D-ga, kui ja ainult siis, kui A on tõene M-s. Sellest järeldub, et probleem P, mida esindab eksistentsiaalselt kvantifitseeritud positiivsete kirjete konjunktsioon, on loogiliselt seotud D-ga, kui ja ainult siis, kui P on tõene M-s. Horni lausete minimaalne mudelisemantika on aluseks loogikaprogrammide stabiilse mudelisemantikale.

Propositsioonilised Horni laused pakuvad huvi ka arvutusliku keerukuse seisukohalt, kus tõeväärtuste määramise probleem, mis muudab propositsiooniliste Horni lausete konjunktsiooni tõeseks, on P-täielik probleem (tegelikult lahendatav lineaarses ajas), mida mõnikord nimetatakse HORNSATiks. (Piiranguteta Boole'i rahuldatavuse probleem on aga NP-täielik probleem). Esimese järjekorra Horni lausete rahuldatavus on otsustamatu.

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.