Models And Counter-Examples (Mace) is a
model
A model is an informative representation of an object, person, or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin , .
Models can be divided in ...
finder.
Most
automated theorem prover
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ma ...
s try to perform a proof by refutation on the
clause normal form of the proof problem, by showing that the combination of
axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
s and negated conjecture can never be simultaneously true, i.e. does not have a model. A model finder such as Mace, on the other hand, tries to find an explicit model of a set of clauses. If it succeeds, this corresponds to a counter-example for the conjecture, i.e. it disproves the (claimed) theorem.
Mace is
GNU GPL
The GNU General Public Licenses (GNU GPL or simply GPL) are a series of widely used free software licenses, or ''copyleft'' licenses, that guarantee end users the freedom to run, study, share, or modify the software. The GPL was the first ...
licensed.
See also
*
Otter (theorem prover)
*
Prover9 Prover9 is an automated theorem proving, automated theorem prover for first-order logic, first-order and equational logic developed by William McCune.
Description
Prover9 is the successor of the Otter (theorem prover), Otter theorem prover also dev ...
References
External links
System download
Free theorem provers
Software using the GNU General Public License
{{logic-stub