Модели и контрпримеры

Эта статья может чрезмерно полагаться на источники, слишком тесно связанные с темой , что потенциально делает статью непроверяемой и нейтральной . Пожалуйста , помогите улучшить ее, заменив их более подходящими ссылками на надежные, независимые источники . ( Март 2024 ) ( Узнайте, как и когда удалить это сообщение )

Models And Counter-Examples ( Mace ) — это поисковик моделей . ^[1] Большинство автоматизированных доказателей теорем пытаются выполнить доказательство опровержением на нормальной форме предложения задачи доказательства, показывая, что комбинация аксиом и отрицаемая гипотеза никогда не могут быть одновременно истинными, т. е. не имеют модели. С другой стороны, поисковик моделей, такой как Mace, пытается найти явную модель набора предложений. Если это удается, это соответствует контрпримеру для предположения, т. е. он опровергает (заявленную) теорему.

Mace распространяется по лицензии GNU GPL . ^[2]

• Выдра (доказатель теорем)
• Доказательство9

• Загрузка системы

Эта статья, связанная с логикой, является заглушкой . Вы можете помочь Википедии, расширив ее.

• в
• т
• е