Horņa klauzula — definīcija, veidi un nozīme loģikā un Prologā

Horņa klauzula — skaidra definīcija, veidi un nozīme loģikā un Prologā. Uzzini par noteiktām, mērķa un fakta klauzulām, SLD izšķiršanu un pielietojumu automātiskajā pierādīšanā.

Horna klauzula ir literālu disjunkcija, kurā ne vairāk kā viens literāls ir pozitīvs, bet visi pārējie ir negatīvi. Nosaukums cēlies no Alfrēda Horna, kurš šo klauzulu klasi izpētīja 1951. gada rakstā. Horna klauzulas ir īpaši ērti lietojamas gan teoretiskajā loģikā, gan praktiskajā loģiskajā programmēšanā.

Veidi un piemēri

Izšķir trīs bieži izmantotus Horna klauzulu paveidus:

• Noteiktā (definite) klauzula — satur tieši vienu pozitīvu literālu un jebkādu skaitu negatīvu literālu. To parasti raksta implikācijas formā (sk. zemāk).
• Fakts — noteikta klauzula bez negatīviem literāliem (tātad satur tikai vienu pozitīvu literālu).
• Mērķa (goal, query) klauzula — Horna klauzula bez pozitīva literāla (tātad tikai negatīvi literāli); loģiskajā programmēšanā šo interpretē kā pieprasījumu vai noliegumu, kuru jāatrisina.

Piemēros ar propozicionālajām formām šie trīs veidi var tikt ilustrēti šādi:

Horna klauzula (ar vienu pozitīvu literālu): ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

Fakts: u {\displaystyle u}

Mērķa klauzula: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}

Horna klauzulas pirmajā kārtā

Nepropozicionālā (pirmās kārtas) gadījumā mainīgie klauzulā tiek saprasti kā netieši universāli kvantificēti pār visu klauzulas darbības jomu. Piemēram:

¬ cilvēks ( X ) ∨ mirstīgais ( X ) {\displaystyle \neg {\text{cilvēks}}(X)\lor {\text{mirstīgais}}(X)}

Šī klauzula nozīmē:

∀ X ( ¬ cilvēks ( X ) ∨ mirstīgais ( X ) ) {\displaystyle \forall X(\neg {\text{cilvēks}}(X)\lor {\text{mirstīgais}}(X))}

ko var pārrakstīt ekvivalentā implikācijas formā:

∀ X ( cilvēks ( X ) → mirstīgais ( X ) ) . {\displaystyle \forall X({\text{cilvēks}}(X)\rightarrow {\text{mirstīgais}}(X)).}

Horna klauzulu loma loģikā un automātiskajā pierādīšanā

Horna klauzulām ir būtiska vieta konstrukciju loģikā un skaitļošanas loģikā. Viens no svarīgiem iemesliem ir tāds, ka atrisināšana (resolution) saglabā Horna klauzulu klasi: divu Horna klauzulu atrisinājums atkal ir Horna klauzula, un, īpaši, mērķa klauzulas un noteiktas klauzulas atrisinājums dod mērķa klauzulu. Šī īpašība ļauj veidot efektīvas pierādīšanas procedūras, jo nolieguma formā izteiktos teikumus (mērķa klauzulas) var soli pa solim reducēt, piemērojot noteiktās klauzulas.

Horna klauzulas un loģiskā programmēšana (Prolog)

Horna klauzulas ir loģiskās programmēšanas pamatā, jo noteiktas klauzulas viegli interpretēt kā implikācijas, kas apraksta procedūras vai noteikumus. Noteiktu klauzulu parasti pieraksta formā:

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

Programmēšanas valodā Prolog to raksta kā:
u :- p, q, ..., t.

Šo klauzulu var saprast arī procedurāli: lai pierādītu u, nepieciešams pierādīt p, q, …, t. Mērķa klauzulas (vaicājumi) tiek risinātas samazināšanas (goal-reduction) metodes ceļā, un tieši no šīs idejas izriet SLD (Selective Linear Definite clause) izšķiršanas process, ko izmanto Prolog izpildītāji.

Vēl jāpiebilst, ka terminoloģija nav pilnīgi viennozīmīga: mērķa klauzulas mainīgos reizēm interpretē kā universāli vai eksistenciāli kvantificētus, un atvasinājumu "nepatiess" var skatīt kā pretrunas atvasinājumu vai kā risinājuma atrašanu vaicājumam.

Semantika: minimālais modelis un Herbrand semantika

Van Emden un Kowalski (1976) analizēja Horna klauzulu modeļu teoriju loģiskās programmēšanas kontekstā, parādot, ka katrai noteiktu klauzulu kopai D pastāv unikāls minimālais modelis M (bieži saprotams kā mazākais Herbranda modelis). Atomārā formula A ir loģiski implicēta ar D tieši tad, ja A ir patiesa M. No tā seko, ka problēma P, ko attēlo pozītīvu literālu eksistenciāli kvantificēta noteiktu klauzulu konjunkcija (t.i., vaicājums par atomu patiesumu), ir loģiski implicēta ar D tad un tikai tad, ja P ir patiesa M. Šī minimālā modeļa semantika ir pamatā stabilajām semantikām un citiem loģisko programmu semantikas modeļiem.

Sarežģītība un izpildāmība

Propozicionālo Horna klauzulu apmierināmības problēma (atrod piemērotu patiesības piešķīrumu, lai visa Horna klauzulu konjunkcija būtu patiess) ir P-pilna problēma, bieži dēvēta par HORNSAT; praktiski to var atrisināt lineārā laikā. Tas atšķiras no vispārīgās Boolea apmierināmības problēmas, kas ir NP-kompleksa. Savukārt pirmās kārtas Horna klauzulu izpildāmība (satura apmierināmība, meklējot modeļus ar mainīgajiem un rekurencēm) parasti ir neizšķirama.

Kopsavilkums

• Horna klauzulas — klauzulu klase ar ne vairāk kā vienu pozitīvu literālu — ir centrāla gan teorētiskajā loģikā, gan loģiskajā programmēšanā.
• Tās ļauj ērtu un efektīvu automātiskās dedukcijas īstenošanu (piem., SLD izšķiršana Prologā) un nodrošina vienkāršāku semantiku (minimālais modelis).
• Propozicionālā HORNSAT ir polinomāla (P-pilna), bet pirmās kārtas izpildāmība var būt neizšķirama.

Ja nepieciešams, varu pievienot īsu Prolog piemēru ar konkrētiem faktiem un noteikumiem, demonstrējot, kā SLD izšķiršana operē praksē.

Jautājumi un atbildes

J: Kas ir raga klauzula?

J: Kurš pirmais tos aprakstīja?

J: Kas ir galīgais teikums?

J: Kas ir fakts?

J: Kas ir mērķa teikums?

J: Kā darbojas mainīgie nepropozicionālos gadījumos?

Meklēt pēc burta