The scientific man does not aim at an immediate result. He does not expect that his advanced ideas will be readily taken up. His work is like that of the planter – for the future. His duty is to lay the foundation for those who are to come, and point the way. — Nikola Tesla
About Prooftoys.org
Welcome! The Prooftoys website and its software are ongoing experiments in creating computer aids to help human beings learn and do mathematics. The application software is proudly open source, hosted at Github, primarily in the crisperdue/prooftoys repository.
The key goal is to create a computer math tool or tools that are easy, highly available, useful, attractive, and valuable to people learning (or doing) mathematics, especially newcomers, for reading and writing proofs, and for solving problems deductively.
The larger vision is to develop the kind of user experience that can bridge the gap between computer proof technology and ordinary people learning to understand and use mathematics.
About the logic
At its core, the reasoning in Prooftoys is equational, in other words based on equations. In particular Leibniz’s principle of replacing a term with an equal term is fundamental, as applied in algebra from the basic high school level and up.
Prooftoys implements a form of logic known as simple type theory. Anything provable in “first-order” logic remains provable. Furthermore, reasoning about equality is not an add-on, in fact it is the core. General statements about functions and predicates can also be expressed and proved here, unlike first-order logic.
This particular system is based rather directly on the Q0 system of Carnegie Mellon University Professor Peter B. Andrews. See the tech notes for more details.
Working with a logic textbook
Yes, you should be able to use the Proof Builder tool with your logic textbook. If your textbook presents problems to solve by formally proving or disproving statements in pure logic, the intention is that you will solve the problems using the rules laid out in the textbook.
To do this, you will need to be careful to limit the inference steps and logic facts you use. This page has details for a couple of examples I have seen reference.
Getting in touch
One goal is to develop a friendly community of users around the tools here and their goals of using computers for mathematical reasoning. Don’t hesitate to say “hello” to the author through email.
Sincerely,
Cris Perdue