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.


References in zbMATH (referenced in 116 articles )

Showing results 1 to 20 of 116.
Sorted by year (citations)

1 2 3 4 5 6 next

  1. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Cardinality of relations and relational approximation algorithms (2016)
  2. Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: Order in implication zroupoids (2016)
  3. Hirsch, Robin; Jackson, Marcel; Mikulás, Szabolcs: The algebra of functions with antidomain and range (2016)
  4. Hoare, Tony; van Staden, Stephan; Möller, Bernhard; Struth, Georg; Zhu, Huibiao: Developments in concurrent Kleene algebra (2016)
  5. Kinyon, Michael K.; Kunen, Kenneth; Phillips, J.D.; Vojtěchovský, Petr: The structure of automorphic loops (2016)
  6. Kinyon, Michael; Stuhl, Izabella; Vojtěchovský, Petr: Half-isomorphisms of Moufang loops. (2016)
  7. Sankappanavar, Hanamantagouda P.: A note on regular De Morgan semi-Heyting algebras (2016)
  8. Torrens, Antoni: Semisimples in varieties of commutative integral bounded residuated lattices (2016)
  9. Araújo, João Pedro; Kinyon, Michael: A natural characterization of semilattices of rectangular bands and groups of exponent two. (2015)
  10. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Tool-based verification of a relational vertex coloring program (2015)
  11. Bergman, Clifford; Failing, David: Commutative idempotent groupoids and the constraint satisfaction problem. (2015)
  12. Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
  13. Brengos, Tomasz: Weak bisimulation for coalgebras over order enriched monads (2015)
  14. Dang, Han-Hing; Möller, Bernhard: Modal algebra and Petri nets (2015)
  15. Dang, Han-Hing; Möller, Bernhard B.: Extended transitive separation logic (2015)
  16. Drápal, Aleš; Griggs, Terry S.; Kozlik, Andrew R.: Pure Latin directed triple systems (2015)
  17. Furusawa, Hitoshi; Nishizawa, Koki: Multirelational representation theorems for complete idempotent left semirings. (2015)
  18. Guttmann, Walter: Infinite executions of lazy and strict computations (2015)
  19. Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
  20. Kinyon, Michael; Wanless, Ian M.: Loops with exponent three in all isotopes. (2015)

1 2 3 4 5 6 next