|
Здравствуйте.
В последнее время меня заинтересовала тема пруверов, т.к. сейчас изучаю методы доказательства теорем. В частности, пользуюсь Proof Designer из книги Vellman "How to Prove It" для доказательства различных утверждений и теорем в теории множеств.( Единственно, не могу понять как там доказывать утверждения по поводу отношений и их композиций, т.к. он вводит столько разных букв, что невозможно их потом сократить, например, в условии и цели доказательства. Не получается заменить чтобы получились одни и те же буквы).ю
Хотел бы спросить, кто пользуется, немного о них рассказать. Пока в примете Coq и Microsoft Lean. По последнему нашел книгу "Logic and Proof"
Jeremy Avigad, Robert Y.Lewis and Floris van Doorn. По Coq какая то более разбросанная информация в сети, ну книги не встречал по крайней мере. Хотел узнать о принципе доказательств в тех пруверах , где вы работаете (ну кто работает естественно). Т.е. можно ли выбирать стратегии доказательства, такие как контрпозиция в импликативных утверждениях, приведение к противоречию и т.д. , автоматическое преобразование определений, скажем , объединение множества представить как конъюнкцию двух переменных и т.д. , метод мат. индукции.
Кстати, в таких пакетах как Math или MatLab есть функции для работы с доказательствами?
|
