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

Число типов выводимых формул (целей) для реальной среды ограничено конкретными потребностями. Вывод только этих формул следует гарантировать, ограничиваясь тем множеством аксиом, которые это позволяют сделать. 94 4.3. Полнота и непротиворечивость исчисления Проблемой полноты и непротиворечивости исчислений занимались и продолжают заниматься. Для некоторых исчислений вопрос о полноте имеет положительный ответ, например для классического исчисления высказываний и для классического исчисления предикатов первого порядка. Для классического исчисления предикатов вопрос полноты был решен немецким математиком Куртом Геделем в 1930-1931 годах. Он доказал теорему, которая называется теоремой о полноте классического исчисления логики предикатов первого порядка. Согласно этой теореме любая общезначимая формула классического исчисления логики предикатов первого порядка выводима в этом исчислении. Это означает, что для классического исчисления логики предикатов первого порядка существует полная стратегия вывода.