Roga klauzula

Roga klauzula ir literālu loģiskā disjunkcija, kurā ne vairāk kā viens no literāļiem ir pozitīvs, bet visi pārējie ir negatīvi. Tā ir nosaukta Alfrēda Horna vārdā, kurš to aprakstīja 1951. gada rakstā.

Roga klauzula ar tieši vienu pozitīvu literālu ir noteikta klauzula; noteikta klauzula bez negatīva literāla dažkārt tiek saukta par "faktu"; un Roga klauzula bez pozitīva literāla dažkārt tiek saukta par mērķa klauzulu. Šie trīs Horna klauzulu veidi ir ilustrēti nākamajā propozīcijas piemērā:

galīgais teikums: ¬ 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$

fakts: u {\displaystyle u} $u$

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

Nepropozicionālā gadījumā visi klauzulas mainīgie ir netieši universāli kvantificēti ar darbības jomu visā klauzulā. Tādējādi, piemēram:

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

apzīmē:

∀ X ( ¬ cilvēks ( X ) ∨ mirstīgais ( X ) ) {\displaystyle \forall X(\neg {\text{cilvēks}}(X)\lor {\text{mortāls}}(X))} $\forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))$

kas ir loģiski ekvivalents:

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

Roga klauzulām ir būtiska loma konstruktīvajā loģikā un skaitļošanas loģikā. Tās ir svarīgas automātiskajā teorēmu pierādīšanā ar pirmās kārtas atrisinājumu, jo divu Horna klauzulu atrisinājums pats par sevi ir Horna klauzula, bet mērķa klauzulas un noteiktas klauzulas atrisinājums ir mērķa klauzula. Šīs Horna klauzulu īpašības var nodrošināt lielāku teorēmas (ko attēlo kā mērķa klauzulas noliegumu) pierādīšanas efektivitāti.

Horna klauzulas ir arī loģiskās programmēšanas pamatā, kur ir ierasts rakstīt noteiktas klauzulas implikācijas formā:

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

Patiesībā mērķa klauzulas izšķiršana ar noteiktu klauzulu, lai iegūtu jaunu mērķa klauzulu, ir SLD izšķiršanas noteikuma pamatā, kas tiek izmantots loģiskās programmēšanas un programmēšanas valodas Prolog implementācijā.

Loģiskajā programmēšanā noteiktais teikums darbojas kā mērķa reducēšanas procedūra. Piemēram, iepriekš uzrakstītais Horna formulējums uzvedas kā procedūra:

parādīt u {\displaystyle u} $u$ , parādīt p {\displaystyle p} $p$ un parādīt q {\displaystyle q} un ⋯ {\displaystyle \cdots } $\cdots$ un show t {\displaystyle t} $t$ .

Lai uzsvērtu šo atkāpju lietojumu, to bieži raksta atkāpju formā:

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

Prologā tas tiek rakstīts šādi:

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

Prolog valodas apzīmējums patiesībā ir neviennozīmīgs, un arī termins "mērķa klauzula" dažkārt tiek lietots neviennozīmīgi. Mērķa klauzulas mainīgos var lasīt kā universāli vai eksistenciāli kvantificētus, un atvasinājumu "nepatiess" var interpretēt vai nu kā pretrunas atvasinājumu, vai kā risināmās problēmas veiksmīga risinājuma atvasinājumu.

Van Emdens un Kowalski (1976) pētīja Horna klauzulu modeļu teorijas īpašības loģiskās programmēšanas kontekstā, parādot, ka katrai noteiktu klauzulu kopai D ir unikāls minimālais modelis M. Atomārā formula A ir loģiski implicēta ar D tad un tikai tad, ja A ir patiesa M. No tā izriet, ka problēma P, ko attēlo pozitīvu literālu eksistenciāli kvantitatīvi noteikta konjunkcija, ir loģiski implicēta ar D tad un tikai tad, ja P ir patiesa M. Horna klauzulu minimālā modeļa semantika ir loģisko programmu stabilā modeļa semantikas pamatā.

Propozicionālās Horna klauzulas ir interesantas arī skaitļošanas sarežģītības jomā, kur problēma, kā atrast patiesības vērtību piešķīrumus, lai propozicionālo Horna klauzulu konjunkcija būtu patiesa, ir P-pilna problēma (faktiski atrisināma lineārā laikā), ko dažreiz sauc par HORNSAT. (Tomēr neierobežota Boolea apmierināmības problēma ir NP-kompleksa problēma.) Pirmās kārtas Horna klauzulu izpildāmība ir neizšķirama.

Jautājumi un atbildes

J: Kas ir raga klauzula?

A: Horna klauzula ir literālu loģiska disjunkcija, kur ne vairāk kā viens no literāļiem ir pozitīvs un visi pārējie ir negatīvi.

J: Kurš pirmais tos aprakstīja?

A: Alfrēds Horns pirmo reizi aprakstīja tās 1951. gada rakstā.

J: Kas ir galīgais teikums?

A: Horna klauzulu ar tieši vienu pozitīvu literālu sauc par noteiktu klauzulu.

J: Kas ir fakts?

A: Noteikto teikumu bez negatīviem literāļiem dažkārt sauc par "faktu".

J: Kas ir mērķa teikums?

A: Horna teikumu bez pozitīva literāļa dažkārt sauc par mērķa teikumu.

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

A: Nepropozicionālā gadījumā visi klauzulas mainīgie ir netieši vispārīgi kvantificēti ar darbības jomu visā klauzulā. Tas nozīmē, ka tie attiecas uz katru izteikuma daļu.

J: Kāda loma Horna klauzulām ir konstruktīvajā loģikā un skaitļošanas loģikā? A: Horna klauzulām ir svarīga loma automātiskajā teorēmu pierādīšanā ar pirmās kārtas atrisinājumu, jo divu Horna klauzulu vai starp vienu mērķa un vienu noteiktu klauzulu atrisinājumu var izmantot, lai radītu lielāku efektivitāti, pierādot kaut ko, kas attēlots kā mērķa klauzulas noliegums. Tos izmanto arī kā pamatu loģiskās programmēšanas valodās, piemēram, Prolog, kur tie darbojas kā mērķu reducēšanas procedūras.