E is a purely equational theorem prover for full first-order logic.
That means it is a program that you can stuff a mathematical
specification (in first-order format) and a hypothesis into, and which
will then run forever, using up all of your machines' resources. Very
occasionally it will find a proof for the hypothesis and tell you so.
E's inference core is based on a modified version of the superposition
calculus for equational clausal logic. Both clausification and
reasoning on the clausal form can be documented in checkable proof
E was the best-performing open source software prover in the 2008 CADE
ATP System Competition (CASC) in the FOF, CNF, and UEQ divisions. In
the 2011 competition, it won second place in the FOF division, and
placed highly in CNF and UEQ.
checkproof checkproof 1.9.1-001 Read an UPCL2 protocol and verify the inferences using one of a varity of external provers. This is a _very_ experimental program. Passing... e_axfilter e_axfilter 1.9.1-001 "Sungma" This problem applies SinE-like goal-directed filters to a problem specification to generate reduced problem specifications that... eground eground 1.9.1-001 Read a set of clauses and determine if it can be grounded (i.e. is either already ground or has no non-constant function symbols). If this is... ekb_create ekb_create 1.9.1-001 Create an empty knowledge base with name <name> for E. Options -h --helpPrint a short description of program usage and options. -V... ekb_delete ekb_delete 0.1dev Remove the example <name> from an E knowledge base. Options -h --helpPrint a short description of program usage and options. --versionPrint... ekb_ginsert ekb_ginsert 1.9.1-001 Generate a set of training examples from an E inference list (i.e. an EPCL trace of a proof run) and insert it into a knowledge base... ekb_insert ekb_insert 1.9.1-001 Insert example files into an E knowledge base. Each non-option argument is considered as one individual example file. For most applications... e_ltb_runner e_ltb_runner 1.9.1-001 "Sungma" Read a CASC 24 LTB batch specification file and process it. epclextract epclextract 1.9.1-001 Read an PCL2 protocol and print the steps necessary for proving the clauses in "proof", "final", or "extract" steps. Options -h... eproof eproof Eproof is a wrapper around E and epclextract. It will run E with output level 4 (full output of all potentially proof-relevant inferences) and, in the... eproof_ram eproof Eproof_ram is a wrapper around E and epclextract. It will run E with output level 4 (full output of all potentially proof-relevant inferences) and pipe... eprover E 1.9.1-001 "Sungma" Read a set of first-order clauses and formulae and try to refute it.