Prover9 является автоматическим построителем доказательства теорем для логики первого порядка и эквациональной логики. В нем используются методы вывода упорядоченных резолюций и парамодуляций с буквальным выбором.
Пакет Prover9 предоставляет программу построения доказательств теорем методом резолюций/парамодуляции Prover9 и генератор контрмоделей Mace4.
Имеются интерфейс командной строки (LADR) и графический интерфейс
Сайт разработчика:
Что почитать?
Разместил: