|
|
|
leanHaT is a compact automated theorem prover
for the first-order logic of Here and There (HT).
It is based on a sequent calculus for HT.
Features of leanHaT
-
Theorem prover for the first-order logic of Here and There (HT)
with equality.
-
Based on a sequent calculus for HT.
-
Proof search on the original formula structure.
-
Implemented in Prolog.
-
Sound and complete.
-
Decision procedure for the propositional fragment of HT.
-
Simple input format (leanCoP/nanoCoP or TPTP syntax).
-
Available under the GNU general public license.
leanHaT 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 leanHaT.
|
A Sequent Prover for the Logic of Here and There