Хорнови клаузи: определение, примери и роля в логиката и Prolog

Клаузата на Хорн е логическа дизюнкция от литерали, в която най-много един от литералите е положителен, а всички останали са отрицателни. Наречена е на името на Алфред Хорн, който я описва в статия през 1951 г.

Клауза на Хорн с точно един положителен литерал е определена клауза; определена клауза без отрицателни литерали понякога се нарича "факт"; а клауза на Хорн без положителен литерал понякога се нарича клауза с цел. Тези три вида клаузи на Хорн са илюстрирани в следния пропозиционален пример:

определително изречение: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u}

факт: u {\displaystyle u}

клауза за цел: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t}

В непропозиционалния случай всички променливи в клаузата са имплицитно универсално квантифицирани с обхват цялата клауза. Така например:

¬ човек ( X ) ∨ смъртен ( X ) {\displaystyle \neg {\text{човек}}(X)\lor {\text{смъртен}}(X)}

означава:

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

което е логически еквивалентно на:

∀ X ( човек ( X ) → смъртен ( X ) ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). }

Клаузите на Хорн играят основна роля в конструктивната логика и изчислителната логика. Те са важни при автоматизираното доказване на теореми чрез разрешаване от първи ред, тъй като разрешаването на две клаузи на Хорн е само по себе си клауза на Хорн, а разрешаването на клауза на цел и определена клауза е клауза на цел. Тези свойства на клаузите на Хорн могат да доведат до по-голяма ефективност при доказването на теорема (представена като отрицание на клауза с цел).

Клаузите на Хорн са в основата и на логическото програмиране, където е обичайно да се записват определени клаузи под формата на импликация:

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

Всъщност разрешаването на целева клауза с определена клауза, за да се получи нова целева клауза, е в основата на правилото за разрешаване на SLD, използвано за реализиране на логическо програмиране и езика за програмиране Prolog.

В логическото програмиране определена клауза се държи като процедура за редукция на цели. Например клаузата Horn, написана по-горе, се държи като процедурата:

да покаже u {\displaystyle u} , да покаже p {\displaystyle p} и да покаже q {\displaystyle q} и ⋯ {\displaystyle \cdots } и show t {\displaystyle t} .

За да се подчертае тази обратна употреба на клаузата, тя често се пише в обратна форма:

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

На езика Prolog това се записва като:

Записът в Prolog всъщност е двусмислен, а терминът "целева клауза" също понякога се използва двусмислено. Променливите в една клауза за цел могат да се четат като универсално или екзистенциално квантифицирани, а извеждането на "false" може да се тълкува или като извеждане на противоречие, или като извеждане на успешно решение на решаваната задача.

Ван Емден и Ковалски (1976) изследват теоретичните свойства на моделите на клаузите на Хорн в контекста на логическото програмиране, като показват, че всяко множество от определени клаузи D има уникален минимален модел M. Атомна формула A е логически имплицирана от D тогава и само тогава, когато A е истинна в M. От това следва, че проблем P, представен чрез екзистенциално количествено определена конюнкция от положителни литерали, е логически имплициран от D тогава и само тогава, когато P е истинна в M. Семантиката на минималния модел на клаузите на Хорн е в основата на семантиката на стабилния модел на логическите програми.

Пропозиционалните клаузи на Хорн представляват интерес и в областта на изчислителната сложност, където проблемът за намиране на присвояване на истинностни стойности, които да направят конюнкцията от пропозиционални клаузи на Хорн вярна, е P-пълен проблем (всъщност решаем за линейно време), понякога наричан HORNSAT. (Проблемът за неограничената булева изпълнимост обаче е NP-пълен проблем.) Задоволимостта на клаузи от първи ред на Хорн е нерешима.

Синтаксис, видове и основни свойства

• Дефинитивна (definite) клауза — клауза с точно един положителен литерал, често записвана като импликация: (p ∧ q ∧ ... ∧ t) → u или u ← p, q, ..., t. Това е стандартната форма в логическото програмиране.
• Факт — определителна клауза без отрицателни литерали (само u). В Prolog: u.
• Клауза за цел (goal clause или query) — клауза без положителен литерал, т.е. дизюнкция само от отрицателни литерали (¬p ∨ ¬q ∨ ...), еквивалентна на конюнкция на цели p ∧ q ∧ ... за доказване.
• Затвореност под разрешаване — разрешаването (resolution) на две клаузи на Хорн води отново до клауза на Хорн. В частност, разрешението на клауза за цел с определителна клауза дава нова клауза за цел.
• Празната клауза (без литерали) се появява при доказване на противоречие; в контекста на целите това означава успех (доказахме заявката).

Семантика и образ на минимален модел

За множество от определени клаузи D съществува единствен минимален модел M (в смисъл на включване на множество от атоми), наричан най-малък Хербартов модел за D. Това означава, че дадена атомна формула A е логически следствие от D точно тогава, когато A е в M. Оперативно това се формализира чрез оператора за непосредствени последици T_P (имедиатният последствен оператор) — итеративно прилагане започващо от празното множество достига до най-малкия фиксиран модел (least fixpoint).

Оперативна семантика: насочено търсене и дърводържане

Клаузите на Хорн имат ясен оперативен прочит:

• Backward chaining (обратен ланец, използван в Prolog) — започва се от цел (заявка) и се опитва да я редуцира, като се прилагат правила (определени клаузи) за заместване на целите с по-подцели. Това е основата на SLD разрешаването и на изпълнението на Prolog програмите.
• Forward chaining (напреден ланец, даталог/инференция) — започва се от факти и правила и се извеждат нови факти последователно, докато не се достигне цел или фиксиран модел. Това е ефективен подход при пропозиционални Horn програми и при някои видове бази данни.

Пример в Prolog и стъпки на SLD-разрешаване

Елементарна Prolog програма:

• parent(a,b).
• parent(b,c).
• ancestor(X,Y) :- parent(X,Y).
• ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y).

Заявка: ?- ancestor(a,c).

Примерна SLD-стъпка: целта ancestor(a,c) се съпоставя с второто правило за ancestor, което води до подцели parent(a,Z) и ancestor(Z,c). parent(a,Z) се удовлетворява от факта parent(a,b) чрез унификация с Z=b, остава цел ancestor(b,c), която се удовлетворява с помощта на факта parent(b,c). Така заявката се доказва успешно.

Алгоритмична сложност и решаемост

• Пропозиционалният HORNSAT (задачата да се намери присвояване, което прави конюнкцията от пропозиционални Horn клаузи вярна) е в P и дори може да се решава за линейно време чрез алгоритъм на напредна интензификация (forward chaining / unit propagation). Затова HORNSAT често се използва като пример за голяма подкласа на SAT, която е полиномиално разрешима.
• Пълният проблем SAT (неограничена булева изпълнимост) е NP-пълен.
• Задоволимостта на клаузи от първи ред на Хорн (когато се позволят променливи и предикатни символи, без ограничение) е в общия случай нерешима.

Разширения, ограничения и приложения

• Ограничения: Horn клаузите не позволяват повече от един положителен литерал — това ги прави по-ограничени от общите булеви формули, но и по-ефективни за обработка.
• Негативна информация: в логическото програмиране често се използва "negation as failure" (негиране чрез неуспех), което е процедурно средство, но невинаги има класическа логическа семантика; за коректно поведение се въвеждат стратифицирани програми или по-сложни семантики като стабилни модели (stable model semantics).
• Datalog: подмножество на първо-редовите Horn програми без функции (термове) — използван широко в бази данни и системи за логическа заявка; изпълнението е гарантирано да приключи и сложността е по-добре контролирана.
• Приложения: логическо програмиране (Prolog), автоматизирано доказване на теореми, системи експертни системи, анализ на зависимости, системи типов контрол и разпознаване на цели в изкуствен интелект.

Теоретични подходи и семантики

Основни формални резултати:

• Ван Емден и Ковалски: свързват оперативната SLD-резолюция и семантиката на минималния модел. Те дефинират най-малкия модел чрез фиксирана точка на оператора T_P и показват коректност и пълнота на процедурите за определени програми спрямо тази семантика.
• За обработка на отрицание са разработени различни семантики: negation as failure (процедурна), семантика на стабилния модел (answer set programming) и well-founded semantics (добре-основна семантика), които обясняват поведението на програми с негирови предикати.

Кратко обобщение

• Клаузите на Хорн представляват важен синтактичен клас в логиката, с полезни алгори�мични и семантични свойства.
• Те са в основата на логическото програмиране и Prolog и позволяват ефективни механизми за извеждане (forward/backward chaining, SLD).
• Докато пропозиционалните Horn формули са ефективно разрешими, общият първо-редовен случай остава нерешим, а при добавяне на негиране е необходимо внимателно определяне на семантиката.

За по-нататъшно четене и исторически справки вижте споменатите източници и разработките на логическото програмиране и семантиките за програми с негативни предикати.

Въпроси и отговори

Въпрос: Какво представлява клаузата за рога?

В: Кой пръв ги е описал?

Въпрос: Какво е определена клауза?

В: Какво е факт?

Въпрос: Какво е клауза за цел?

Въпрос: Как работят променливите в случаите, които не са пропозиционални?

Търсене по буква