Prover9

0
Ваша оценка: Нет

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

Сайт разработчика: http://www.cs.unm.edu/~mccune/mace4/
Что почитать?


Разместил: vikos 20 Июль 2012 в 09:37