Оговорка о роге

В математической логике и логическом программировании предложение Хорна — это логическая формула особой формы, похожей на правило, которая придает ей полезные свойства для использования в логическом программировании, формальной спецификации , универсальной алгебре и теории моделей . Предложения Хорна названы в честь логика Альфреда Хорна , который впервые указал на их значение в 1951 году.

Определение

Предложение Хорна — это дизъюнктивное ) с не более предложение (дизъюнкция литералов чем одним положительным, то есть неотрицательным , литералом.

И наоборот, дизъюнкция литералов не более чем с одним отрицательным литералом называется предложением двойного Хорна .

Предложение Хорна, имеющее ровно один положительный литерал, является определенным предложением или строгим предложением Хорна ; определенное предложение без отрицательных литералов является единичным предложением , и единичное предложение без переменных — это факт ; Предложение Хорна без положительного литерала является целевым предложением . Пустое предложение, не состоящее из литералов (что эквивалентно false ), является целевым предложением. Эти три вида предложений Хорна иллюстрируются следующим пропозициональным примером:

Тип предложения Хорна	Форма дизъюнкции	импликации Форма	Читать интуитивно, как
Определенное предложение	¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u	ты ← p ∧ q ∧ ... ∧ t	предположим, что, если все p и q и ... и t выполняются, то также u выполняется
Факт	в	ты ← правда	предположим, что ты держишь
Пункт о цели	¬ p ∨ ¬ q ∨ ... ∨ ¬ t	ложь ← p ∧ q ∧ ... ∧ t	покажи это p и q и ... и t все верно

Все переменные в предложении неявно имеют универсальную количественную оценку , при этом областью действия является все предложение. Так, например:

¬ человек ( X ) ∨ смертный ( X )

означает:

∀X( ¬ человек ( X ) ∨ смертный ( X ) ),

что логически эквивалентно:

∀X ( человек ( X ) → смертный ( X )).

Значение

Предложения Хорна играют основную роль в конструктивной логике и вычислительной логике . Они важны при автоматическом доказательстве теорем с помощью разрешения первого порядка , поскольку резольвента двух предложений Хорна сама по себе является предложением Хорна, а резольвента целевого предложения и определенного предложения является целевым предложением. Эти свойства предложений Хорна могут привести к большей эффективности доказательства теоремы: предложение цели является отрицанием этой теоремы; см. пункт «Цель» в таблице выше. Интуитивно, если мы хотим доказать φ, мы предполагаем ¬φ (цель) и проверяем, приводит ли такое предположение к противоречию. Если да, то φ должно выполняться. Таким образом, механическому инструменту доказательства необходимо поддерживать только один набор формул (предположений), а не два набора (предположений и (под)целей).

Пропозициональные предложения Хорна также представляют интерес с точки зрения вычислительной сложности . Проблема поиска присвоений истинностного значения, чтобы сделать конъюнкцию пропозициональных предложений Хорна истинной, известна как HORNSAT . Эта задача является P-полной и разрешима за линейное время . Напротив, неограниченная булева проблема выполнимости является NP-полной проблемой.

В универсальной алгебре определенные предложения Хорна обычно называются квазитождествами ; классы алгебр, определяемые набором квазитождеств называются квазимногообразиями и обладают некоторыми хорошими свойствами более ограничительного понятия многообразия , т. е. эквационального класса. С теоретико-модельной точки зрения предложения Хорна важны, поскольку они в точности (с точностью до логической эквивалентности) являются теми предложениями, которые сохраняются при редуцированных произведениях ; в частности, они сохраняются под прямыми произведениями . С другой стороны, существуют предложения, которые не являются хорновскими, но тем не менее сохраняются при произвольных прямых произведениях.

Логическое программирование

Предложения Хорна также являются основой логического программирования , где принято записывать определенные предложения в форме импликации :

( п ∧ q ∧ ... ∧ т ) → ты

Фактически, разрешение предложения цели с определенным предложением для создания нового предложения цели является основой правила вывода разрешения SLD , используемого в реализации языка логического программирования Prolog .

В логическом программировании определенное предложение ведет себя как процедура сведения цели. Например, предложение Хорна, написанное выше, ведет себя как процедура:

Чтобы показать тебе , покажи р , покажи q и... и покажи т .

Чтобы подчеркнуть обратное использование этого предложения, его часто пишут в обратной форме:

ты ← ( п ∧ q ∧ ... ∧ т )

В Прологе это записывается так:

u :- p, q, ..., t.

В логическом программировании — предложение цели, имеющее логическую форму.

∀ Икс ( ложь ← п ∧ q ∧ ... ∧ т )

представляет собой отрицание проблемы, которую необходимо решить. Сама проблема представляет собой экзистенциально определенное соединение положительных литералов:

∃ Икс ( п ∧ q ∧ ... ∧ т )

Нотация Пролога не имеет явных кванторов и записывается в виде:

:- p, q, ..., t.

Это обозначение неоднозначно в том смысле, что его можно читать либо как формулировку проблемы, либо как констатацию отрицания проблемы. Однако оба прочтения верны. В обоих случаях решение проблемы сводится к получению пустого предложения. В нотации Пролога это эквивалентно выводу:

:- true.

Если предложение цели верхнего уровня читается как отрицание проблемы, то пустое предложение представляет собой ложь , а доказательство пустого предложения является опровержением отрицания проблемы. Если предложение цели верхнего уровня читается как сама проблема, то пустое предложение представляет true , а доказательство пустого предложения является доказательством того, что проблема имеет решение.

Решением проблемы является замена переменных X в предложении цели верхнего уровня терминами, которые можно извлечь из доказательства резолюции. Используемые таким образом предложения целей аналогичны конъюнктивным запросам в реляционных базах данных , а логика предложений Хорна по вычислительной мощности эквивалентна универсальной машине Тьюринга .

Ван Эмден и Ковальски (1976) исследовали теоретико-модельные свойства предложений Хорна в контексте логического программирования, показав, что каждый набор определенных предложений имеет уникальную минимальную модель M. D Атомарная формула A логически подразумевается из D тогда и только тогда, когда истинно в M. A Отсюда следует, что проблема P, представленная экзистенциально квантифицированной конъюнкцией положительных литералов, логически подразумевается из D тогда и только тогда, когда P истинно в M . Минимальная модельная семантика предложений Хорна является основой стабильной модельной семантики логических программ.

См. также

• Пропозициональное исчисление

Ссылки

• Беррис, Стэнли; Санкаппанавар, HP, ред. (1981). Курс универсальной алгебры . Спрингер-Верлаг. ISBN  0-387-90578-2 .
• Басс, Сэмюэл Р. (1998). «Введение в теорию доказательств» . У Сэмюэля Р. Басса (ред.). Справочник по теории доказательств . Исследования по логике и основам математики. Том. 137. Эльзевир Б.В., стр. 1–78. дои : 10.1016/S0049-237X(98)80016-5 . ISBN  978-0-444-89840-1 . ISSN   0049-237X .
• Чанг, Чен Чунг ; Кейслер, Х. Джером (1990) [1973]. Теория моделей . Исследования по логике и основам математики (3-е изд.). Эльзевир. ISBN  978-0-444-88054-3 .
• Даулинг, Уильям Ф.; Галье, Жан Х. (1984). «Алгоритмы линейного времени для проверки выполнимости пропозициональных формул Хорна» . Журнал логического программирования . 1 (3): 267–284. дои : 10.1016/0743-1066(84)90014-1 .
• ван Эмден, Миннесота ; Ковальский, Р.А. (1976). «Семантика логики предикатов как языка программирования» (PDF) . Журнал АКМ . 23 (4): 733–742. CiteSeerX   10.1.1.64.9246 . дои : 10.1145/321978.321991 . S2CID   11048276 .
• Хорн, Альфред (1951). «О предложениях, истинных для прямых объединений алгебр». Журнал символической логики . 16 (1): 14–21. дои : 10.2307/2268661 . JSTOR   2268661 . S2CID   42534337 .
• Лау, Кунг-Киу; Орнаги, Марио (2004). «Указание композиционных единиц для правильной разработки программ в вычислительной логике». Разработка программ по вычислительной логике . Конспекты лекций по информатике. Том. 3049. стр. 1–29. дои : 10.1007/978-3-540-25951-0_1 . ISBN  978-3-540-22152-4 .
• Маковский, Дж. А. (1987). «Почему формулы Хорна имеют значение в информатике: исходные структуры и общие примеры» (PDF) . Журнал компьютерных и системных наук . 34 (2–3): 266–292. дои : 10.1016/0022-0000(87)90027-4 .