Models_And_Counter-Examples

Models And Counter-Examples

Models And Counter-Examples

Computer software for model generation

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

References

  1. [1]
    William McCune home site
  2. [2]
    See COPYING file in the tarball.
Stub icon

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

This article uses material from the Wikipedia article Models_And_Counter-Examples, and is written by contributors. Text is available under a CC BY-SA 4.0 International License; additional terms may apply. Images, videos and audio are available under their respective licenses.