ileanTAP: An Intuitionistic Theorem Prover

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 be adapted to deal with other non-classical logics.

• Type: Conference
• Year: 1997
• Where: TABLEAUX
• Authors: Jens Otten
• Keywords: Artificial Intelligence, Complete Theorem Prover, Intuitionistic Logic, TABLEAUX 1997, first-order Intuitionistic Logic