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.1.3 of E-KRHyper is available for download here. See included "this_version.txt" for further details (last update: 20.07.2009)
Test Results (dated, revision forthcoming)
Home