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

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

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

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

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

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

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

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

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

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

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

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

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

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

Предложение  называется подслучаем предложения , если существует такая подстановка , что . Например,

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

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

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

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

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

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

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

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

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