Интерпретатор языка Пролог (стр. 4 из 15)

Пусть исходные предложения задаются в виде

и переменные, входящие в

, не встречаются в

и обратно. Пусть

- такие два подмножества

, что для объединения

существует наиболее общий унификатор

. Тогда говорят, что два предложения

разрешаются, а новое предложение

является их резольвентой. Резольвента представляет выведенное предложение, и процесс образования резольвенты из двух "родительских" предложений называется резольвенцией.

Иными словами мы хотим иметь возможность находить доказательство того, что некоторая правильно построенная формула W в исчислении предикатов логически следует из некоторого множества S правильно построенных формул. Это задача эквивалентна задаче доказательства того, что множество

неудовлетворимо. Процессы выявления неудовлетворимости некоторого множества предложений называются процессами опровержения.

Принцип резольвенции непротиворечив и полон. Непротиворечивость означает, что если когда-нибудь мы придем к пустому предложению, то исходное множество обязано быть неудовлетворимым. Полнота означает, что если исходное множество неудовлетворимо, то, в конце концов, мы придем к пустому предложению.[2]

1.3.2 Методы поиска доказательства в исчислении предикатов

1.3.2.1 Исчисление предикатов при решении задач

Иногда достаточно только знать, следует ли логически правильно построенная формула W из некоторого множества S правильно построенных формул. Если W не следует из S, то, возможно, мы захотим знать, следует ~W из S. Конечно, в силу неразрешимости исчисления предикатов не всегда можно установить, следует ли W из S.

В других приложениях нужно знать значение элемента x (если он существует), при котором данная правильно построенная формула W (содержащая x в качестве переменной) логически следует из некоторого множества S правильно построенных формул. Иными словами, мы хотели бы знать, следует ли логически правильно построенная формула

, и если да, то каков тот частный случай переменной x. Проблема поиска доказательства правильно построенной формулы

, исходя из S, является обычной проблемой доказательства в исчислении предикатов, но для построения удовлетворяющего частного случая требуется, чтобы метод доказательства был "конструктивным".

Часто утверждения, относящиеся к задаче, делаются в форме фраз на разговорном языке, например английском. Поэтому естественно возникает вопрос, в каких случаях можно осуществить автоматический перевод с английского языка на язык исчисления предикатов. Написано несколько программ, позволяющих в ограниченных рамках перевод с естественного языка на язык предикатов, но способность работать с естественным языком пока находится в весьма неудовлетворительном состоянии.[1]

1.3.2.2 Стратегии перебора

Непосредственное применение принципа резольвенции соответствует простой процедуре полного перебора при построении опровержения. Такой перебор мы начинается множества S, к которому добавляется резольвенты всех пар предложений в S с тем, чтобы образовать множество R. Затем добавляются резольвенты всех пар предложений в R с тем, чтобы образовать множество R(R(S))=R²(S), и т.д. Этот метод перебора как правило непригоден для практики, так как множества R(S), R²(S),… слишком быстро разрастаются. Практические процедуры доказательства определяются стратегиями перебора, применяемыми для его ускорения. Такие стратегии бывают трех типов: стратегии упрощения, стратегии очищения и стратегии упорядочения.[2]

1.3.2.3 Стратегии упрощения

Иногда множество предложений удается упростить, исключив из него некоторые предложения или исключив из предложений определенные литералы. Эти упрощения таковы, что упрощенное множество предложений выполнимо тогда и только тогда, когда выполнимо исходное множество предложений. Таким образом, применение стратегий упрощения позволяет снизить скорость роста новых предложений.

Исключение тавтологий.

Любое предложение, содержащее литерал и его дополнение (такое предложение называется тавтологией), можно отбросить, так как любое невыполнимое множество, содержащее тавтологию, остается невыполнимым и после ее удаления.

Исключение путем означивания предикатов.

Иногда появляется возможность означить (выяснить значение истинности) литералы, и это оказывается удобнее, чем включать соответствующие предложения в S. Такое означивание легко провести для константных частных случаев. Например, если предикатная буква E обозначает отношение равенства, то означивание константных частных случаев типа E(7,3), когда они появляются, провести легко, хотя нам бы не хотелось добавлять к S полную таблицу, содержащих много константных частных случаев литералов E(x,y) и ~E(x,y).

Если какой-нибудь литерал предложения получает значение истинности T, то все предложения можно отбросить, не нарушая при этом свойства невыполнимости оставшегося множества. Если же какой-нибудь литерал при означивании получает значение истинности F, то из этого предложения можно исключить данное вхождение литерала.[2]

Исключение подслучаев.

Предложение

называется подслучаем предложения

, если существует такая подстановка

, что

. Например,

- подслучай предложения

Предложение в S, являющиеся подслучаем другого предложения в S, можно исключить из S, не нарушая свойства невыполнимости оставшегося множества. Отбрасывание предложений, являющихся подслучаями других, часто ведет к значительному уменьшению числа резольвенций, необходимых для нахождения доказательства.[2]

1.3.2.4 Стратегии очищения

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

объединение множества S и множества всех резольвент всех пар предложений из S , удовлетворяющих критерию C. Ясно, что

Про стратегию очищения, использующую критерий C, говорят, что в ней используется "резольвенция по отношению к C". Для применения такой стратегии сначала вычисляется

, затем

и т.д. до тех пор, пока при некотором n в

не окажется пустого предложения обозначемого nil.

Потенциальное достоинство стратегии очищения, в том, что на каждом уровне требуется меньше резольвенций. Однако уровень, на котором появляется пустое предложение, обычно возрастает, так что стратегия очищения приводит обычно к узконаправленному, но более глубокому перебору. Стратегия очищения полезна лишь в том случае, если она уменьшает все затраты усилий на перебор, включая усилия, необходимые для проверки критерия C.[2]

1.3.2.5 Формы доказательства с отфильтровыванием

предшествующих вершин

Доказательство с отфильтровыванием предшествующих вершин производится с использованием AF-графа. Граф опровержения имеет AF-форму, если каждая из его вершин соответствует одному из следующих предложений: