Some time ago, I've implemented a non visual version of the incredible proof machine: http://hediet.de/projects/predicate-logic-proof-validator/examples/index.h

Some time ago, I've implemented a non visual version of the incredible proof machine: http://hediet.de/projects/predicate-logic-proof-validator/examples/index.html?template=peano http://hediet.de/projects/predicate-logic-proof-validator/ex... Using the deduction theorem solver, you can easily generate solutions for some problems of the incredible proof machine.