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