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