nanoCoP-i-HT is a compact automated theorem prover for intuitionistic first-order logic and the first-order logic of Here and There (HT). It is based on the non-clausal connection calculus for intuitionistic logic and extends the classical nanoCoP prover.

Features of nanoCoP-i-HT

• Theorem prover for first-order intuitionistic and HT logic with equality.
• Based on the intuitionistic non-clausal connection calculus.
• Proof search on the original formula structure.
• Implemented in Prolog.
• Sound (but not complete for HT).
• Good performance.
• Simple input format (nanoCoP or TPTP syntax).
• Available under the GNU general public license.

nanoCoP-i-HT 2.0 runs on ECLiPSe Prolog (5.x) and on SWI-Prolog. It should run on most other Prolog systems as well. The ReadMe file contains more information on installing and running nanoCoP-im.

• nanoCoP-i-HT.tar.gz (tar/gzip, 12.1 kbytes)

ileanTAP-i-HT is a compact automated theorem prover for intuitionistic first-order logic and the first-order logic of Here and There (HT). It is based on a free-variable semantic tableau extended by an additional prefix unification. It runs on the open source Prolog system ECLiPSe.

• ileanTAP-HT.tar.gz (tar/gzip, 5.8 kbytes)

ileanSeP-i-HT is a compact automated theorem prover for intuitionistic first-order logic and the first-order logic of Here and There (HT). It is based on a single-succedent intuitionistic sequent calculus, very similar to Gentzen's LJ. It runs on the open source Prolog system ECLiPSe.

• ileanSeP-HT.tar.gz (tar/gzip, 5.2 kbytes)