×

Mace4

swMATH ID: 6905
Software Authors: William McCune
Description: 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.
Homepage: http://www.mcs.anl.gov/research/projects/AR/mace4/
Keywords: finite model
Related Software: Prover9; OTTER; TPTP; GAP; VAMPIRE; E Theorem Prover; SPASS; Isabelle/HOL; LOOPS; Coq; MiniSat; Isabelle; Sledgehammer; E-Darvin; FINDER; OEIS; Mizar; z3; HR; Chaff
Referenced in: 231 Publications
all top 5

Referenced by 248 Authors

21 Kinyon, Michael K.
14 Höfner, Peter
12 Vojtěchovský, Petr
11 Möller, Bernhard
9 Colton, Simon
9 Sankappanavar, Hanamantagouda P.
9 Urban, Josef
8 Struth, Georg
7 Cornejo, Juan Manuel
7 Lucas, Salvador
7 McCune, William W.
6 Araújo, João
6 Fiala, Nick C.
6 Jipsen, Peter
6 Kozlik, Andrew Richard
6 Sorge, Volker
5 Baumgartner, Peter
5 Berghammer, Rudolf
5 Greer, Mark R.
5 Griggs, Terry S.
5 Gutiérrez, Raúl
5 Kaliszyk, Cezary
5 Meier, Andreas
5 Padmanabhan, Ranganathan
4 Cvetko-Vah, Karin
4 Dang, Han-Hing
4 Drápal, Aleš
4 Guttmann, Walter
4 Lisitsa, Alexei P.
4 McCasland, Roy L.
4 Santocanale, Luigi
4 Schulz, Stephan
4 Sutcliffe, Geoff
3 Agre, Keith M.
3 Fitelson, Branden
3 Furusawa, Hitoshi
3 Grabowski, Adam
3 Harding, John
3 Hoare, C. A. R. Tony
3 Jedlička, Přemysl
3 Peltier, Nicolas
3 Stokes, Timothy E.
3 Stucke, Insa
3 Tinelli, Cesare
3 Wehrung, Friedrich
3 Zhang, Hantao
2 Blanchette, Jasmin Christian
2 Bonacina, Maria Paola
2 Claessen, Koen
2 Cristiá, Maximiliano
2 de Nivelle, Hans
2 Dunets, Andriy
2 Fuchs, Alexander
2 Furbach, Ulrich
2 Jackson, Marcel G.
2 Jakubův, Jan
2 Kunen, Kenneth
2 Leech, Jonathan Edmund
2 Lillieström, Ann
2 Melo de Sousa, Simão
2 Moreira, Nelma
2 Nishizawa, Koki
2 Olšák, Miroslav
2 Paulson, Lawrence Charles
2 Pease, Adam
2 Pennemann, Karl-Heinz
2 Pereira, David P.
2 Pilitowska, Agata
2 Ponse, Alban
2 Pula, Kyle
2 Raney, Lee
2 Reif, Wolfgang
2 Rossi, Gianfranco
2 Sawicki, Damian
2 Schellhorn, Gerhard
2 Schmidt, Renate A.
2 Spinks, Matthew
2 Staudt, Daan J. C.
2 Stein, Itamar
2 Veroff, Robert
2 Voronkov, Andrei
2 Walker, Carol L.
2 Walker, Elbert Abner
2 Wehrman, Ian
2 Zamojska-Dzienio, Anna
1 Aameri, Bahar
1 Abbadini, Marco
1 Ahmad, Iftikhar
1 Ahmad, Imtiaz
1 Akhtar, Reza
1 Alama, Jesse
1 Alpay, Natanael
1 Andréka, Hajnal
1 Araújo, João Pedro
1 Araújo, Maria Leonor
1 Araújo, Maria Teresa
1 Arthan, Rob D.
1 Audemard, Gilles
1 Benhamou, Belaid
1 Bennett, Frank E.
...and 148 more Authors
all top 5

Referenced in 60 Serials

17 Journal of Automated Reasoning
11 Algebra Universalis
9 Journal of Algebra
9 Semigroup Forum
9 Journal of Logical and Algebraic Methods in Programming
7 Commentationes Mathematicae Universitatis Carolinae
5 Communications in Algebra
5 Discrete Mathematics
4 Soft Computing
4 The Journal of Logic and Algebraic Programming
3 Journal of Pure and Applied Algebra
3 Studia Logica
3 Order
3 Journal of Symbolic Computation
3 Annals of Mathematics and Artificial Intelligence
3 Quasigroups and Related Systems
3 Journal of Applied Logic
3 Formalized Mathematics
2 Acta Informatica
2 Artificial Intelligence
2 Information Processing Letters
2 Journal of Philosophical Logic
2 Transactions of the American Mathematical Society
2 European Journal of Combinatorics
2 Journal of Logic and Computation
2 The Australasian Journal of Combinatorics
2 Journal of Applied Non-Classical Logics
2 Journal of Combinatorial Designs
1 Computers & Mathematics with Applications
1 Houston Journal of Mathematics
1 Beiträge zur Algebra und Geometrie
1 Ars Combinatoria
1 Czechoslovak Mathematical Journal
1 Demonstratio Mathematica
1 Glasgow Mathematical Journal
1 Journal of Combinatorial Theory. Series A
1 The Journal of Symbolic Logic
1 Mathematica Slovaca
1 Pacific Journal of Mathematics
1 Programming and Computer Software
1 Topology and its Applications
1 Advances in Applied Mathematics
1 Science of Computer Programming
1 Note di Matematica
1 JCMCC. The Journal of Combinatorial Mathematics and Combinatorial Computing
1 AI Communications
1 Machine Learning
1 International Journal of Algebra and Computation
1 MSCS. Mathematical Structures in Computer Science
1 Journal of Mathematics. The Punjab University
1 Documenta Mathematica
1 Constraints
1 Portugaliae Mathematica. Nova Série
1 Journal of Algebra and its Applications
1 Parallel Processing Letters
1 Lecture Notes in Computer Science
1 Logical Methods in Computer Science
1 Journal of Formalized Reasoning
1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
1 Distinguished Dissertations

Referencing Publications by Year