Horno klauzulė: apibrėžimas, pavyzdžiai ir taikymas Prologe

Horno klauzulė: aiškus apibrėžimas, pavyzdžiai ir Prologo taikymai — konstruktyvioji logika, teoremų įrodymas ir loginis programavimas praktikams.

Autorius: Leandro Alegsa

28-12-2025 21:13

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 $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

faktas: u $u$

tikslo klauzulė: ¬p ∨ ¬q ∨ ⋯ ∨ ¬t $\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) $\neg {\text{human}}(X)\lor {\text{mortal}}(X)$

reiškia

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

kas logiškai atitinka implikaciją

∀X (žmogus(X) → mirtingas(X)) $\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 $(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) $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.

Klausimai ir atsakymai

Klausimas: Kas yra rago klaustukas?

A: Horno išlyga - tai loginė literalų disjunkcija, kai ne daugiau kaip vienas iš literalų yra teigiamas, o visi kiti - neigiami.

K: Kas pirmasis juos aprašė?

A: Alfredas Hornas pirmą kartą jas aprašė 1951 m. straipsnyje.

K: Kas yra apibrėžtoji išlyga?

A: Horno išlyga, kurioje yra lygiai vienas teigiamas literalas, vadinama apibrėžtąja išlyga.

K: Kas yra faktas?

A: Apibrėžtinis sakinys, neturintis neigiamų literatalų, kartais vadinamas "faktu".

K: Kas yra tikslo sąlyga?

A: Horno išlyga be teigiamo literalo kartais vadinama tikslo išlyga.

K: Kaip veikia kintamieji nepropoziciniais atvejais?

A: Nepropoziciniu atveju visi kintamieji sąlygoje yra netiesiogiai visuotinai kvantifikuojami, o jų taikymo sritis - visa sąlyga. Tai reiškia, kad jie taikomi kiekvienai teiginio daliai.

Klausimas: Kokį vaidmenį Horno sąlygos atlieka konstruktyviojoje logikoje ir skaičiavimo logikoje? A: Horno sąlygos vaidina svarbų vaidmenį automatizuotame teoremų įrodyme taikant pirmosios eilės rezoliuciją, nes dviejų Horno sąlygų arba tarp vienos tikslo ir vienos apibrėžtos sąlygos rezolventas gali būti naudojamas siekiant didesnio efektyvumo įrodant ką nors, kas pateikiama kaip tikslo sąlygos neiginys. Jos taip pat naudojamos kaip loginio programavimo kalbų, pavyzdžiui, Prologo, pagrindas, kur jos elgiasi kaip tikslų redukcijos procedūros.

Ieškoti