Horno klauzulė — tai loginė literalių disjunkcija, kurioje yra ne daugiau kaip vienas teigiamas literalis, o visi kiti literaliai yra neigiami. Šį klauzulės tipą aprašė Alfredas Hornas 1951 m., todėl ji gavo jo vardą.

Rūšys ir pavyzdžiai

Yra trys dažniausiai minima Horno klauzulės rūšys:

  • apibrėžtoji klauzulė (definite clause) — turi tik vieną teigiamą literalą ir vieną arba kelis neigiamus literalius;
  • faktas — tai apibrėžtoji klauzulė be neigiamų literalų (t. y. tik vienas teigiamas literalas);
  • tikslo (goal) klauzulė — Horno klauzulė be teigiamų literalių (t. y. tik neigiami literaliai).

Šias tris rūšis iliustruoja įprastas propozicinis pavyzdys:

apibrėžtoji klauzulė: ¬p ∨ ¬q ∨ ⋯ ∨ ¬t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

faktas: u {\displaystyle u}

tikslo klauzulė: ¬p ∨ ¬q ∨ ⋯ ∨ ¬t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}

Pirmos eilės Horno klauzulės ir kvantifikacija

Pirmos eilės (predikatinės) Horno klauzulės leidžia kintamuosius. Pagal įprastą konvenciją visi klauzulės kintamieji laikomi implicitinai (netiesiogiai) visuotinai kvantifikuotais ir jie galioja visai klauzulei. Pavyzdžiui, klauzulė

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

reiškia

∀X (¬žmogus(X) ∨ mirtingas(X)) {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))}

kas logiškai atitinka implikaciją

∀X (žmogus(X) → mirtingas(X)) {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).}

Horno klauzulės automatiniame įrodinėjime ir loginiame programavime

Horno klauzulės turi svarbių savybių automatizuotame teoremų įrodyme. Rezolventas (rezoliucijos rezultatas) dviejų Horno klauzulų yra vėl Horno klauzulė; be to, rezolventas tarp tikslo klauzulės (be teigiamų literalių) ir apibrėžtos klauzulės yra vėl tikslo klauzulė. Dėl šių savybių galima išvystyti efektyvius įrodymo mechanizmus, pvz., SLD-rezoliuciją, kuri yra pagrindas daugeliui loginių programavimo metodų.

Horno klauzulės yra ir loginio programavimo pagrindas. Apibrėžtąsias klauzules įprasta rašyti implikacijos forma:

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

Tokiai klauzulei atitinka įrašas atvirkštine forma, parodantis procedūrinį jos semantiką:

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

Prologe tai užrašoma taip:

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

Tokiu atveju apibrėžtoji klauzulė funkcionaliai veikia kaip procedūra, kuri sumažina tikslą (goal) u į subtikslų seka p, q, …, t. Išvedimas "false" Prologe (pvz., kai tikslas yra paneigiamas) gali būti aiškinamas tiek kaip prieštaravimo išvedimas, tiek kaip sėkmingas sprendžiamo uždavinio sprendimas — priklausomai nuo konteksto ir naudojamo formalizmo.

Semantika: minimalus modelis ir Van Emden–Kowalski teorema

Van Emdenas ir Kowalskis (1976) nagrinėjo Horno klauzulų semantiką loginio programavimo kontekste ir parodė svarbų rezultatą: kiekviena apibrėžtųjų klauzulų aibė D turi vienintelį minimalų (least) modelį M (paprastai Herbrando modelio prasme). Atominė formulė A yra logiškai implikuojama iš D tada ir tik tada, kai A yra teisinga šiame minimaliame modelyje M. Analogiškai, egzistenciškai kiekybiškai išreikšta teigiamų literalių konjunkcija P yra logiškai implikuojama iš D tada ir tik tada, kai P tenkinama modelyje M.

Ši minimalaus modelio semantika sudaro pagrindą kitiems loginių programų semantikos požiūriams, įskaitant stabilųjį modelį ir vėlesnius semantikos plėtojimus.

Skaičiavimo sudėtingumas

Propozicinės Horno klauzulės turi palankų algoritmo sudėtingumą: sprendinys, ieškant priskyrimų, kad propozicinė Horno formulė būtų tenkinama (HORNSAT), yra išsprendžiamas polinomiškai — tiesiškai laiku. Dėl to HORNSAT priklauso klases P. Tuo tarpu bendroji (neapribota) loginio patenkinamumo problema yra NP‑užbaigta.

Pirmos eilės Horno klauzulės problemos (pvz., bendro įrodomumo klausimas) gali būti neišsprendžiamos (nealgoritmiškai sprendžiamos) ir priklauso nuo naudojamo formalizmo bei apribojimų (pvz., ar leidžiami funktoriai su neribota gylio rekursija ir kt.).

Santrauka

Horno klauzulės — tai griežtai struktūruotos literalių disjunkcijos, kurias ypač patogu naudoti tiek automatiniame įrodinėjime, tiek loginiame programavime. Dėl jų savybių (rezolventas lieka Horno klauzulė, egzistuoja minimalus modelis ir pan.) galima sukurti efektyvias išvedimo strategijas, kurias praktiškai įgyvendina tokios kalbos kaip Prolog.