Equational Theorem Prover

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

objects.

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...

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...

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...

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_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_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_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...

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.

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...

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 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...

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...