Questions tagged [e-theorem-prover]
E is a theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms. (From wwwlehre.dhbw-stuttgart.de)
1
question
7
votes
1
answer
122
views
Understanding "saturating" theorem provers
The documentation for the E Theorem Prover explains this as the first step in its process:
A clausification algorithm translates first-order input into clause
normal form, such that the resulting ...
- 519