IPC: An Intuitionistic Propositional Checker

			Klaus Weich

(adaptation to Coq 8: Pierre Letouzey  <[email protected]>)

NOTA BENE:
---------
These files have been developped by Klaus Weich during his PhD thesis
at LMU Munich, defended in 2001. Unfortunately, Klaus seems to have
quit academical research and has since been out of reach. In
particular, this nice work was not available on-line anymore. So I
(Pierre Letouzey) take the liberty to place it into Coq User's
Contributions, in order for it not to be definitively lost.
IF YOU HAPPEN TO CONTACT KLAUS WEICH, PLEASE ASK HIM WHETHER THIS IS OK
WITH HIM, OTHERWISE TELL HIM TO EMAIL ME.


DESCRIPTION:
-----------
(excerpt from K. Weich thesis)

This thesis treats proof search in intuitionistic propositional logic,
a fragment of any constructive type theory. We present new and more
efficient decision procedures for intuitionistic propositional
logic. They themselves are given by (non-formal) constructive proofs.
We take one of them to demonstrate that constructive type theory can
be used in practice to develop a real, efficient, but error-free proof
searcher. This was done by formally proving the decidability of
intuitionistic propositional logic in Coq; the proof searcher was
automatically extracted.


REFERENCES:
----------
Improving Proof Search in Intuitionistic Propositional Logic,
Klaus Weich, PhD thesis, 139 pages, 2001
ISBN 3-89722-767-3
Paper copy available at:
 http://www.logos-verlag.de/cgi-bin/engbuchmid?isbn=767&lng=deu&id=
Preis: 40.50 Eur

Decision Procedures for Intuitionistic Propositional Logic by Program Extraction,
Klaus Weich, TABLEAUX 1998, LNCS 1397, pages 292-306, 1998.
ISBN 3-540-64406-7


PRACTICAL DETAILS:
-----------------

Invoking `make` will compile the Coq files and perform the extraction. To
compile the benchmark program, run `make benchmark` (which requires the
`ocamlbuild` tool). This program can then be launched via
`./benchmark.native`. This will run a sequence of increasingly difficult
tests as long as these tests finish within 1 second of time. So the longer
the output is, the better the checker is.

By default, the checker doesn't build the derivations for the
formulae. This can be changed by changing in `Derivable_Def.v` the
`Require Import` command.