Какие функции я хочу видеть:
1.Способность доказать или опровергнуть истинность высказывания (логической формулы) на основе постулирования истинности неких других высказываний. То есть, я ввожу несколько высказываний (с помощью специального синтаксиса, вроде синтаксиса мат. логики) чья истинность принимается на веру, после чего даю программе команду попытаться доказать что некое новое высказывание противоречит им или же следует из них. Желательно чтобы в случае успеха программа показала подробный «ход своей мысли», дабы было понятно почему новое высказывание входит в противоречие с уже принятыми или почему оно следует из них в результате дедукции.
2.Самостоятельная дедукция без подсказок. Я ввожу несколько высказываний чья истинность принимается на веру, после чего даю программе команду вывести все возможные следствия из них. Желательно чтобы в случае успеха программа подробно расписала свою дедукцию, дабы было понятно как то или иное высказывание является следствием уже принятых высказываний.