Checker
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
- The latest version is checker2008v1c. It can be downloaded by clicking
here .
-
Former version, checker2008v1b could also be downloaded from
here .
- Read changelog here
- See grammar of our specification language: txt
/ ps
- See small examples
Running Checker
- Decompress archive, then run make.
- Prepare theorem prover config file.
We use geo_parameters for Geo theorem prover.
See this file for complete config description.
- Run ./checker -configfile prover_parameters -inputfile
examples/natded to see an example ( another one is examples/naturals).
Alternatively -inputfile could be ommited to read from stdin. Parameter
-configfile is mandatory.
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