Глава 6. ДОКАЗАТЕЛЬСТВО ТЕОРЕМ В ИСЧИСЛЕНИИ ПРЕДИКАТОВ
6.1. ИСЧИСЛЕНИЕ ПРЕДИКАТОВ КАК ЯЗЫК ДЛЯ РЕШЕНИЯ ЗАДАЧ
Мы отмечали в гл. 1, что для решения многих задач может потребоваться логический анализ. Для автоматического логи ческого рассуждения необходим некоторый формальный язык, на котором можно формулировать посылки и делать верные логические выводы. Все, что для этого требуется, — это возможность описать интересующую нас задачу и средства поиска соответствующих шагов в процессе логического вывода.
Исчисление предикатов первого порядка — это такая система в логике, в которой можно выразить большую часть того, что относится к математике, а также многое из разговорного языка. Эта система содержит правила логического вывода, позволяющие делать верные логические построения новых утверждений, исходя из некоторого заданного множества утверждений. Благодаря своей общности и логической силе исчисление предикатов может всерьез претендовать на использование его для машинного построения умозаключений.
В этой главе мы на время отойдем от нашей главной цели изучения процессов решения и дадим обзор теории исчисления предикатов и приемов дедукции в этой системе, основанных на 
принципе резольвенций. В гл. 7 мы вернемся к предмету решения задач и приведем примеры, иллюстрирующие задачи. Наконец, в гл. 8 мы объясним работу некоторых наиболее эффективных способов поиска требуемых логических заключений.
Язык, подобный языку в исчислении предикатов, определяется его синтаксисом. Чтобы задать синтаксис, надо задать алфавит символов, которые будут использоваться в этом языке, и правила соединения этих символов друг с другом в выражениях, допустимых на этом языке. Один из важных классов выражений в исчислении предикатов — это класс правильно построенных формул (п. п. формул).
Мы обычно пользуемся языком для того, чтобы делать утверждения, касающиеся интересующей нас области. Отношения между языком и описываемой им областью определяются семантикой этого языка. П. п. формулы исчисления предикатов как раз являются теми выражениями, которые мы будем
использовать в качестве утверждений, касающихся интересующей 
области. Говорят, что п. п. формулы принимают значение Т или 
в зависимости от того, являются эти утверждения в этой области истинными или ложными. Приемы обращения с п. п. формулами позволяют строить умозаключения, относящиеся к некоторой области, и, следовательно, могут представить интерес при создании процессов принятия решения, требующих такого умозаключения.
В следующем разделе мы зададим синтаксис одного из вариантов исчисления предикатов. Затем покажем, как на этом языке можно делать утверждения, касающиеся описываемой им области.
