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

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

1 2 3 ... 9 10 11 next

  1. East, James; Gray, Robert D.: Ehresmann theory and partition monoids (2021)
  2. Jackson, Marcel; Stokes, Tim: Override and update (2021)
  3. Wehrung, Friedrich: Right-orderability versus left-orderability for monoids (2021)
  4. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  5. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  6. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  7. Cvetko-Vah, Karin; Verwimp, Charlotte: Skew lattices and set-theoretic solutions of the Yang-Baxter equation (2020)
  8. Didurik, Natalia; Shcherbacov, Victor: Units in quasigroups with classical Bol-Moufang type identities. (2020)
  9. Drápal, Aleš; Vojtěchovský, Petr: Division sudokus: invariants, enumeration, and multiple partitions (2020)
  10. Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
  11. Gil-Férez, José; Jipsen, Peter; Metcalfe, George: Structure theorems for idempotent residuated lattices (2020)
  12. Greer, Mark; Raney, Lee: Automorphic loops and metabelian groups. (2020)
  13. Jedlička, Přemysl; Pilitowska, Agata; Zamojska-Dzienio, Anna: The construction of multipermutation solutions of the Yang-Baxter equation of level 2 (2020)
  14. Kozlik, Andrew R.: The centre of a Steiner loop and the maxi-Pasch problem. (2020)
  15. Lucas, Salvador: Using well-founded relations for proving operational termination (2020)
  16. Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques (2020)
  17. Araújo, João; Kinyon, Michael; Robert, Yves: Varieties of regular semigroups with uniquely defined inversion (2019)
  18. Bright, Curtis; Đoković, Dragomir Ž.; Kotsireas, Ilias; Ganesh, Vijay: The SAT+CAS method for combinatorial search with applications to best matrices (2019)
  19. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  20. Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: Symmetric implication zroupoids and weak associative laws (2019)

1 2 3 ... 9 10 11 next