Глава 7. ПРИМЕНЕНИЯ ИСЧИСЛЕНИЯ ПРЕДИКАТОВ К РЕШЕНИЮ ЗАДАЧ

7.1. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ ПРИ РЕШЕНИИ ЗАДАЧ

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

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

Заметим, что умение строить удовлетворяющие частные случаи для переменной, относящейся к квантору существования, позволяет ставить вопросы весьма общего свойства. Например, мы могли бы задаться вопросом: «Существует ли решающая последовательность для некоторого случая игры в пятнадцать?» Если можно найти конструктивное доказательство того, что решение существует, то можно указать также само решение. Мы могли бы задать даже более трудный вопрос: «Существует ли программа, которая будет производить определенные вычисления?» Из конструктивного доказательства ее существования можно было бы извлечь саму программу. (Очевидно, следует помнить, что сложные вопросы, вообще говоря, приводят к сложным доказательствам, возможно настолько сложным, что

наши автоматические процедуры поиска доказательства их не найдут.)

Основная цель настоящей главы — описать процесс, с по- мощью которого удовлетворяющий частный случай переменной, относящейся к квантору существования, в некоторой п. п. формуле можно извлечь из доказательства п. п. формулы, содержащей эту переменную. Затем на ряде примеров мы проиллюстрируем применение этого процесса и вообще исчисления предикатов к решению задач. Обсуждение процессов поиска при построении самих доказательств мы отложим до следующей главы.

Часто утверждения, относящиеся к задаче, делаются в форме фраз на разговорном языке, например английском. Поэтому естественно возникает вопрос, в каких случаях можно осуществить автоматический перевод с английского языка на язык п. п. формул исчисления предикатов первого порядка. Хотя такой процесс перевода должен быть одной из основных частей законченного решателя задач, мы его не будем здесь рассматривать. Написано несколько программ, позволяющих осуществлять в ограниченных рамках перевод с английского языка на язык исчисления предикатов, но способность работать с естественным языком пока находится в весьма неудовлетворительном состоянии. Можно выделить две главные трудности: (1) выбор отношений, которые следует использовать при переводе предложений с английского языка, и (2) однозначное преобразование смысла, вложенного в фразу, в п. п. формулы, использующие предикатные символы для этих отношений. Часто неоднозначность можно устранить только рассмотрением «контекста» фразы, а это сопряжено с трудными и не до конца понятыми процессами. Проблема преобразования английского языка в п. п. формулы нисколько не легче, чем, например, проблема преобразования английского языка в описания состояний, операторы и т. д. В настоящей книге мы вынуждены оставить без рассмотрения вопросы перевода (сколь ни важны они) и сосредоточить все свое внимание на процессах решения уже сформулированных задач.