Horn-klauzulák: definíció, tulajdonságok és szerep a logikai programozásban

Horn-klauzulák: világos definíció, kulcsfontosságú tulajdonságok és gyakorlati szerep a logikai programozásban — hatékony tételbizonyítás és automatizált következtetés.

A Horn-klauzula (vagy Horn-záradék) olyan logikai diszjunkció, amelyben a literálok között legfeljebb egy pozitív literál szerepel; az összes többi literál negatív. A név Alfred Horn nevéhez fűződik, aki 1951-ben írta le ezeket az állításokat.

Három fontos speciális esete van a Horn-klauzuláknak:

• határozott klauzula (definite clause): pontosan egy pozitív literált tartalmaz, például egy implikáció formájában (ha p és q igazak, akkor u igaz);
• tény (fact): nincs negatív literálja, tehát csak egy pozitív literál áll benne (például u);
• célklauzula (goal clause vagy néha üres fejű klauzula): nincs pozitív literálja, azaz csak negatív literálokból áll (ez a logikai üres fejű klauzula a levezetésben ellentmondás vagy cél reprezentációja lehet).

határozott klauzula: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

tény: u {\displaystyle u}

célklauzula: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}

A nem-propozicionális (elsőrendű) esetben a klauzulában szereplő változókat általában implicit módon univerzálisan kvantifikáljuk a teljes mondat hatókörével. Például a következő Horn-klauzula:

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

értelmezhető úgy, hogy

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

ami logikailag egyenértékű a következő implikációval:

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

Felbontás és következtetés

A Horn-klauzulák fontos algebrai tulajdonsággal rendelkeznek a felbontás (resolution) szempontjából: két Horn-klauzula felbontója ismét Horn-klauzula lesz. Különösen egy célklauzula és egy határozott klauzula felbontójaként újból célklauzula keletkezik. Ez a tulajdonság lehetővé teszi hatékonyabb tételbizonyítást és lekérdezés-végrehajtást a Horn-elképzelések esetén.

Ez alapján az SLD-felbontás (selective linear definite clause resolution) szabálya alapozza meg a logikai programozás következtetési mechanizmusát: egy céltétel (a kívánt állítás tagadása) és egy határozott klauzula felbontásával új célokat kapunk; ezt ismételve vagy ellentmondást találva dönthetjük el a bizonyíthatóságot.

Logikai programozás és Prolog

A Horn-klauzulák alkotják a logikai programozás formális alapját. Gyakran használjuk a határozott klauzulákat implikációként:

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

A Horn-klauzula procedurális szemlélete a célredukciós (backward chaining) mechanizmus: ha a fej u akkor igaz, ha a test p, q, …, t mind igaz. Emiatt gyakran írják a záradékot visszafelé irányuló szabályként:

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

Prologban ezt egyszerűen így írjuk:

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

A Prolog jelölésben a klauzulák és a célok változóit gyakran univerzális vagy egzisztenciális kvantifikálásként értelmezik a kontextustól függően: lekérdezésnél a megoldás keresése (sikeres levezetés) procedurális célként értelmezhető, míg a tételek bizonyítása klasszikus logikai ellentmondáskeresésként is felfogható.

Minimális modell és szemantika

Van Emden és Kowalski (1976) eredménye szerint minden véges (vagy általános) határozott klauzula-halmaznak létezik egy egyedi minimális (Herbrand) modellje M. Továbbá egy atomikus formula A logikai következménye a határozott klauzula-halmaznak D pontosan akkor, ha A igaz a minimális modellben M (D ⊨ A ⇔ M ⊨ A). Ennek következtében egy P probléma, amelyet pozitív literálok konjunkciója képvisel, logikailag akkor és csak akkor következik D-ből, ha P igaz M-ben.

Ez a minimális modellszemantika szolgál a logikai programok deklaratív szemantikájának alapjául, és fontos kapcsolódási pontot jelent más szemantikákkal, például a stabil modellszemantikával (különösen a normál programok és nemmonoton logikák vizsgálatakor).

Komplexitás és kielégíthetőség

A Horn-klauszulák kielégíthetőségi problémája (HORNSAT) nevezetes: a Horn-klauszulákból álló gegeben konjunkció kielégíthető érték-kiosztás megtalálása polinomiális időben, sőt lineáris időben megoldható, ezért HORNSAT P-teljesnek tekinthető a köznapi értelemben (az algoritmikus eljárások hatékonyak). Ez éles ellentétben áll az általános Boole-féle kielégíthetőségi problémával, amely NP-teljes.

Fontos azonban megjegyezni, hogy az elsőrendű Horn-feltételek kielégíthetőségének eldöntése általános esetben eldönthetetlen: az elsőrendű logika általános határozatlansága itt is érvényesül.

Gyakorlati megjegyzések és példák

Gyakorlati logikai programokban a Horn-klauzulákat gyakran használják tudásreprezentációra, szabályok és tények megadására, valamint lekérdezések végrehajtására. Egy egyszerű Prolog-példa:

apa(X) :- fiú(X), felnott(X).

fiú(janos).

felnott(janos).

Ebben a programban a szabály (határozott klauzula) azt mondja, hogy X apa, ha X fiú és X felnőtt. A tények (fact) megadják, hogy janos fiú és felnőtt, így a lekérdezés apa(janos)? sikeres lesz az SLD-felbontás segítségével.

Összefoglalva: a Horn-klauzulák egyszerre rendelkeznek kedvező elméleti tulajdonságokkal (lezártság felbontás alatt, minimális modell, hatékony kielégíthetőség) és gyakorlati jelentőséggel a logikai programozás és a Prolog megvalósításában.

Kérdések és válaszok

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

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

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

K: Mi az a tény?

K: Mi az a céltagmondat?

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

Keresés betűvel