Hornov stavek

Hornov stavek je logična disjunkcija literalov, kjer je največ en literal pozitiven, vsi ostali pa so negativni. Poimenovana je po Alfredu Hornu, ki jo je opisal v članku leta 1951.

Hornov stavek s točno enim pozitivnim literalom je določni stavek; določni stavek brez negativnih literalov se včasih imenuje "dejstvo"; Hornov stavek brez pozitivnega literala pa se včasih imenuje ciljni stavek. Te tri vrste Hornovih stavkov so ponazorjene v naslednjem propozicionalnem primeru:

določni stavek: ¬ 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$

dejstvo: u {\displaystyle u} $u$

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

V nepropozicijskem primeru so vse spremenljivke v stavku implicitno univerzalno kvantificirane z obsegom celotnega stavka. Tako je na primer:

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

pomeni:

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

kar je logično enakovredno:

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

Hornovi stavki imajo osnovno vlogo v konstruktivni logiki in računski logiki. Pomembni so pri avtomatiziranem dokazovanju izrekov z reševanjem prvega reda, saj je resolvent dveh Hornovih stavkov sam Hornov stavek, resolvent ciljnega stavka in določenega stavka pa je ciljni stavek. Te lastnosti Hornovih stavkov lahko vodijo do večje učinkovitosti pri dokazovanju teoremov (predstavljenih kot negacija ciljnega stavka).

Hornovi stavki so tudi osnova logičnega programiranja, v katerem se določeni stavki običajno zapišejo v obliki implikacije:

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

Pravzaprav je razrešitev ciljnega stavka z določenim stavkom, da bi dobili nov ciljni stavek, osnova pravila za sklepanje o razrešitvi SLD, ki se uporablja za izvajanje logičnega programiranja in programskega jezika Prolog.

V logičnem programiranju se določni stavek obnaša kot postopek redukcije ciljev. Na primer, zgoraj zapisana klavzula Horn se obnaša kot postopek:

prikazati u {\displaystyle u} $u$ , prikazati p {\displaystyle p} $p$ in prikazati q {\displaystyle q} ter ⋯ {\displaystyle \cdots } $\cdots$ in show t {\displaystyle t} $t$ .

Da bi poudarili to povratno rabo stavka, ga pogosto pišemo v povratni obliki:

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

V prologu je to zapisano kot:

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

Zapis v Prologu je pravzaprav dvoumen in tudi izraz "ciljni stavek" se včasih uporablja dvoumno. Spremenljivke v ciljnem stavku se lahko berejo kot univerzalno ali eksistencialno kvantificirane, izpeljavo "false" pa je mogoče razlagati kot izpeljavo protislovja ali kot izpeljavo uspešne rešitve problema, ki ga je treba rešiti.

Van Emden in Kowalski (1976) sta raziskala modelnoteoretične lastnosti Hornovih stavkov v kontekstu logičnega programiranja in pokazala, da ima vsaka množica določenih stavkov D edinstven minimalni model M. Atomska formula A je logično implicirana z D, če in samo če je A resnična v M. Iz tega sledi, da je problem P, predstavljen z eksistencialno kvantificirano konjunkturo pozitivnih literalov, logično impliciran z D, če in samo če je P resničen v M. Minimalna modelna semantika Hornovih stavkov je podlaga za stabilno modelno semantiko logičnih programov.

Propozicijske Hornove klavzule so zanimive tudi na področju računske zahtevnosti, kjer je problem iskanja pripisov resničnostnih vrednosti, da je konjunkcija propozicijskih Hornovih klavzul resnična, popoln problem P (dejansko rešljiv v linearnem času), včasih imenovan HORNSAT. (Problem neomejene boolske zadovoljivosti pa je NP-poln problem.) Zadovoljivost Hornovih stavkov prvega reda je neodločljiva.

Vprašanja in odgovori

V: Kaj je klavzula o rogu?

O: Hornov stavek je logična disjunkcija literalov, kjer je največ en literal pozitiven, vsi drugi pa negativni.

V: Kdo jih je prvi opisal?

O: Alfred Horn jih je prvič opisal v članku leta 1951.

V: Kaj je določni stavek?

O: Hornov stavek s točno enim pozitivnim literalom se imenuje končni stavek.

V: Kaj je dejstvo?

O: Določni stavek brez negativnih literalov se včasih imenuje "dejstvo".

V: Kaj je ciljni stavek?

O: Hornov stavek brez pozitivnega literala se včasih imenuje ciljni stavek.

V: Kako delujejo spremenljivke v nepredložnih primerih?

O: V nepropozicijskem primeru so vse spremenljivke v stavku implicitno univerzalno kvantificirane z obsegom celotnega stavka. To pomeni, da veljajo za vsak del izjave.

V: Kakšno vlogo imajo Hornovi stavki v konstruktivni logiki in računski logiki? O: Hornovi stavki imajo pomembno vlogo pri avtomatiziranem dokazovanju izrekov s pomočjo resolucije prvega reda, saj se lahko resolucija med dvema Hornovima stavkoma ali med enim ciljnim in enim določenim stavkom uporabi za večjo učinkovitost pri dokazovanju nečesa, kar je predstavljeno kot negacija njegovega ciljnega stavka. Uporabljajo se tudi kot osnova za logične programske jezike, kot je prolog, kjer se obnašajo kot postopki redukcije ciljev.