Существует ли какое-либо программное обеспечение, связанное с использованием формата Fitch (используется в Language, Proof and Logic), позволяет разместить определенный набор помещений и целей и показать им полный список шагов, необходимых для решения проблемы?Fitch Format Proofs - любые автоматические решатели вокруг?
Короткий ответ: Нет
Medium Ответ: Не может действительно быть сделано, хотя можно было бы написать программу, чтобы проверить правильность данного доказательства довольно легко. В случае логики высказываний проблема автоматического нахождения доказательства NP-полная (хотя она разрешима!), И в логике первого порядка существуют истинные теоремы, для которых превентор никогда не прекратится. (неразрешимый) (через доказательство неполноты Gödel)
Если вы заинтересованы в написании такого материала, вы можете нанести удар по нему и, возможно, заставить его работать в некоторых небольших случаях, но в целом это невозможно.
Если вы ищете такое, чтобы получить ответы на свои домашние задания, бросьте попытку. (а) вы его не найдете и (б) проблемы из этой книги довольно легкие и могут быть интересными! Просто дайте им попробовать, и при необходимости попробуйте помощь. и, конечно же, (c) вы не узнаете ничего, если будете обманывать.
Рассмотрим Apros на OLI Карнеги-Меллона http://www.phil.cmu.edu/projects/apros/.
Хотя эта ссылка может ответить на вопрос, лучше включить здесь основные части ответа и предоставить ссылку для справки , Ответные ссылки могут стать недействительными, если связанная страница изменится. – honk
На самом деле существуют механические способы создания доказательств стиля Fitch. Например. в главе 13 [Логический учебник Пола Теллера] (http://tellerprimer.ucdavis.edu/pdf/) содержится описание такой процедуры для логики высказываний (в основном дерева истинности в нотации Fitch). Кроме того, логика первого порядка является полуразграниченной, то есть есть способы механически найти доказательство, если секвенция действительна (хотя поиск может никогда не заканчиваться в случае неправильной секвенции). Конечно, ничто из этого не помогает для логической домашней работы, поскольку такие доказательства имеют тенденцию быть смехотворно длинными ;-) –