📑 Table of Contents▼

Models And Counter-Examples (Mace) is a model finder.[1] Most automated theorem provers try to perform a proof by refutation on the clause normal form of the proof problem, by showing that the combination of axioms 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 licensed.[2]

See also

edit

References

edit
  1. ^ William McCune home site
  2. ^ See COPYING file in the tarball.
edit
Stub icon

This logic-related article is a stub. You can help Wikipedia by adding missing information.

📚 Artikel Terkait di Wikipedia

Prover9

having a powerful hints strategy. Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples. Both can be run simultaneously

Automated theorem proving

paramodulation. Otter has since been replaced by Prover9, which is paired with Mace4. SETHEO is a high-performance system based on the goal-directed model elimination

William McCune

methods. He was best known for the development of the Otter, Prover9, and Mace4 automated reasoning systems, and the automated proof of the Robbins conjecture

Otter (theorem prover)

OTTER is written in approximately 28,000 lines of C programming language. Mace4 McCune, William (2003). Otter 3.3 Reference Manual (PDF). doi:10.2172/822573

Symbolic artificial intelligence

logic are: Prover9 ACL2 Vampire Prover9 can be used in conjunction with the Mace4 model checker. ACL2 is a theorem prover that can handle proofs by induction