В чем разница между логическим программированием и автоматическим доказательством теорем (ATP) (например, с помощью E-Prover, Spass или Princess)?
Я много искал, и единственная информация, которую я нашел, это то, что АТФ является предшественником логического программирования. Но я не вижу разницы. Но я думаю, это больше, чем синтаксис.
Что касается прологовой части вопроса, лучше всего это сказал Ричард О'Киф:
Пролог — эффективный язык программирования, потому что это глупый доказатель теорем.
Таким образом, существует связь между Прологом и доказательством теорем. Пролог имеет некоторые особенности средства доказательства теорем, например, он ищет доказательства или, скорее, опровержения разрешения, но делает это неполным способом. это больше приспособлено к языку программирования общего назначения.
Конечно, сравнительно близкое родство между Прологом и средствами доказательства теорем делает Пролог отличным выбором для реализации более полноценных средств доказательства теорем.
На самом деле сравнительно легко дополнить и расширить неполную стратегию выполнения Пролога по умолчанию, чтобы поиск стал более полным.
Обратите внимание, однако, что Пролог также демонстрирует некоторые экстралогические особенности, которые выходят за рамки доказательства теорем и фактически часто могут мешать декларативным рассуждениям. См. также logical-purity.
