Previous: AIDA-96-17 Next: AIDA-96-19 Index 1996

Intellectics Group: Technical Report 96-18

ileanTAP: An Intuitionistic Theorem Prover

Jens Otten

We present a Prolog program that implements a sound and complete theorem prover for first-order intuitionistic logic. It is based on free-variable semantic tableaux extended by an additional string unification to ensure the particular restrictions in intuitionistic logic. Due to the modular treatment of the different logical connectives the implementation can easily adapted to deal with other non-classical logics.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry