The missionProoftoys is an open-source effort to use the Web to bring user-friendly full-fledged logical reasoning tools to anyone who works with math. The current components are the engine and the user interface. They are both under continuing development and important work remains to be done on both, but are available for experimental use.
The Basic Logic through Pictures, is an introduction to some fundamental ideas of classical logic with interactive illustrations.
The Introduction page is a good first step toward A good first step toward reading Prooftoys proofs and building your own.
There is quite a bit more yet to be said about our logic as well. Fortunately the logic and inference steps are quite standard, so any part that looks familiar should work for you in textbook fashion.
The user interface
In the web-based Proof Builder user interface you can select steps, expressions, and locations in steps by pointing and clicking, and apply any predefined or extended public inference rule. When reading an existing proof you can drill down into the details of high-level inference steps or theorems to see how they are proved in more detail.
The engineThe Prooftoys inference engine uses higher-order logic, which means it can reason about functions and predicates, which themselves can have functions and predicates as inputs and outputs. This gives it the power to help you develop as much of mathematics as you wish. The engine runs directly in your web browser for best responsiveness, interactivity, and convenient access to servers in the Internet cloud.
The engine implements a variant of Professor Peter B. Andrews' Q0, a version of higher-order logic with a small, simple, and understandable kernel. On this base it builds natural deduction-style reasoning and a variety high-level inference rules that make it easy to build high-level proofs.
The engine is safely programmable, and you can create new high-level inference rules without compromising correctness.
The Proof builder is also available on a standalone page.
Note: Proof displays and the proof builder are supported in recent versions of Firefox and Chrome.
An Introduction to Mathematical Logic and Type Theory by Professor Andrews contains a rigorous presentation of the full logic implemented here among other logical topics.