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

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

1 2 3 ... 6 7 8 next

  1. Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: On implicator groupoids (2017)
  2. Glück, Roland: Algebraic investigation of connected components (2017)
  3. Greer, Mark: Semiautomorphic inverse property loops (2017)
  4. Harding, John; Romanowska, Anna B.: Varieties of Birkhoff systems. I (2017)
  5. Peltier, N.: A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules (2017)
  6. Ahmad, Imtiaz; Ahmad, Iftikhar; Rashad, Muhammad: A study of anti-commutativity in AG-groupoids (2016)
  7. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Cardinality of relations and relational approximation algorithms (2016)
  8. Bres, Emile; van Glabbeek, Rob; Höfner, Peter: A timed process algebra for wireless networks with an application in routing (extended abstract) (2016)
  9. Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: Order in implication zroupoids (2016)
  10. Cornejo, Juan M.; Sankappanavar, Hanamantagouda P.: Semisimple varieties of implication zroupoids (2016)
  11. Hirsch, Robin; Jackson, Marcel; Mikulás, Szabolcs: The algebra of functions with antidomain and range (2016)
  12. Hoare, Tony; van Staden, Stephan; Möller, Bernhard; Struth, Georg; Zhu, Huibiao: Developments in concurrent Kleene algebra (2016)
  13. Höfner, Peter; Möller, Bernhard: Extended feature algebra (2016)
  14. Kinyon, Michael K.; Kunen, Kenneth; Phillips, J.D.; Vojtěchovský, Petr: The structure of automorphic loops (2016)
  15. Kinyon, Michael; Stuhl, Izabella; Vojtěchovský, Petr: Half-isomorphisms of Moufang loops. (2016)
  16. Padmanabhan, Ranganathan; Zhang, Yang: Automated deduction in ring theory (2016)
  17. Reger, Giles; Suda, Martin; Voronkov, Andrei: Finding finite models in multi-sorted first-order logic (2016)
  18. Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
  19. Sankappanavar, Hanamantagouda P.: A note on regular De Morgan semi-Heyting algebras (2016)
  20. Santocanale, Luigi: Relational lattices via duality (2016)

1 2 3 ... 6 7 8 next