![cover image](https://wikiwandv2-19431.kxcdn.com/_next/image?url=https://upload.wikimedia.org/wikipedia/commons/thumb/0/0d/CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png/640px-CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png&w=640&q=50)
Инструмент интерактивного доказательства теорем
Материал из Википедии — свободной encyclopedia
Инструмент интерактивного доказательства теорем (интерактивный решатель теорем) — программное обеспечение, помогающее исследователю в разработке формальных доказательств. Доказательства вырабатываются в процессе взаимодействия человека с машиной. Как правило, такое программное обеспечения включает в себя какую-то разновидность интерактивного редактора доказательств или другой интерфейс, с помощью которого человек может вести поиск доказательств, сведения о которых хранятся в компьютере, а также процедуры автоматической проверки доказательств, осуществляемые компьютером.
Эту страницу предлагается переименовать в «Система интерактивного доказательства». |
![](http://upload.wikimedia.org/wikipedia/commons/thumb/0/0d/CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png/640px-CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png)