Оговорка о роге - Horn clause
В математической логике и логическом программировании предложение Хорна - это логическая формула определенной формы, подобной правилу, которая дает ей полезные свойства для использования в логическом программировании, формальной спецификации и теории моделей . Предложения Хорна названы в честь логика Альфреда Хорна , который впервые указал на их значение в 1951 году.
Определение
Пункт рогом является пункт (а дизъюнкция из литералов ) с более чем одним положительным, т.е. unnegated , буквальным.
И наоборот, дизъюнкция литералов с одним отрицательным литералом называется предложением двойного рога .
Предложение Хорна с ровно одним положительным литералом является определенным предложением или строгим предложением Хорна ; определенное предложение без отрицательных литералов - это предложение unit , а предложение unit без переменных - это факт ;. Предложение Хорна без положительного литерала является целевым предложением . Обратите внимание, что пустое предложение, не содержащее литералов (что эквивалентно false ), является целевым предложением. Эти три вида предложений Хорна проиллюстрированы в следующем пропозициональном примере:
| Тип оговорки Рога | Форма дизъюнкции | Форма следствия | Читайте интуитивно как |
|---|---|---|---|
| Определенная оговорка | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u | u ← p ∧ q ∧ ... ∧ t | Предположу , что, если р и д и ... и т всего трюма, то и у имеют место |
| Факт | ты | u ← верно | Предположим, что u выполняется |
| Положение о цели | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t | ложь ← p ∧ q ∧ ... ∧ t | показать , что р и д и ... и т все держать |
Все переменные в предложении неявно универсально количественно оцениваются с охватом всего предложения. Так, например:
- ¬ человек ( X ) ∨ смертный ( X )
означает:
- ∀X (¬ человек ( X ) ∨ смертный ( X ))
что логически эквивалентно:
- ∀X ( человек ( X ) → смертный ( X ))
Значимость
Предложения Хорна играют основную роль в конструктивной логике и вычислительной логике . Они важны при автоматическом доказательстве теорем с помощью разрешения первого порядка , потому что резольвента двух предложений Хорна сама по себе является предложением Хорна, а резольвента предложения цели и определенного предложения является предложением цели. Эти свойства предложений Хорна могут повысить эффективность доказательства теоремы: целевое предложение - отрицание этой теоремы; см. пункт «Цель» в приведенной выше таблице. Интуитивно, если мы хотим доказать φ, мы предполагаем ¬φ (цель) и проверяем, приводит ли такое предположение к противоречию. Если это так, то φ должно выполняться. Таким образом, механический инструмент доказательства должен поддерживать только один набор формул (предположений), а не два набора (предположения и (под) цели).
Пропозициональные предложения Хорна также представляют интерес с точки зрения вычислительной сложности . Проблема нахождения присвоений истинностных значений, чтобы сделать конъюнкцию пропозициональных предложений Хорна истинными, известна как HORNSAT . Эта задача является P-полной и разрешима за линейное время . Обратите внимание, что проблема неограниченной булевой выполнимости является NP-полной проблемой.
Логическое программирование
Предложения Horn также являются основой логического программирования , где обычно пишут определенные предложения в форме импликации :
- ( p ∧ q ∧ ... ∧ t ) → u
Фактически, разрешение предложения цели с определенным предложением для создания нового предложения цели является основой правила вывода разрешения SLD , используемого в реализации языка логического программирования Prolog .
В логическом программировании определенное предложение ведет себя как процедура приведения к цели. Например, предложение Horn, написанное выше, ведет себя как процедура:
- чтобы показать u , показать p и показать q и ... и показать t .
Чтобы подчеркнуть обратное использование предложения, его часто пишут в обратной форме:
- u ← ( p ∧ q ∧ ... ∧ t )
В Прологе это записывается так:
u :- p, q, ..., t.
В логическом программировании вычисления и оценка запросов выполняются путем представления отрицания решаемой проблемы в виде целевого предложения. Например, проблема решения экзистенциально квантифицированной конъюнкции положительных литералов:
- ∃ X ( p ∧ q ∧ ... ∧ t )
представлен отрицанием проблемы (отрицанием того, что у нее есть решение) и представлением ее в логически эквивалентной форме предложения цели:
- ∀ X ( ложь ← p ∧ q ∧ ... ∧ t )
В Прологе это записывается так:
:- p, q, ..., t.
Решение проблемы сводится к получению противоречия, которое представлено пустым предложением (или «ложным»). Решение проблемы - замена переменных в целевом предложении терминами, которые можно извлечь из доказательства противоречия. При таком использовании целевые предложения аналогичны конъюнктивным запросам в реляционных базах данных, а логика предложения Хорна по вычислительной мощности эквивалентна универсальной машине Тьюринга .
Нотация Пролога на самом деле неоднозначна, и термин «целевое предложение» иногда также используется неоднозначно. Переменные в предложении цели могут быть прочитаны как универсально или экзистенциально количественно оцененные, а вывод «ложного» можно интерпретировать либо как вывод противоречия, либо как вывод успешного решения проблемы, которую необходимо решить.
Ван Эмден и Ковальский (1976) исследовали теоретико-модельные свойства Хорна в в контексте логического программирования, показывая , что каждый набор определенных ПОСТАНОВЛЕНИЯ D имеет единственную минимальную модель M . Атомная формула логически вытекает из D тогда и только тогда , когда истинно в М . Отсюда следует , что проблема Р представлена экзистенциально количественным сочетанием положительных литералов логически вытекает из D тогда и только тогда , когда Р истинно в М . Минимальная модельная семантика предложений Хорна является основой стабильной модельной семантики логических программ.