Программы для логического вывода в различный системах

[Dr4kon]

Ищу аналоги программы deductio: http://logic.ru/ru/node/291
Я так понял, что к программам типа Mathcad, Matlab можно писать модули. Так вот вопрос: есть-ли какие-нибудь современные аналоги deductio, или модули для Mathcad/Matlab?

[Dims]

С deductio не знаком.

Я знаю, что Mathematica умеет решать логические выражения. Не знаю, насколько глубоко, но предикаты можно задавать, упрощать можно и т.п.

Насколько я слышал, перспективный доказыватель теорем, это

http://en.wikipedia.org/wiki/Coq

Точнее, это не доказыватель, а помощник доказывателя. Вроде бы, он очень мощный. Но я не разобрался в нём, слишком заумно.

Добавлено спустя 2 минуты 51 секунду:

P.S. В Coq точно можно свои аксиоматики задавать.

[luitzen]

Нашёл у себя в каталоге Provers такие подкаталоги: STRIP, ACL, Gandalf, Isabelle, Otter.

Большое количество разных штуковин упомянуто тут.

[Dr4kon]

luitzen писал(а):

Нашёл у себя в каталоге Provers такие подкаталоги: STRIP, ACL, Gandalf, Isabelle, Otter.

Большое количество разных штуковин упомянуто тут.

Отлично. Как можно попасть в Ваш каталог Provers?

[luitzen]

Dr4kon писал(а):

Отлично. Как можно попасть в Ваш каталог Provers?

Туда даже Coq, упомянутый Dims’ом, не попал. Где уж Вам-то, неофиту .