TL;DR
Mace4 is a software tool that efficiently searches for finite models of first-order formulas, complementing theorem provers by finding countermodels and aiding in finite algebra research.
Contribution
This paper introduces Mace4, a new model-searching program that improves performance on equational problems compared to its predecessor Mace2.
Findings
Mace4 successfully finds finite models for various first-order formulas.
It performs better on equational problems than Mace2.
Mace4 is useful for finite algebra work and complements theorem provers.
Abstract
Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than did our previous model-searching program Mace2.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.