// Workers AI · dad joke modeWhy did Models And Counter-Examples go to therapy? It had conflicting views.
(Redirected from Mace4)
 | This article may rely excessively on sources too closely associated with the subject, potentially preventing it from being verifiable and neutral. (March 2024) |
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.
See also
[edit]References
[edit]- ↑ William McCune home site
- ↑ See COPYING file in the tarball.
External links
[edit] | This logic-related article is a stub. You can help Wikipedia by adding missing information. |