E-KRHyper

E-KRHyper is a model generator and theorem prover for first-order logic with equality. It is an extended version of Christoph Wernhard's KRHyper system and implements the new E-Hyper tableaux calculus.

E-KRHyper is in a functional state, but always undergoing optimization.

The current version 1.2 of E-KRHyper is available for download here. See included "this_version.txt" for further details (last update: 31.01.2012)

Home