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