8 lines
361 B
Text
8 lines
361 B
Text
|
A saturating 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.
|
||
|
|
|
||
|
|
WWW: http://www.eprover.org
|