Искусственный интеллект

Гедель доказал теорему о полноте классического исчисления предикатов первого порядка, но не привел полной стратегии вывода, которую можно достаточно эффективно использовать на практике. Это сделал в 1965 г. Дж. Робинсон, опубликовав полную стратегию вывода для классического исчисления высказываний на основе правила резолюции. Заметим, что упомянутые положительные ответы о полноте относятся к классическому исчислению предикатов первого порядка. Нас же в практическом плане интересуют, прежде всего, неклассические исчисления. Вопрос об их полноте и непротиворечивости обсудим далее. Однако еще раз заметим, что неклассические исчисления, использующие классическое исчисление предикатов первого порядка, могут, наряду с другими, включать его правила вывода, в частности правило резолюции. Вследствие теоретической и практической значимости этого правила стратегию вывода на его основе рассмотрим детально в следующем параграфе.