Оговорка о роге
В математической логике и логическом программировании предложение Хорна — это логическая формула особой формы, похожей на правило, которая придает ей полезные свойства для использования в логическом программировании, формальной спецификации , универсальной алгебре и теории моделей . Предложения Хорна названы в честь логика Альфреда Хорна , который впервые указал на их значение в 1951 году. [1]
Определение [ править ]
Предложение Хорна — это дизъюнктивное предложение ( дизъюнкция литералов неотрицательным ) не более чем с одним положительным, то есть , литералом.
И наоборот, дизъюнкция литералов не более чем с одним отрицательным литералом называется предложением двойного Хорна .
Предложение Хорна, имеющее ровно один положительный литерал, является определенным предложением или строгим предложением Хорна ; [2] определенное предложение без отрицательных литералов является единичным предложением , [3] и единичное предложение без переменных — это факт ; [4] Предложение Хорна без положительного литерала является целевым предложением . Пустое предложение, не содержащее литералов (что эквивалентно false ), является целевым предложением. Эти три вида предложений Хорна иллюстрируются следующим пропозициональным примером:
| Тип предложения Хорна | Форма дизъюнкции | импликации Форма | Читать интуитивно, как |
|---|---|---|---|
| Определенное предложение | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u | ты ← p ∧ q ∧ ... ∧ t | Предположим, что, если все p и q и... и t верны, то и u тоже верно |
| Факт | в | ты ← правда | Предположим, что ты держишь |
| Пункт о цели | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t | ложь ← p ∧ q ∧ ... ∧ t | покажи то p и q и ... и t все верно [5] |
Все переменные в предложении неявно имеют универсальную количественную оценку, при этом областью действия является все предложение. Так, например:
- ¬ человек ( X ) ∨ смертный ( X )
означает:
- ∀X( ¬ человек ( X ) ∨ смертный ( X ) ),
что логически эквивалентно:
- ∀X ( человек ( X ) → смертный ( X )).
Значение [ править ]
Предложения Хорна играют основную роль в конструктивной логике и вычислительной логике . Они важны при автоматическом доказательстве теорем с помощью разрешения первого порядка , поскольку резольвента двух предложений Хорна сама по себе является предложением Хорна, а резольвента целевого предложения и определенного предложения является целевым предложением. Эти свойства предложений Хорна могут привести к большей эффективности доказательства теоремы: предложение цели является отрицанием этой теоремы; см. пункт «Цель» в таблице выше. Интуитивно, если мы хотим доказать φ, мы предполагаем ¬φ (цель) и проверяем, приводит ли такое предположение к противоречию. Если да, то φ должно выполняться. Таким образом, механическому инструменту доказательства необходимо поддерживать только один набор формул (предположений), а не два набора (предположений и (под)целей).
Пропозициональные предложения Хорна также представляют интерес с точки зрения вычислительной сложности . Проблема поиска присвоений истинностного значения, чтобы сделать конъюнкцию пропозициональных предложений Хорна истинной, известна как HORNSAT . Эта задача является P-полной и разрешима за линейное время . [6] Напротив, проблема неограниченной булевой выполнимости является NP-полной проблемой.
В универсальной алгебре определенные предложения Хорна обычно называются квазитождествами ; классы алгебр, определяемые набором квазитождеств называются квазимногообразиями и обладают некоторыми хорошими свойствами более ограничительного понятия многообразия , т. е. эквационального класса. [7] С теоретико-модельной точки зрения предложения Хорна важны, поскольку они в точности (с точностью до логической эквивалентности) являются теми предложениями, которые сохраняются при редуцированных произведениях ; в частности, они сохраняются под прямыми произведениями . С другой стороны, существуют предложения, которые не являются хорновскими, но тем не менее сохраняются при произвольных прямых произведениях. [8]
Логическое программирование [ править ]
Предложения Хорна также являются основой логического программирования , где принято записывать определенные предложения в форме импликации :
- ( п ∧ q ∧ ... ∧ т ) → ты
Фактически, разрешение предложения цели с определенным предложением для создания нового предложения цели является основой правила вывода разрешения SLD , используемого в реализации языка логического программирования Prolog .
В логическом программировании определенное предложение ведет себя как процедура сведения цели. Например, предложение Хорна, написанное выше, ведет себя как процедура:
- Чтобы показать тебе , покажи р , покажи q и... и покажи т .
Чтобы подчеркнуть обратное использование этого предложения, его часто пишут в обратной форме:
- ты ← ( п ∧ q ∧ ... ∧ т )
В Прологе это записывается так:
ю :- п , д , ..., т .
В логическом программировании — предложение цели, имеющее логическую форму.
- ∀ Икс ( ложь ← п ∧ q ∧ ... ∧ т )
представляет собой отрицание проблемы, которую необходимо решить. Сама проблема представляет собой экзистенциально определенное соединение положительных литералов:
- ∃ Икс ( п ∧ q ∧ ... ∧ т )
Нотация Пролога не имеет явных кванторов и записывается в виде:
:- п , д , ..., т .
Это обозначение неоднозначно в том смысле, что его можно читать либо как формулировку проблемы, либо как констатацию отрицания проблемы. Однако оба прочтения верны. В обоих случаях решение проблемы сводится к получению пустого предложения. В нотации Пролога это эквивалентно выводу:
:- истинный .
Если предложение цели верхнего уровня читается как отрицание проблемы, то пустое предложение представляет собой ложь , а доказательство пустого предложения является опровержением отрицания проблемы. Если предложение цели верхнего уровня читается как сама проблема, то пустое предложение представляет true , а доказательство пустого предложения является доказательством того, что проблема имеет решение.
Решением проблемы является замена переменных X в предложении цели верхнего уровня, которую можно извлечь из доказательства резолюции. Используемые таким образом предложения целей аналогичны конъюнктивным запросам в реляционных базах данных , а логика предложений Хорна по вычислительной мощности эквивалентна универсальной машине Тьюринга .
Ван Эмден и Ковальски (1976) исследовали теоретико-модельные свойства предложений Хорна в контексте логического программирования, показав, что каждый набор определенных предложений имеет уникальную минимальную модель M. D Атомарная формула A логически подразумевается из D тогда и только тогда, когда истинно в M. A Отсюда следует, что проблема P, представленная экзистенциально квантифицированной конъюнкцией положительных литералов, логически подразумевается из D тогда и только тогда, когда P истинно в M . Минимальная модельная семантика предложений Хорна является основой стабильной модельной семантики логических программ. [9]
См. также [ править ]
Примечания [ править ]
- ^ Хорн 1951 .
- ^ Маковский 1987 .
- ^ Басс 1998 .
- ^ Лау и Орнаги 2004 .
- ^ Как и в доказательстве теоремы о разрешении , «показать φ» и «предположить ¬φ» являются синонимами ( косвенное доказательство ); они оба соответствуют одной и той же формуле, а именно. ¬φ.
- ^ Даулинг и Гальер 1984 .
- ^ Чанг и Кейслер 1990 , раздел 6.2.
- ^ ван Эмден и Ковальски 1976 .
Ссылки [ править ]
- Беррис, Стэнли; Санкаппанавар, 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 .
