Checker is a small framework for proof checking, based on first-order logic with schematic quantifications. It has a few natural deduction-style rules, that can deal witch those schematic formulas, and a mechanism for definition handling. It has no types essentially, but identifiers must be declared before use. First order reasoning is done by an external theorem prover. The Checker is described in a paper A Small Framework for Proof Checking by Hans de Nivelle and me.

Download Checker

Running Checker

Plans for Nearest Future

We intend to play with checker and make it more convenient to use. We would also like to compare usefulness of different theorem provers as components of interactive proof systems. To accomplish this some practical verification tasks are in progress.
Return to Piotr Witkowski's homepage.
Content last modified: Sat Aug 9 2008 10.25