В математической логике и логическом программировании предложение Хорна - это логическая формула определенной формы, подобной правилу, которая дает ей полезные свойства для использования в логическом программировании, формальной спецификации и теории моделей . Предложения Хорна названы в честь логика Альфреда Хорна , который впервые указал на их значение в 1951 г. [1]
Определение
Пункт рогом является пункт (а дизъюнкция из литералов ) с более чем одним положительным, т.е. unnegated , буквальным.
И наоборот, дизъюнкция литералов с одним отрицательным литералом называется предложением двойного рога .
Предложение Хорна с ровно одним положительным литералом является определенным предложением или строгим предложением Хорна ; [2] определенное предложение без отрицательных литералов является единичным предложением , [3] а единичное предложение без переменных является фактом ; [4] . Предложение Хорна без положительного литерала является целевым предложением . Обратите внимание, что пустое предложение, не содержащее литералов (что эквивалентно false ), является целевым предложением. Эти три вида предложений Хорна проиллюстрированы в следующем пропозициональном примере:
Тип оговорки Рога | Форма дизъюнкции | Форма следствия | Читайте интуитивно как |
---|---|---|---|
Определенная оговорка | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t ∨ u | u ← p ∧ q ∧ ... ∧ t | Предположу , что, если р и д и ... и т всего трюма, то и у имеют место |
Факт | ты | u ← верно | Предположим, что u выполняется |
Положение о цели | ¬ p ∨ ¬ q ∨ ... ∨ ¬ t | ложь ← p ∧ q ∧ ... ∧ t | показать , что р и д и ... и т все держать [примечание 1] |
Все переменные в предложении неявно универсально количественно оцениваются с охватом всего предложения. Так, например:
- ¬ человек ( X ) ∨ смертный ( X )
означает:
- ∀X (¬ человек ( X ) ∨ смертный ( X ))
что логически эквивалентно:
- ∀X ( человек ( X ) → смертный ( X ))
Значимость
Предложения Хорна играют основную роль в конструктивной логике и вычислительной логике . Они важны при автоматическом доказательстве теорем с помощью разрешения первого порядка , потому что резольвента двух предложений Хорна сама по себе является предложением Хорна, а резольвента целевого предложения и определенного предложения является целевым предложением. Эти свойства предложений Хорна могут повысить эффективность доказательства теоремы: целевое предложение - отрицание этой теоремы; см. пункт «Цель» в приведенной выше таблице. Интуитивно, если мы хотим доказать φ, мы предполагаем ¬φ (цель) и проверяем, приводит ли такое предположение к противоречию. Если это так, то φ должно выполняться. Таким образом, механический инструмент доказательства должен поддерживать только один набор формул (предположений), а не два набора (предположения и (под) цели).
Пропозициональные предложения Хорна также представляют интерес с точки зрения вычислительной сложности . Проблема нахождения присвоений истинностных значений, чтобы сделать конъюнкцию пропозициональных предложений Хорна истинными, известна как HORNSAT . Эта задача является P-полной и разрешима за линейное время . [5] Обратите внимание, что проблема неограниченной булевой выполнимости является NP-полной проблемой.
Логическое программирование
Предложения Horn также являются основой логического программирования , где обычно пишут определенные предложения в форме импликации :
- ( p ∧ q ∧ ... ∧ t ) → u
Фактически, разрешение предложения цели с определенным предложением для создания нового предложения цели является основой правила вывода разрешения SLD , используемого в реализации языка логического программирования Prolog .
В логическом программировании определенное предложение ведет себя как процедура приведения к цели. Например, предложение Horn, написанное выше, ведет себя как процедура:
- чтобы показать u , показать p и показать q и ... и показать t .
Чтобы подчеркнуть обратное использование предложения, его часто пишут в обратной форме:
- u ← ( p ∧ q ∧ ... ∧ t )
В Прологе это записывается так:
u : - p , q , ..., t .
В логическом программировании вычисления и оценка запроса выполняются путем представления отрицания решаемой проблемы в виде целевого предложения. Например, проблема решения экзистенциально квантифицированной конъюнкции положительных литералов:
- ∃ X ( p ∧ q ∧ ... ∧ t )
представлен отрицанием проблемы (отрицанием того, что у нее есть решение) и представлением ее в логически эквивалентной форме предложения цели:
- ∀ X ( ложь ← p ∧ q ∧ ... ∧ t )
В Прологе это записывается так:
: - п , д , ..., т .
Решение проблемы сводится к получению противоречия, которое представлено пустым предложением (или «ложным»). Решением проблемы является замена переменных в целевом предложении терминами, которые можно извлечь из доказательства противоречия. При таком использовании целевые предложения аналогичны конъюнктивным запросам в реляционных базах данных, а логика предложения Хорна по вычислительной мощности эквивалентна универсальной машине Тьюринга .
Нотация Пролога на самом деле неоднозначна, и термин «целевое предложение» иногда также используется неоднозначно. Переменные в предложении цели могут быть прочитаны как универсально или экзистенциально количественно оцененные, а вывод «ложного» можно интерпретировать либо как вывод противоречия, либо как вывод успешного решения проблемы, которую необходимо решить. [ требуется дальнейшее объяснение ]
Ван Эмден и Ковальский (1976) исследовали теоретико-модельные свойства Хорна в в контексте логического программирования, показывая , что каждый набор определенных ПОСТАНОВЛЕНИЯ D имеет единственную минимальную модель M . Атомная формула логически вытекает из D тогда и только тогда , когда истинно в М . Отсюда следует , что проблема Р представлена экзистенциально количественным сочетанием положительных литералов логически вытекает из D тогда и только тогда , когда Р истинно в М . Минимальная модельная семантика предложений Хорна является основой стабильной модельной семантики логических программ. [6]
Заметки
- ^ Как и в доказательстве теоремы о разрешении , «показать φ» и «предположить ¬φ» являются синонимами ( косвенное доказательство ); они оба соответствуют одной и той же формуле, а именно. ¬φ.
Рекомендации
- ^ Хорн, Альфред (1951). «О предложениях, истинных для прямых объединений алгебр». Журнал символической логики . 16 (1): 14–21. DOI : 10.2307 / 2268661 . JSTOR 2268661 .
- ^ Маковский (1987). «Почему формулы Хорна имеют значение в компьютерных науках: исходные структуры и общие примеры» (PDF) . Журнал компьютерных и системных наук . 34 (2–3): 266–292. DOI : 10.1016 / 0022-0000 (87) 90027-4 .
- ^ Басс, Сэмюэл Р. (1998). «Введение в теорию доказательства» . В Сэмюэле Р. Бассе (ред.). Справочник по теории доказательств . Исследования по логике и основам математики. 137 . Elsevier BV, стр. 1–78. DOI : 10.1016 / S0049-237X (98) 80016-5 . ISBN 978-0-444-89840-1. ISSN 0049-237X .
- ^ Лау и Орнаги (2004). «Определение композиционных единиц для правильной разработки программ в вычислительной логике». Конспект лекций по информатике . 3049 : 1-29. DOI : 10.1007 / 978-3-540-25951-0_1 . ISBN 978-3-540-22152-4.
- ^ Доулинг, Уильям Ф .; Галлье, Жан Х. (1984). «Алгоритмы линейного времени для проверки выполнимости пропозициональных формул Хорна». Журнал логического программирования . 1 (3): 267–284. DOI : 10.1016 / 0743-1066 (84) 90014-1 .
- ^ van Emden, MH; Ковальский, Р.А. (1976). «Семантика логики предикатов как языка программирования» (PDF) . Журнал ACM . 23 (4): 733–742. CiteSeerX 10.1.1.64.9246 . DOI : 10.1145 / 321978.321991 .