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