Horn-klóz
Horn-klóz a matematikai logikában, konkrétan a nulladrendű (vagy ítélet-) és az elsőrendű (vagy predikátum-) logikában olyan zárt klóz, azaz véges sok negálatlan vagy negált zárt atomi formulából (literálból) diszjunkció által összetett formula, mely legfeljebb egy negálatlan, azaz pozitív atomot tartalmaz; a többi tagja viszont negált.
Tehát egy Horn-klóz a következőképp fest:
ahol n∈ℕ (ideértve, hogy esetleg n=0), továbbá B1, B2, … , Bn zárt atomi formulák, és A pedig vagy szintén zárt atomi formula, vagy pedig az „üres klóz”. A Horn-klóz eszerint egy speciális alakú konjunktív normálforma.
Definit Horn-klóz olyan Horn-klóz, mely pontosan egy pozitív literált tartalmaz (tehát A nem „üres klóz/literál”). Lásd még definit programklóz.
A Horn-klózok fontos szerepet játszanak a logikai programozásban és a konstruktivista logikában, illetve a számításelméletben. A fogalom megalkotója Alfred Horn, aki 1951-es cikkében („On sentences which are true of direct unions of algebras”, Journal of Symbolic Logic, 16, 14-21.) először foglalkozott velük.
Definit programklóz[szerkesztés]
A definit programklóz a logikai programozás (elsősorban a Prolog programozási nyelv ) szakzsargonjában szereplő kifejezés, mely speciális alakú implikációs formulát jelent:
Felhasználva, hogy B→A ≡ ¬B∨A általánosan érvényes logikai törvény, továbbá az egyik De Morgan-szabályt, egyszerűen adódik, hogy a Horn-klózok éppen a definit programklózok; pontosabban ezekkel ekvivalensek. Ugyanis ekkor
Ez utóbbi szokás a következő formában is írni:
A :- jel bal oldalán szereplő A atom a formula feje, a jobb oldalon szereplő jelsorozat a klóz törzse; az utóbbiban szereplő Bi atomokat a klóz argumentumainak szokás nevezni; míg az A és B atomokat közösen literáloknak. A „definit” jelző arra utal, hogy a :- jel (tulajdonképp ez ugyanazt jelenti, mint a ← jel) bal oldalán egyetlen A atom szerepel, és így a definit klóz felfogható mint egy definíció, vagy annak részlete. Ellenben, ha több atom is szerepelne, azok a fenti levezetés alapján diszjunkcióval lennének elválasztva, és a formula nem azt jelentené, hogy „ha a B formulák igazak, akkor az A formula is”, hanem azt, hogy „ha a B formulák igazak, akkor az A formulák legalább egyike igaz”. Tehát ez esetben az A konklúzió diszjunkciós formula lenne (eredménye egy esetszétválasztás). Míg definit programklóz esetében a konklúzió egyértelműen (meghatározottan, definiáltan) egy adott atom, és nem tartalmaz választási lehetőséget.
Minthogy szemantikai szempontból a (definit) programklóz és a (definit) Horn-klóz majdnem ugyanaz a fogalom: tetszőleges definit programklóz a literálok sorrendjétől eltekintve egyértelműen definit Horn-klózzá írható át és viszont; ezért az informatikában a (definit) programklóz fogalmát teljes joggal szokás azonosítani a (definit) Horn-klózéval.
Számításelméleti vonatkozások[szerkesztés]
A SAT-probléma[szerkesztés]
A Kielégíthetőségi probléma (SAT-probléma) azt takarja, hogy adott F formula konjunktív normálforma (KNF) alakjáról megállapítható-e, hogy kielégíthető-e, azaz változóinak adható-e olyan igazságérték (interpretáció), melyben F igaz lesz? Jelenleg nem tudjuk, erre a feladatra adható-e egy polinomidőben befejeződő determinisztikus megoldási algoritmus (azaz fogalmunk sincs arról, hogy SAT∈P igaz-e); noha azt tudjuk, hogy a probléma (exponenciális időben) megoldható. Azonban egy változóinak adott igazságértékről polinomiális időben el tudjuk dönteni, hogy az valóban igazat ad ezért SAT∈NP.
A HORNSAT-probléma[szerkesztés]
A probléma egy könnyített alesete, a HORNSAT -probléma (melyben megköveteljük, hogy a KNF minden klóza legfeljebb egy pozitív literált tartalmazzon) viszont P-ben van, adható rá determinisztikus polinomidejű megoldóeljárás. A kezdeti, kísérleti jellegű logikai programozási nyelvekben nem Horn-logikát használtak, emiatt a programok idő- vagy nyelvi bonyolultság szempontjából gyakorta torkollottak kombinatorikus robbanásba. A Horn-logikára alapozó programokban ez már kevésbé fordul elő, noha más okok miatt ezek a programok is viselkedhetnek előnytelenül a gyakorlat szempontjából bizonyos szituációkban.
Egyéb[szerkesztés]
A logikai programozásban azonban nem kizárólag emiatt alkalmaznak Horn-klózokat, hanem azért, mert a legtöbb ilyen program a rezolúciós kalkulus szerint, mégpedig lineáris inputrezolúcióval végzi a formulák feldolgozását, és az inputrezolúció a Horn-klózokra bizonyítottan egy helyes és teljes kalkulus, míg tetszőleges elsőrendű formulákra alkalmazva nem az.
Hivatkozások[szerkesztés]
Külső hivatkozások[szerkesztés]
Irodalom[szerkesztés]
- Papadimitriou, Christos H.: Számítási bonyolultság (Computational complexity). Egyetemi tankönyv. Novadat Bt., 1999. ISBN 963-9056-20-0 .
- Pásztorné Varga Katalin – Várterész Magda: A matematikai logika alkalmazásszemléletű tárgyalása, Panem, Bp., 2003. ISBN 963-545-364-7
- Alfred Horn: On sentences which are true of direct unions of algebras”, Journal of Symbolic Logic, 16, 14-21., 1951.