В математической логике и логическом программировании предложение Хорна — это логическая формула особой формы, похожей на правило, которая придает ей полезные свойства для использования в логическом программировании, формальной спецификации , универсальной алгебре и теории моделей . Предложения Хорна названы в честь логика Альфреда Хорна , который впервые указал на их значение в 1951 году. [1]
Предложение Хорна — это дизъюнктивное предложение ( дизъюнкция литералов ) не более чем с одним положительным, то есть неотрицательным , литералом.
И наоборот, дизъюнкция литералов не более чем с одним отрицательным литералом называется предложением двойного Хорна .
Предложение Хорна, имеющее ровно один положительный литерал, является определенным предложением или строгим предложением Хорна ; [2] определенное предложение без отрицательных литералов является единичным предложением , [3] и единичное предложение без переменных является фактом ; [4] Предложение Хорна без положительного литерала является целевым предложением . Обратите внимание, что пустое предложение, не содержащее литералов (что эквивалентно false ), является целевым предложением. Эти три вида предложений Хорна иллюстрируются следующим пропозициональным примером:
Все переменные в предложении неявно имеют универсальную количественную оценку, при этом областью действия является все предложение. Так, например:
означает:
что логически эквивалентно:
Предложения Хорна играют основную роль в конструктивной логике и вычислительной логике . Они важны при автоматическом доказательстве теорем с помощью разрешения первого порядка , поскольку резольвента двух предложений Хорна сама по себе является предложением Хорна, а резольвента целевого предложения и определенного предложения является целевым предложением. Эти свойства предложений Хорна могут привести к большей эффективности доказательства теоремы: предложение цели является отрицанием этой теоремы; см. пункт «Цель» в таблице выше. Интуитивно, если мы хотим доказать φ, мы предполагаем ¬φ (цель) и проверяем, приводит ли такое предположение к противоречию. Если да, то φ должно выполняться. Таким образом, механическому инструменту доказательства необходимо поддерживать только один набор формул (предположений), а не два набора (предположений и (под)целей).
Пропозициональные предложения Хорна также представляют интерес с точки зрения вычислительной сложности . Проблема поиска присвоений истинностного значения, чтобы сделать конъюнкцию пропозициональных предложений Хорна истинной, известна как HORNSAT . Эта задача является P-полной и разрешима за линейное время . [6]
Обратите внимание, что проблема неограниченной булевой выполнимости является NP-полной задачей.
В универсальной алгебре определенные предложения Хорна обычно называются квазитождествами ; классы алгебр, определяемые набором квазитождеств, называются квазимногообразиями и обладают некоторыми хорошими свойствами более ограничительного понятия многообразия , т. е. эквационального класса. [7] С теоретико-модельной точки зрения предложения Хорна важны, поскольку они в точности (с точностью до логической эквивалентности) являются теми предложениями, которые сохраняются при редуцированных произведениях ; в частности, они сохраняются под прямыми произведениями . С другой стороны, существуют предложения, которые не являются хорновскими, но тем не менее сохраняются при произвольных прямых произведениях. [8]
Предложения Хорна также являются основой логического программирования , где принято записывать определенные предложения в форме импликации :
Фактически, разрешение предложения цели с определенным предложением для создания нового предложения цели является основой правила вывода разрешения SLD , используемого в реализации языка логического программирования Prolog .
В логическом программировании определенное предложение ведет себя как процедура сведения цели. Например, предложение Хорна, написанное выше, ведет себя как процедура:
Чтобы подчеркнуть обратное использование этого предложения, его часто пишут в обратной форме:
В Прологе это записывается так:
ю :- п , д , ..., т .В логическом программировании — предложение цели, имеющее логическую форму.
представляет собой отрицание проблемы, которую необходимо решить. Сама проблема представляет собой экзистенциально квантифицированное соединение положительных литералов:
Нотация Пролога не имеет явных кванторов и записывается в виде:
:- п , д , ..., т .Это обозначение неоднозначно в том смысле, что его можно читать либо как формулировку проблемы, либо как констатацию отрицания проблемы. Однако оба прочтения верны. В обоих случаях решение проблемы сводится к получению пустого предложения. В нотации Пролога это эквивалентно выводу:
:- истинный .Если предложение цели верхнего уровня читается как отрицание проблемы, то пустое предложение представляет собой ложь , а доказательство пустого предложения является опровержением отрицания проблемы. Если предложение цели верхнего уровня читается как сама проблема, то пустое предложение представляет true , а доказательство пустого предложения является доказательством того, что проблема имеет решение.
Решением проблемы является замена переменных X в предложении цели верхнего уровня, которую можно извлечь из доказательства резолюции. Используемые таким образом предложения целей аналогичны конъюнктивным запросам в реляционных базах данных , а логика предложений Хорна по вычислительной мощности эквивалентна универсальной машине Тьюринга .
Ван Эмден и Ковальски (1976) исследовали теоретико-модельные свойства предложений Хорна в контексте логического программирования, показав, что каждый набор определенных предложений D имеет уникальную минимальную модель M. Атомарная формула A логически подразумевается из D тогда и только тогда, когда A истинно в M. Отсюда следует, что проблема P, представленная экзистенциально квантифицированной конъюнкцией положительных литералов, логически подразумевается из D тогда и только тогда, когда P истинно в M . Минимальная модельная семантика предложений Хорна является основой стабильной модельной семантики логических программ. [9]