blob: aea9f022fa48911bea49383a6ba8035212f0a4e6 (
plain) (
tree)
|
|
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.
|