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

Отметим еще один важный момент, связанный с теоремой о полноте классического исчисления логики предикатов первого порядка и вопросом об установлении факта невыводимости формулы из начальной базы знаний без вывода. Теорема Геделя гласит, что любая общезначимая формула логики предикатов первого порядка выводима в классическом исчислении логики предикатов первого порядка. Но в каждом конкретном случае до тех пор пока вывод не осуществлен, мы не знаем, выводима ли данная формула. А если она не выводима и, следовательно, вывод никогда не будет найден, то как отличить ситуацию, когда мы еще не достигли вывода, от ситуации, когда он никогда не будет достигнут? К сожалению, ответ на этот вопрос не утешителен: невозможно различить эти две ситуации и выводимость формулы может быть установлена только тогда, когда она выведена. Если же она не выводится, то придется осуществить все варианты вывода и только после этого, если она все-таки не была выведена, сделать заключение о невыводимости. Это же считается справедливым и для неклассических исчислений.