nanoCoP-i is a compact automated theorem prover
for intuitionistic first-order logic. It is based on the non-clausal
connection calculus for intuitionistic logic and extends the
classical nanoCoP prover.
More details about the calculus can be found in the
documentation.
Features of nanoCoP-i
-
Theorem prover for intuitionistic first-order logic with equality.
-
Based on the intuitionistic non-clausal connection calculus.
-
Proof search on the original formula structure.
-
Implemented in Prolog.
-
Sound and complete.
-
Leading performance.
-
Simple input format (nanoCoP or TPTP syntax).
-
Output of readable non-clausal connection proof (v2.0).
-
Available under the GNU general public license.
nanoCoP-i 2.0
contains several enhancements and optimizations of the basic
non-clausal connection calculus, such as improved restricted
backtracking and a strategy scheduling.
nanoCoP-i 2.0
can output a detailed non-clausal connection proof in different
formats, for example in a Prolog syntax or in a readable format.
nanoCoP-i 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-i.
nanoCoP-i 1.0 implements the basic non-clausal connection calculus
and a few optimizations. It runs on the open source Prolog system
ECLiPSe.
The following package includes a
ReadMe file containing
more information.
|