View source for Models And Counter-Examples

{{Short description|Computer software for model generation}}
{{Third-party|date=March 2024}}
'''Models And Counter-Examples''' ('''Mace''') is a [[model theory|model]] finder.<ref name="McCuneHome"/>  Most [[automated theorem prover]]s try to perform a proof by refutation on the [[clause normal form]] of the proof problem, by showing that the combination of [[axiom]]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]] licensed.<ref name="TARBALL"/>
== See also ==
* [[Otter (theorem prover)]]
* [[Prover9]]
== References ==
{{reflist|refs=
<ref name="McCuneHome">[http://www.cs.unm.edu/~mccune/ William McCune home site]</ref>
<ref name="TARBALL">See COPYING file in the [http://www.cs.unm.edu/~mccune/mace4/download/LADR-2009-11A.tar.gz tarball].</ref>
}}
== External links ==
* [http://www.cs.unm.edu/~mccune/mace4/ System download]
[[Category:Free theorem provers]]
[[Category:Software using the GPL license]]
{{logic-stub}}