Přehled a základní definice

Hornova klauzule je speciální tvar klauzule v klasické logice používaný v teorii důkazů a v logickém programování. V propoziční nebo predikátové logice jde o disjunkci literálů s tím omezením, že nejvýše jeden literál je pozitivní (kladný), zatímco všechny ostatní, pokud existují, jsou negativní. Tento syntaktický tvar popsal Alfred Horn v roce 1951 a od té doby se Hornovy klauzule staly základním stavebním kamenem mnoha aplikací v informatice. Často se vyjadřují i ve formě implikace: konjunkce negativních literálů implikuje pozitivní literál, což odpovídá přepisování ¬p ∨ ¬q ∨ ... ∨ u jako (p ∧ q ∧ ...) → u. {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} disjunkce a formální přepis tedy tvoří centrální jazykový nástroj pro práci s těmito formulacemi. {\displaystyle u}

Typy Hornových klauzulí a příklady

Podle počtu pozitivních literálů rozlišujeme několik speciálních případů, které mají vlastní názvy a odlišné použití v praxi. Definitní věta (definite clause) obsahuje přesně jeden kladný literál a libovolný počet negativních literálů; když nejsou žádné negativní literály, klauzule je fakt (fact). Pokud naopak není žádný kladný literál, mluvíme o tzv. cílové (goal) nebo také odporující klauzuli, která se často používá při reprezentaci dotazů nebo negace tvrzení. Příklady zápisu v predikátové logice: ¬člověk(X) ∨ smrtelný(X) reprezentuje ∀X (člověk(X) → smrtelný(X)). {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} Také lze uvést formální implikativní zápis: (p ∧ q ∧ … ∧ t) → u, který přirozeně odpovídá způsobu, jakým se klauzule používají v logickém programování. {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}}(X)}

Role v predikátové logice a automatizovaném dokazování

Hornovy klauzule mají výhodné vlastnosti z hlediska rezoluce a konstrukce důkazů: rezolvent dvou Hornových klauzulí je opět Hornova klauzule, což zachovává tvar při aplikaci rezolvenčních pravidel. To vede k efektivnějším algoritmům pro dokazování, zejména pokud je cílem dokázat tvrzení reprezentované jako negace cílové klauzule. V kontextu prvního řádu se proměnné v klauzulích zpravidla považují za univerzálně kvantifikované; konkrétní interpretace proměnných a kvantifikátorů ovlivňuje způsob, jakým se výsledný důkaz chápe. Praktické mechanismy jako SLD-resoluce specializují rezoluci na práci s Hornovými klauzulemi a jsou základem vyhledávacích a odvozovacích strategií v implementacích logického programování. {\displaystyle \forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))}

Logické programování a Prolog

V paradigmatech logického programování se definiční Hornovy klauzule používají jako pravidla definující vztahy a procedury. Zápis pravidla se často obrací do tvaru hlava ← tělo a implementační jazyky jej zapisují v praktické notaci; v jazyce Prolog je například pravidlo u :- p, q, ..., t. Takový zápis interpretujeme procedurálně tak, že k dosažení cíle u systém zkouší postupně dosáhnout cílů p, q, …, t. Tento způsob „zpětného vyhledávání“ nebo redukce cílů je esencí vykonatelné semantics logických programů. Definiční klauzule tedy fungují současně jako logická tvrzení a jako instrukce pro vyhledávací stroj. {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).} {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u}

Modelová sémantika a výsledky Van Emden–Kowalski

V modelově teoretickém pojetí, které pro logické programování prozkoumali John van Emden a Maarten Kowalski, má každá množina definičních klauzulí jedinečný minimální model. To znamená, že existuje nejmenší struktura (model) vachotící všechny pravdivé atomické formule odvozené z těchto klauzulí. Důsledkem je silná věta: atomická formule A je logickým důsledkem množiny definičních klauzulí D právě tehdy, když A platí v tomto minimálním modelu. Tato minimální modelová sémantika poskytuje pevný základ pro interpretaci výsledků odvození a je východiskem pro další modely sémantik, včetně stabilní modelové sémantiky používané v programování s negací. {\displaystyle u} {\displaystyle p}

Výpočetní vlastnosti, složitost a praktické poznámky

Propoziční Hornovy formule mají příznivé výpočetní vlastnosti: problém rozhodnutí, zda existuje přiřazení pravdivostních hodnot splňující konjunkci Hornových klauzulí (tzv. HORNSAT), je rozhodnutelný v polynomiálním čase a v praxi řešitelný lineárně. To je výrazný kontrast s obecnou booleovskou splnitelností, která je NP-úplná, viz problematiku SAT. Na druhé straně, když povýšíme na Hornovy klauzule prvního řádu (s kvantifikátory a volnými funkcemi), obecný problém splnitelnosti se stává nerozhodnutelným. Z praktického hlediska to znamená, že omezení tvaru klauzulí přináší významné výhody pro efektivitu a jednodušší sémantickou interpretaci, což vysvětluje široké uplatnění Hornových klauzulí v programovacích jazycích a automatickém dokazování. Pro další čtení a související témata viz logické programování, Prolog a další informace. q {\displaystyle \cdots } {\displaystyle t} {\displaystyle u\leftarrow (p\land q\land \cdots \land t)}