## About Prooftoys

### The mission

Prooftoys 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.
### Introduction

Prooftoys in its current form can be used in two rather different but
related ways. It can be used to explore and create simple proofs in
mathematical logic. Or it can be used as a tool to help in solving
basic algebra problems.

### Algebra in Prooftoys

For practice with algebra problem solving, try the
Mathtoys website. That site is powered by the
same Prooftoys software that powers this one, but the
Mathtoys site is dedicated to
helping you solve algebra problems.

### Logic in Prooftoys

The Basic Logic through Pictures, is an
introduction to some fundamental ideas of classical logic with
interactive illustrations.

The Introduction to Proofs page is a
good first step toward reading Prooftoys proofs and building your own.

There is quite a bit more yet to be said about the 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 engine

The 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'
Q_{0}, 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.

### Further steps

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.