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 173 articles )
Showing results 41 to 60 of 173.
Sorted by year (- Brock-Nannestad, Taus; Chaudhuri, Kaustuv: Disproving using the inverse method by iterative refinement of finite approximations (2015)
- Dang, Han-Hing; Möller, Bernhard: Modal algebra and Petri nets (2015)
- Dang, Han-Hing; Möller, Bernhard B.: Extended transitive separation logic (2015)
- Drápal, Aleš; Griggs, Terry S.; Kozlik, Andrew R.: Pure Latin directed triple systems (2015)
- Furusawa, Hitoshi; Nishizawa, Koki: Multirelational representation theorems for complete idempotent left semirings. (2015)
- Guttmann, Walter: Infinite executions of lazy and strict computations (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kinyon, Michael; Wanless, Ian M.: Loops with exponent three in all isotopes. (2015)
- Moreira, Nelma; Pereira, David; Melo de Sousa, Simão: Deciding Kleene algebra terms equivalence in Coq (2015)
- Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
- Araújo, João; Kinyon, Michael: Inverse semigroups with idempotent-fixing automorphisms. (2014)
- Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Automated verification of relational while-programs (2014)
- Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C.: Machine learning for first-order theorem proving (2014)
- Drápal, Aleš; Griggs, Terry S.; Kozlik, Andrew R.: Triple systems and binary operations (2014)
- Fish, Andrew; Lisitsa, Alexei: Detecting unknots via equational reasoning. I: Exploration (2014)
- Greer, Mark: A class of loops categorically isomorphic to Bruck loops of odd order. (2014)
- Greer, Mark; Raney, Lee: Moufang semidirect products of loops with groups and inverse property extensions. (2014)
- Höfner, Peter; McIver, Annabelle: Hopscotch -- reaching the target hop by hop (2014)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
- Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014) ioport