Hornova klauzule: definice, vlastnosti a význam v logice a programování

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)). 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í.

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í.

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.

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í.

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.