Доказательства Формата Fitch - Какие-либо автоматические решатели вокруг? [закрытый]

Коротко ответ: Нет.

Средний ответ: На самом деле это невозможно, хотя можно довольно легко написать программу для проверки действительности данного доказательства. В случае логики высказываний проблема автоматического нахождения доказательства является NP-полной (хотя она разрешима!), А в логике первого порядка есть истинные теоремы, на которых доказывающий никогда не остановится. (неразрешимо) (через доказательство неполноты Гёделя)

Если вы заинтересованы в написании такой вещи, вы можете нанести удар и, возможно, заставить ее работать в некоторых более мелких случаях, но в целом это невыполнимо.

Если вы ищете что-то подобное, чтобы получить ответы на домашнее задание, перестаньте пытаться. (а) вы его не найдете и (б) задачи из этой книги довольно просты и могут быть интересными! Просто попробуйте и при необходимости обратитесь за помощью. и, конечно, (в) вы ничему не научитесь, если будете жульничать.