Клаузата на Хорн

Клаузата на Хорн е логическа дизюнкция от литерали, в която най-много един от литералите е положителен, а всички останали са отрицателни. Наречена е на името на Алфред Хорн, който я описва в статия през 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-пълен проблем.) Задоволимостта на клаузи от първи ред на Хорн е нерешима.

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

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

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

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

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

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

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

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