2001/06/19 by William McCune, McCune, William
Computer Science · #FOS: Computer and information sciences #I.2.3 #I.2.8 #Logic in Computer Science (cs.LO) #Service-Oriented Architecture and Web Services #Symbolic Computation (cs.SC) #cs.LO #cs.SC
paper · pdf · doi:10.48550/arxiv.cs/0106042
10 pages
arxiv created 2001/06/19 · openalex publication_date 2001/06/19 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
MACE is a program that searches for finite models of first-order statements. The statement to be modeled is first translated to clauses, then to relational clauses; finally for the given domain size, the ground instances are constructed. A Davis-Putnam-Loveland-Logeman procedure decides the propositional problem, and any models found are translated to first-order models. MACE is a useful complement to the theorem prover Otter, with Otter searching for proofs and MACE looking for countermodels.