# 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' 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.

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