Intellectics Group: Technical Report 96-18
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 adapted to
deal with other non-classical logics.