Models And Counter-Examples

Short description: Computer software for model generation

This article may rely excessively on sources too closely associated with the subject, potentially preventing the article from being verifiable and neutral. Please help improve it by replacing them with more appropriate citations to reliable, independent, third-party sources. (March 2024) (Learn how and when to remove this template message)

|

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

* Otter (theorem prover)
* Prover9

## References

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

## External links

* System download

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Models And Counter-Examples. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Software:Models_And_Counter-Examples&oldid=3953733"