Мейс означает « Модели и контрпримеры » и является средством поиска моделей . [1] Большинство автоматических средств доказательства теорем пытаются выполнить доказательство путем опровержения клаузульной нормальной формы проблемы доказательства, показывая, что комбинация аксиом и отрицаемой гипотезы никогда не может быть одновременно истинной, т. Е. Не имеет модели. С другой стороны, средство поиска моделей, такое как Мейс, пытается найти явную модель набора предложений. В случае успеха это соответствует контрпримеру для гипотезы, т.е. опровергает (заявленную) теорему.
Mace под лицензией GNU GPL . [2]
Смотрите также
Рекомендации
- ^ Домашний сайт Уильяма МакКьюна
- ^ См. КОПИРОВАНИЕ файла в архиве .