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 227 articles )

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

1 2 3 ... 10 11 12 next

  1. Smith, Jonathan D. H.; Vojtěchovský, Petr: Okubo quasigroups (2022)
  2. Stokes, Tim: ((\mathscrF,\mathscrG))-abundant semigroups (2022)
  3. Abbadini, Marco: Equivalence à la Mundici for commutative lattice-ordered monoids (2021)
  4. Araújo, Maria Leonor; Araújo, Maria Teresa; Kinyon, Michael: The solution of an open problem on semigroup inclusion classes (2021)
  5. Bergstra, Jan A.; Ponse, Alban; Staudt, Daan J. C.: Non-commutative propositional logic with short-circuit evaluation (2021)
  6. Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: Semidistributivity and whitman property in implication zroupoids (2021)
  7. East, James; Gray, Robert D.: Ehresmann theory and partition monoids (2021)
  8. Griggs, Terry S.; Kozlik, Andrew R.: On quasigroups satisfying Stein’s third law (2021)
  9. Jackson, Marcel; Stokes, Tim: Override and update (2021)
  10. Jipsen, Peter; Tuyt, Olim; Valota, Diego: The structure of finite commutative idempotent involutive residuated lattices (2021)
  11. Macke, Jaroslav; Sedlar, Jiri; Olsak, Miroslav; Urban, Josef; Sivic, Josef: Learning to solve geometric construction problems from images (2021)
  12. Margolis, Stuart; Stein, Itamar: Ehresmann semigroups whose categories are EI and their representation theory (2021)
  13. Merlini Giuliani, Maria de Lourdes; Oliveira Cortes, Wagner de: On loopoids and magma with inverse (2021)
  14. Santocanale, Luigi: Dualizing sup-preserving endomaps of a complete lattice (2021)
  15. Sawicki, Damian; Grabowski, Adam: On weakly associative lattices and near lattices (2021)
  16. Wehrung, Friedrich: Right-orderability versus left-orderability for monoids (2021)
  17. Wernhard, Christoph: Craig interpolation with clausal first-order tableaux (2021)
  18. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  19. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  20. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)

1 2 3 ... 10 11 12 next