Horn-klóz

A Horn-záradék olyan irodalmi elemek logikai diszjunkciója, ahol az irodalmi elemek közül legfeljebb egy pozitív, az összes többi pedig negatív. Nevét Alfred Hornról kapta, aki 1951-ben egy cikkében írta le.

A pontosan egy pozitív literálissal rendelkező Horn-féle tagmondat határozott tagmondat; a negatív literálok nélküli határozott tagmondatot néha "ténynek" nevezik; a pozitív literál nélküli Horn-féle tagmondatot pedig néha céltagmondatnak nevezik. Ezt a háromféle Horn-mondatot a következő mondattani példa szemlélteti:

határozott névelő: ¬ 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$

fact: u {\displaystyle u} $u$

célzáradék: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\neg p\lor \neg q\vee \cdots \vee \neg t$

A nem-propozicionális esetben a mondatban lévő összes változó implicit módon univerzálisan kvantifikált, a teljes mondat hatókörével. Így például:

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

jelentése:

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

ami logikailag egyenértékű a következőkkel:

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

A Horn-tételek alapvető szerepet játszanak a konstruktív logikában és a számítási logikában. Fontosak az elsőrendű felbontással történő automatizált tételbizonyításban, mivel két Horn-tétel felbontója maga is Horn-tétel, egy céltétel és egy határozott tétel felbontója pedig egy céltétel. A Horn-tételek ezen tulajdonságai nagyobb hatékonyságot eredményezhetnek egy (a céltétel tagadásaként ábrázolt) tétel bizonyításában.

A Horn-klauzulák képezik a logikai programozás alapját is, ahol gyakori, hogy a határozott klauzulákat implikáció formájában írjuk:

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

Valójában egy céltételnek egy határozott tétellel való felbontása egy új céltétel előállítása érdekében az SLD felbontási következtetési szabály alapja, amelyet a logikai programozás és a Prolog programozási nyelv megvalósításához használnak.

A logikai programozásban a határozott záradék cél-redukciós eljárásként viselkedik. Például a fent leírt Horn-záradék a következő eljárásként viselkedik:

show u {\displaystyle u} $u$ , show p {\displaystyle p} $p$ és show q {\displaystyle q} és ⋯ {\displaystyle \cdots } $\cdots$ és show t {\displaystyle t} $t$

A záradéknak ezt a visszafelé történő használatát hangsúlyozandó, gyakran írják visszafelé alakban:

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

Prologban ez a következőképpen írható:

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

A Prolog jelölés valójában kétértelmű, és a "goal clause" kifejezést is néha kétértelműen használják. A célklauzulában szereplő változókat lehet univerzálisan vagy egzisztenciálisan kvantifikáltnak olvasni, és a "hamis" levezetése értelmezhető akár ellentmondás levezetéseként, akár a megoldandó probléma sikeres megoldásának levezetéseként.

Van Emden és Kowalski (1976) a Horn-klauzulák modellelméleti tulajdonságait vizsgálta a logikai programozás kontextusában, megmutatva, hogy minden D határozott klauzula-halmaznak van egy egyedi minimális modellje M. Egy A atomos formulát logikailag akkor és csak akkor implikál D, ha A igaz M-ben. Ebből következik, hogy egy P probléma, amelyet pozitív literálok egzisztenciálisan kvantifikált konjunkciója képvisel, logikailag akkor és csak akkor implikál D, ha P igaz M-ben. A Horn-klauzulák minimális modellszemantikája az alapja a logikai programok stabil modellszemantikájának.

A Horn-fogalmazások a számítási komplexitás szempontjából is érdekesek, ahol a Horn-fogalmazások konjunkcióját igazzá tevő igazságérték-kiosztások megtalálásának problémája egy P-teljes (valójában lineáris idő alatt megoldható) probléma, amelyet néha HORNSAT-nak neveznek. (A korlátlan Boolean kielégíthetőségi probléma azonban NP-teljes probléma.) Az elsőrendű Horn-feltételek kielégíthetősége eldönthetetlen.

Kérdések és válaszok

K: Mi az a kürtzáradék?

V: A Horn-záradék olyan literálok logikai diszjunkciója, ahol az literálok közül legfeljebb egy pozitív, az összes többi pedig negatív.

K: Ki írta le őket először?

V: Alfred Horn írta le őket először egy 1951-es cikkében.

K: Mi az a határozott záradék?

V: A Horn-féle, pontosan egy pozitív literált tartalmazó tagmondatot határozott tagmondatnak nevezzük.

K: Mi az a tény?

V: A negatív szóelemek nélküli határozott mondatot néha "ténynek" nevezik.

K: Mi az a céltagmondat?

V: A pozitív literál nélküli Horn-mondatot néha célmondatnak nevezik.

K: Hogyan működnek a változók a nem propozicionális esetekben?

V: A nem-propozicionális esetben a záradékban lévő összes változó implicit módon univerzálisan kvantifikált, a teljes záradék hatókörével. Ez azt jelenti, hogy a kijelentés minden részére vonatkoznak.

K: Milyen szerepet játszanak a Horn-féle klauzulák a konstruktív logikában és a számítási logikában? V: A Horn-klauzulák fontos szerepet játszanak az elsőrendű felbontással történő automatizált tételbizonyításban, mivel két Horn-klauzula vagy egy cél- és egy határozott klauzula közötti felbontás nagyobb hatékonyságot eredményezhet, amikor valaminek a célklauzula tagadásaként ábrázolt dolgot bizonyítunk. A logikai programozási nyelvek, például a Prolog alapjául is szolgálnak, ahol úgy viselkednek, mint a célredukciós eljárások.