Hornova klavzula (Hornov stavek): definicija, primeri in uporaba v Prologu

Hornova klavzula: jasna definicija, praktični primeri in uporaba v Prologu — naučite se razlikovati dejstva, cilje in pravila za učinkovito logično programiranje.

Hornov stavek je logična disjunkcija literalov, v kateri je največ en literal pozitiven, vsi ostali pa so negativni. Poimenovan je po Alfredu Hornu, ki ga je opisal leta 1951. Hornovi stavki so pomembna razred stavkov v propozicijski in prviordni logiki zaradi svoje preproste strukture in ugodnih računskih lastnosti.

Posebne podvrste Hornovih stavkov so:

• določni stavek (definite clause): Hornov stavek s točno enim pozitivnim literalom;
• dejstvo: določni stavek brez negativnih literalov (torej le en pozitiven literal);
• ciljni stavek (goal/clause): Hornov stavek brez pozitivnega literala (v praksi se uporablja za izražanje ciljev ali vprašanj).

Te tri vrste Hornovih stavkov v propozicionalnem primeru izgledajo tako:

določni stavek: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

dejstvo: u {\displaystyle u}

klavzula o cilju: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}

Prviordni (nepropozicijski) primer

Pri prvem redu logike se spremenljivke v stavku običajno implicitno univerzalno kvantificirajo z obsegom celotnega stavka. Na primer:

¬ človek ( X ) ∨ smrtnik ( X ) {\displaystyle \neg {\text{človek}}(X)\lor {\text{smrtnik}}(X)}

to pomeni:

∀ X ( ¬ človek ( X ) ∨ smrtnik ( X ) ) {\displaystyle \forall X(\neg {\text{človek}}(X)\lor {\text{smrtnik}}(X))}

kar je logično ekvivalentno implikaciji:

∀ X ( človek ( X ) → smrtnik ( X ) ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).}

Vloga v avtomatiziranem dokazovanju in logičnem programiranju

Hornovi stavki igrajo ključno vlogo v konstrukcijski logiki in računski logiki. Njihova pomembna lastnost je ohranitev razreda pri resoluciji: resolvent dveh Hornovih stavkov je zopet Hornov stavek, resolvent ciljnega stavka in določenega stavka pa je ciljni stavek. Zaradi tega so postopki dokazovanja, ki temeljijo na resoluciji (zlasti SLD-razreševanje), učinkovitejši, kadar so dokazi predstavljeni s Hornovimi stavki. Uporablja se jih za predstavitev teorij, pravil in reševanje vprašanj (ciljev).

Hornovi stavki so tudi osnova logičnega programiranja. Določeni stavki se v tem kontekstu pogosto zapišejo v obliki implikacije:

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

Pri izvajanju logičnega programiranja in jezika Prolog se za izvajanje uporablja SLD-razrešitev (selective linear definite clause resolution). Razrešitev ciljnega stavka z določenim stavkom, da bi dobili nov ciljni stavek, je osnovni korak tega sklepanja.

V praksi se zato določni stavki pogosto pišejo v povratni (definicionalni) obliki, ki poudari njihovo vlogo kot postopkov za zmanjševanje ciljev:

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

V Prologu je to zabeleženo kot:

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

Ta zapis kaže, da je za dokaz u treba dokazati p, q, ..., t. Določeni stavki se tako obnašajo kot funkcije ali pravila, ki zmanjšujejo zahtevan cilj na podcilje — to imenujemo backward chaining (povratno sklepanje).

Opomba o kvantifikatorjih in dvoumnosti: v formalni semantiki so spremenljivke v pravilih univerzalno kvantificirane, medtem ko rezultati poizvedb (queries) pogosto predstavljajo eksistencialne dokaze. V jezikih kot je Prolog se tako formulacije smiselno bereo: pravila so splošna (za vse spremenljivke), poizvedbe pa iščejo obstoj instanc, ki izpolnjujejo pogoje. Poleg tega je pri negaciji v Prologu pogosto uporabljena tehnika "negation as failure" (negacija kot neuspeh), ki ni enaka klasični logični negaciji in zahteva previdno rabo (npr. stratificirana ali negacija z negacijskim pomenom).

Semantika: minimalni model in posledice

Van Emden in Kowalski (1976) sta preučila modelno-teoretične lastnosti Hornovih stavkov v kontekstu logičnega programiranja in pokazala, da ima vsaka množica določenih stavkov D edinstven minimalni model M (najmanjši model glede na vključevanje atomov). Atomska formula A je logično implicirana z D, če in samo če je A resnična v M. Iz tega sledi tudi, da je poizvedba P (predstavljena z eksistencialno kvantificirano konjunkcijo pozitivnih literalov) logično implicirana z D natanko tedaj, ko je P resnična v M. Ta minimalna-modelna semantika je temelj deklarativne semantike programov, sestavljenih iz Hornovih stavkov.

Računska zahtevnost in dokončnost

Propozicijske Hornove klavzule imajo ugodne računske lastnosti. Problem iskanja pripisa resničnostnih vrednosti, zaradi katerega je konjunkcija propozicijskih Hornovih klavzul resnična, je rešljiv v polinomskem času in dejansko v linear­nem času — ta problem se imenuje HORNSAT. To je v močni nasprotju s splošnim problemom boolske zadovoljivosti, ki je NP-poln.

Za prvi red pa velja, da je splošna zadovoljivost Hornovih stavkov (ko so dovoljeni funkcijski simboli) neodločljiva. Obstajajo pa uporabni in zanimivi omejeni primeri (npr. Datalog, kjer ni funkcijskih simbolov), ki so decidabilni in pogosto uporabljeni v bazičnih jezikih za poizvedbe oziroma v sistemih za logično programiranje in baze znanja.

Primer praktične uporabe v Prologu

Tukaj kratek primer, ki ponazarja delo z določenimi stavki in poizvedbami v Prologu:

Pravila (program):

parent(alice, bob).

parent(bob, charlie).

ancestor(X,Y) :- parent(X,Y).

ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y).

Poizvedba:

?- ancestor(alice, charlie).

SLD-razreševanje bo uporabilo pravilo za ancestor in facts o parent, da zaključi, da je poizvedba resnična. Ta primer ponazori, kako Hornovi stavki (dejstva in pravila) tvorijo osnovo deklarativnega programa, medtem ko SLD-razreševanje izvaja izvedbo (proceduralni pomen).

Zaključek

Hornovi stavki so preprost, a zelo uporaben razred logičnih stavkov, ki povezujejo teoretično logiko in praktično logično programiranje. Zaradi lastnosti, kot so ohranitev razreda pri resoluciji, obstoja enoličnega minimalnega modela in ugodnih računskih kompleksnostnih rezultatov (v propozicijski ravni), so osnova za jezike, kot je Prolog, in za mnoge metode avtomatiziranega sklepavanja ter obdelave znanja.

Vprašanja in odgovori

V: Kaj je klavzula o rogu?

V: Kdo jih je prvi opisal?

V: Kaj je določni stavek?

V: Kaj je dejstvo?

V: Kaj je ciljni stavek?

V: Kako delujejo spremenljivke v nepredložnih primerih?

Išči po črki