Jump to content

Models And Counter-Examples

Add links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Djm-leighpark (talk | contribs) at 22:48, 11 November 2018 (wikilink). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Mace stands for "Models And Counter-Examples", and 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]

References

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

See also

Stub icon

This logic-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Models_And_Counter-Examples&oldid=868394574"