Mace4
finite model-finder Mace4. 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 our previous model-searching program Mace2.
Keywords for this software
References in zbMATH (referenced in 186 articles )
Showing results 1 to 20 of 186.
Sorted by year (- Bright, Curtis; Đoković, Dragomir Ž.; Kotsireas, Ilias; Ganesh, Vijay: The SAT+CAS method for combinatorial search with applications to best matrices (2019)
- Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: Symmetric implication zroupoids and weak associative laws (2019)
- Goodman, Jeremy: Agglomerative algebras (2019)
- Greer, Mark: Simple right conjugacy closed loops (2019)
- Jedlička, Přemysl; Pilitowska, Agata; Zamojska-Dzienio, Anna: The retraction relation for biracks (2019)
- Jipsen, Peter; Kinyon, Michael: Nonassociative right hoops (2019)
- Kinyon, Michael: Proof simplification and automated theorem proving (2019)
- Lucas, Salvador: Proving semantic properties as first-order satisfiability (2019)
- Phillips, J. D.: Moufang and commutant elements in magmas (2019)
- Reis, Giselle; Woltzenlogel Paleo, Bruno: Complexity of translations from resolution to sequent calculus (2019)
- Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
- Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: Symmetric implication zroupoids and identities of Bol-Moufang type (2018)
- Cristiá, Maximiliano; Rossi, Gianfranco: A set solver for finite set relation algebra (2018)
- Donovan, Diane M.; McCourt, Thomas A.; Griggs, Terry S.; Kozlik, Andrew R.: Types of directed triple systems (2018)
- Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef: Proofwatch: watchlist guidance for large theories in E (2018)
- Grabowski, Adam; Sawicki, Damian: On two alternative axiomatizations of lattices by McKenzie and Sholander (2018)
- Huang, Pei; Ma, Feifei; Ge, Cunjing; Zhang, Jian; Zhang, Hantao: Investigating the existence of large sets of idempotent quasigroups via satisfiability testing (2018)
- Lisitsa, Alexej P.: The Andrews-Curtis conjecture, term rewriting and first-order proofs (2018)
- Lucas, Salvador; Gutiérrez, Raúl: Use of logical models for proving infeasibility in term rewriting (2018)
- Ponse, Alban; Staudt, Daan J. C.: An independent axiomatisation for free short-circuit logic (2018)