6.16. БИБЛИОГРАФИЧЕСКИЕ И ИСТОРИЧЕСКИЕ ЗАМЕЧАНИЯ
Основания логики
Наше весьма поверхностное изучение математической логики можно углубить, обратившись к некоторым стандартным учебникам. Блестящими учебниками являются книги Мендельсона (1964) и Роббина (1969), а для специалистов — классическая книга Чёрча (1956). В этих книгах излагается то, что можно назвать классической логикой. Принцип резольвенций (или в действительности любое обсуждение автоматического доказательства теорем) еще не попал в учебники по логике.
В основу настоящей главы мы положили исчисление предикатов первого порядка с резольвенциями, поскольку оно явно играет большую роль при автоматическом решении задач. Существенное упущение здесь, однако, состоит в том, что мы не рассмотрели отношения равенства. Все еще неясно, как «встроить» в автоматические доказатели теорем отношение равенства (и другие стандартные часто встречающиеся отношения). Обсуждение этих усложнений выходит за рамки настоящей книги. Одна из схем, позволяющая включить отношение равенства в устройства автоматического доказательства теорем, обсуждается Робинсоном и Восом (1969).
Далее, становится все яснее, что для создания сложных универсальных решающих устройств необходимо привлечь логики высших порядков. Обсуждение применения логики высших порядков к решению задач можно найти у Маккарти и Хэйеса (1969). В книге Роббина (1969) есть раздел, посвященный логике второго порядка, а в статьях Дж. Робинсона (1969а, 19696) рассматриваются общие проблемы процедур доказательства для логик высших порядков.
Этапы, выделенные нами при преобразовании правильно построенной формулы в совокупность предложений, основаны на процедуре Дэвиса и Путнама (1960). Такое представление в виде предложений называют также бескванторной коиъюнктивно нормальной формой.
Эрбрановские процедуры доказательства и резольвенции
Принцип резольвенций в автоматическом доказательстве теорем основан на процедуре доказательства Эрбрана (1930). Прямая реализация эрбрановской процедуры была бы в высшей степени неэффективной. Усовершенствования, внесенные Правицем (1960) и другими, привели в конечном итоге к принципу резольвенции, Дж. Робинсона (1965а). Наш способ изложения методов доказательства, основанных на резольвенциях, опирается на работу Ковальского и Хэйеса (1969). (См. также Дж. Робинсон, 1968.) Привлечение семантических деревьев делает очевидной связь между резольвенциями и эрбрановскими методами, их можно использовать также для доказательства применимости правил, более общих по сравнению с простой резольвенцией. Наше доказательство полноты принципа резольвенции является частным случаем доказательства полноты более общего правила вывода, приведенного у Ковальского и Хэйеса (1969).
Ясно написанное, сжатое изложение принципа резольвенции с доказательством его полноты и непротиворечивости дано в статье Лакхэма (1967). Доказательство непротиворечивости и полноты можно найти еще в первой работе Дж. Робинсона (1965а). В этих двух работах приведено также доказательство
«корректности» алгоритма унификации. Дж. Робинсон (1970) написал, кроме того, блестящее, исследование, посвященное «механическому доказательству теорем».
Задачи
(см. скан)
