Models And Counter-Examples

Models And Counter-Examples is a model finder. 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 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 theorem.
Mace is GNU GPL licensed.