Расширение системы Prolog
Еще один способ создания средства автоматического доказательства теорем состоит в том, чтобы начать с компилятора Prolog и дополнить его в целях получения непротиворечивого и полного средства формирования рассуждений для полной логики первого порядка, Именно этот подход был принят при создании программы РТТР (Prolog Technology Theorem Prover) [1463]. Как описано ниже, программа РТТР включает пять существенных дополнений к системе Prolog, позволяющих восстановить полноту и выразительность алгоритма обратного логического вывода.
• В процедуру унификации снова вводится проверка вхождения для того, чтобы эта процедура стала непротиворечивой.
• Поиск в глубину заменяется поиском с итеративным углублением. Это позволяет добиться того, чтобы стратегия поиска стала полной, а увеличение продолжительности поиска измерялось лишь постоянной зависимостью от времени.
• Разрешается применение отрицаемых литералов (таких как -iP(x)). В этой реализации имеется две отдельные процедуры; в одной из них предпринимается попытка доказать Р, а в другой — доказать -лР.
• Выражение с п атомами хранится в виде п различных правил. Например, при наличии в базе знаний выражения А <= в л С должно быть также предусмотрено хранение в ней этого выражения, представленного как -лВ <= С л —А и как
-iC <= в л —Л. Применение такого метода, известного под названием блокирование (locking), означает, что текущая цель требует унификации только с головой каждого выражения, и вместе с тем позволяет должным образом учитывать отрицание.
• Логический вывод сделан полным (даже для нехорновских выражений) путем добавления правила резолюции с линейным входным выражением: если текущая цель унифицируется с отрицанием одной из целей в стеке, то данная цель может рассматриваться как решенная. В этом состоит один из способов рассуждения от противного. Предположим, что первоначальной целью было высказывание Р и что эта цель свелась в результате применения ряда этапов логического вывода к цели -нР. Тем самым установлено, что -нР => Р, а это выражение логически эквивалентно Р.
Несмотря на эти изменения, программа РТТР сохраняет свойства, благодаря которым обеспечивается высокое быстродействие системы Prolog. Операции унификации все еще осуществляются посредством непосредственной модификации переменных, а отмена связывания выполняется путем разгрузки контрольного стека во время возврата. Стратегия поиска все еще основана на резолюции с применением входных выражений, а это означает, что в каждой операции резолюции участвует одно из выражений, содержащихся в первоначальной формулировке задачи (а не какое-то производное выражение). Такой подход позволяет осуществить компиляцию всех выражений из первоначальной формулировки задачи.
Основным недостатком программы РТТР является то, что пользователь должен отказаться от любых попыток взять на себя управление поиском решений. Каждое правило логического вывода в этой системе используется и в его первоначальной, и в кон-трапозитивной форме. Это может привести к выполнению таких операций поиска, которые противоречат здравому смыслу. Например, рассмотрим следующее правило:
(f(x,y) = f(a,b)) <= (х = а) л (у = Ь)
Если бы оно рассматривалось как правило Prolog, то применялся бы разумный способ доказательства того, что два терма f равны. Но в системе РТТР должно быть также сформировано контрапозитивное правило:
(х Ф а) (f(x,y) Ф f(a,b)) л (у = Ь)
По-видимому, попытка доказать, что любые два терма, хиа, являются разными, привела бы к непроизводительным затратам ресурсов.
Применение средств автоматического доказательства теорем в качестве помощников
До сих пор в этой книге любая система формирования рассуждений рассматривалась как независимый агент, который должен был принимать решения и действовать самостоятельно. Еще одно направление использования средств автоматического доказательства теорем состоит в том, что они должны служить в качестве помощников, предоставляя консультации, скажем, математикам. При эксплуатации подобных систем в режиме помощи математик действует в роли руководителя, очерчивая стратегию определения того, что должно быть сделано в следующую очередь, а затем передавая системе автоматического доказательства теорем просьбу проработать все детали. Это позволяет в определенной степени устранить проблему полуразрешимости, поскольку руководитель научной разработки может отменить запрос и опробовать другой подход, если поиск ответа на запрос потребовал слишком много времени. Любая система автоматического доказательства теорем может также действовать в качестве средства проверки доказательства; при ее использовании в таком режиме доказательство предоставляется человеком в виде ряда довольно крупных этапов; отдельные операции логического вывода, которые требуются для того, чтобы показать, что каждый из этих этапов является непротиворечивым, определяются системой.
В частности, сократовское средство формирования рассуждений (socratic reasoner) представляет собой такую систему автоматического доказательства теорем, в которой функция Ask является неполной, но эта система всегда позволяет прийти к определенному решению, если ей будет задан правильный ряд вопросов. Таким образом, сократовские средства формирования рассуждений становятся хорошими помощниками, при условии, что есть руководитель, способный составить правильный ряд вызовов функции Ask. Одной из сократовских систем формирования рассуждений для математиков является Ontic [1005].
Области практического использования средств автоматического доказательства теорем
Средства автоматического доказательства теорем позволили получить новейшие математические результаты. Программа SAM (Semi-Automated Mathematics) была первой программой, с помощью которой удалось доказать одну из лемм в теории решеток [602]. Кроме того, программа Aura позволила найти ответ на многие открытые вопросы в нескольких областях математики [1621]. Программа автоматического доказательства теорем Бойера-Мура [165] применялась и дорабатывалась в течение многих лет, и ею воспользовался Натараджан Шанкар для получения первого полностью строгого формального доказательства теоремы Гёделя о неполноте [1393]. Одним из самых строгих средств автоматического доказательства теорем является программа Otter; она использовалась для решения некоторых открытых задач в области комбинаторной логики. Наиболее известные из них касаются алгебры Роб-бинса. В 1933 году Герберт Роббинс предложил простое множество аксиом, которые, на первый взгляд, могли служить для определения булевой алгебры, но ни одного доказательства этой гипотезы найти не удавалось (несмотря на напряженную работу нескольких выдающихся математиков, включая самого Альфреда Тарского). Наконец, 10 октября 1996 года после восьми дней вычислений программа EQP (одна из версий программы Otter) нашла такое доказательство [1019].
Средства автоматического доказательства теорем могут также применяться для решения задач, связанных с проверкой и синтезом как аппаратных, так и программных средств, поскольку для обеих этих проблемных областей могут быть предусмотрены правильные варианты аксиоматизации. Поэтому исследования доказательства теорем проводятся не только в искусственном интеллекте, но и в таких областях, как проектирование аппаратных средств, языки программирования и разработка программного обеспечения. В случае программного обеспечения аксиомы определяют свойства каждого синтаксического элемента языка программирования. (Процесс формирования рассуждений о программах полностью аналогичен процессу формирования рассуждений о действиях в ситуационном исчислении.) Программный алгоритм проверяется путем демонстрации того, что его выходы соответствуют спецификациям для всех входов. Таким образом были проверены алгоритм шифрования RSA с открытым ключом и алгоритм согласования строк Бойера-Мура [166]. В случае аппаратного обеспечения аксиомы описывают способы взаимодействия сигналов и элементов схемы (один из примеров приведен в главе 8). Программой Aura [1610] был проверен проект 16-битового сумматора. Системы формирования логических рассуждений, предназначенные специально для проверки аппаратных средств, оказались способными проверять целые процессоры, включая свойства синхронизации этих процессоров [1455].
Формальный синтез алгоритмов был одним из первых направлений использования средств автоматического доказательства теорем, как и было намечено Кордел-лом Грином [591], который опирался на идеи, высказанные ранее Саймоном [1416]. Общий замысел состоит в том, что должна быть доказана теорема с утверждением, что "существует программа р, удовлетворяющая некоторой спецификации". Если удается ограничить это доказательство конструктивной формой, то появляется возможность извлечь из результатов доказательства требуемую программу. Хотя полностью автоматизированный дедуктивный синтез, как стало называться это направление, еще не осуществим применительно к программированию задач общего назначения, дедуктивный синтез, управляемый вручную, оказался успешным при проектировании нескольких новейших и сложнейших алгоритмов. Кроме того, активной областью исследования является синтез программ специального назначения. В области синтеза аппаратных средств программа автоматического доказательства теорем Aura применялась для проектирования схем, оказавшихся более компактными по сравнению с разработанными во всех предыдущих проектах [1609]. Для многих проектов логических схем достаточно применить пропозициональную логику, поскольку множество интересующих высказываний является фиксированным благодаря конечным размерам множества схемных элементов. В наши дни применение пропозиционального логического вывода в аппаратном синтезе является стандартным методом, имеющим много крупномасштабных областей использования (см., например, работу Новика и др. [1149]).
Те же методы теперь начинают также применяться для проверки программного обеспечения с помощью таких систем, как программа проверки моделей Spin [672]. Например, с ее помощью была проверена до и после полета программа управления космическим аппаратом Remote Agent [633].
В этой главе приведен анализ логического вывода в логике первого порядка и многих алгоритмов его выполнения.
• В первом подходе используется правило логического вывода для конкретизации кванторов в целях преобразования задачи логического вывода в форму пропозициональной логики. Как правило, этот подход характеризуется очень низким быстродействием.
• Использование унификации для выявления подходящих подстановок для переменных позволяет устранить этап конкретизации в доказательствах первого порядка, в результате чего этот процесс становится гораздо более эффективным.
• В поднятой версии правила отделения унификация применяется для получения естественного и мощного правила логического вывода — обобщенного правила отделения. В алгоритмах прямого логического вывода и обратного логического вывода это правило применяется к множествам определенных выражений.
• Обобщенное правило отделения является полным применительно к определенным выражениям, но проблема логического следствия остается полуразрешимой. Для программ Datalog, состоящих из определенных выражений без функций, проблема логического следствия разрешима.
• Прямой логический вывод используется в дедуктивных базах данных, где он может сочетаться с реляционными операциями баз данных. Он также применяется в продукционных системах, которые обеспечивают эффективное обновление при наличии очень больших наборов правил.
• Прямой логический вывод для программ Datalog является полным и выполняется за время, определяемое полиномиальной зависимостью.
• Обратный логический вывод используется в системах логического программирования, таких как Prolog, в которых реализована сложная технология компиляции для обеспечения очень быстрого логического вывода.
• Недостатками обратного логического вывода являются излишние этапы логического вывода и бесконечные циклы; эти недостатки можно устранить путем запоминания.
• Обобщенное правило логического вывода на основе резолюции позволяет создать полную систему доказательства для логики первого порядка с использованием баз знаний в конъюнктивной нормальной форме.
• Существует несколько стратегий сокращения пространства поиска для систем с резолюцией без потери полноты. Эффективные средства автоматического доказательства теорем на основе резолюции использовались для доказательства интересных математических теорем, а также для проверки и синтеза программных и аппаратных средств.