mirror of
https://git.FreeBSD.org/ports.git
synced 2024-10-20 20:09:11 +00:00
91d97411ae
PR: 211903 Submitted by: Greg V <greg@unrelenting.technology> Approved by: tcberner (mentor) Differential Revision: https://reviews.freebsd.org/D13150
8 lines
361 B
Plaintext
8 lines
361 B
Plaintext
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
|