×

zbMATH — the first resource for mathematics

MACE4 and SEM: a comparison of finite model generators. (English) Zbl 1383.68083
Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 101-130 (2013).
Summary: This article has three objectives: (1) Promote Mace4, a program developed by Bill McCune that searches for finite models of first-order formulas and that is the best way to remember Bill. (2) Promote the research on model generation of first-order formulas. Mace4 remains one of the best model generation programs and we need newcomers who can take over Bill’s torch, because model generation is very important to automated reasoning and has many applications. (3) Compare Mace4 with SEM in detail so that the users of these tools or new model generator developers will understand the strengths and weaknesses of both systems and take advantage from this study.
For the entire collection see [Zbl 1259.68002].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Audemard, G., Benhamou, B.: Reasoning by Symmetry and Function Ordering in Finite Model Generation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, p. 226. Springer, Heidelberg (2002) · Zbl 1072.68561 · doi:10.1007/3-540-45620-1_19
[2] Audemard, G., Benhamou, B., Henocque, L.: Predicting and Detecting Symmetries in FOL Finite Model Search. Journal of Automated Reasoning 36(3), 177–212 (2006) · Zbl 1107.68092 · doi:10.1007/s10817-006-9040-3
[3] Audemard, G., Henocque, L.: The eXtended Least Number Heuristic. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 427–442. Springer, Heidelberg (2001) · Zbl 0988.68605 · doi:10.1007/3-540-45744-5_35
[4] Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solver. In: Twenty-First International Joint Conference on Artificial Intelligence, IJCAI 2009 (2009)
[5] Baumgartner, P., Fuchs, A., De Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. of Applied Logic 7(1), 58–74 (2009) · Zbl 1171.68040 · doi:10.1016/j.jal.2007.07.005
[6] Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol. 2741, pp. 350–364. Springer, Heidelberg (2003) · Zbl 1278.68249 · doi:10.1007/978-3-540-45085-6_32
[7] Benhamou, B., Henocque, L.: A new method for finite model search in equational theories: FMSET system. Fundamenta Informaticae 39(1,2), 21–38 (1999) · Zbl 0951.68172
[8] Bennett, F.E., Du, B., Zhang, H.: Existence of conjugate orthogonal diagonal Latin squares. J. Combin. Designs 5, 449–461 (1997) · Zbl 0912.05018 · doi:10.1002/(SICI)1520-6610(1997)5:6<449::AID-JCD6>3.0.CO;2-F
[9] Bennett, F.E., Du, B., Zhang, H.: Existence of self-orthogonal diagonal Latin squares with a missing subsquare. Discrete Math. 261, 69–86 (2003) · Zbl 1012.05042 · doi:10.1016/S0012-365X(02)00461-2
[10] Bennett, F.E., Zhu, L.: Conjugate-orthogonal Latin squares and related structures. In: Dinitz, J., Stinson, D. (eds.) Contemporary Design Theory: A Collection of Surveys, pp. 41–96. Wiley, New York (1992) · Zbl 0765.05022
[11] Boy de la Tour, T.: Up-to-Isomorphism Enumeration of Finite Models - The Monadic Case. In: Bonacina, M.P., Furbach, U. (eds.) International Workshop First-Order Theorem Proving (FTP 1997). RISC-Linz Report Series No. 97-50, pp. 29–33. Schloss Hagenberg by Linz, Austria (1997)
[12] Boy de la Tour, T.: Some Techniques of Isomorph-Free Search. In: Campbell, J., Roanes-Lozano, E. (eds.) AISC 2000. LNCS (LNAI), vol. 1930, pp. 240–252. Springer, Heidelberg (2001) · Zbl 1042.68102 · doi:10.1007/3-540-44990-6_20
[13] Bürckert, H.-J., Herold, A., Kapur, D., Siekmann, J.H., Stickel, M., Tepp, M., Zhang, H.: Opening the AC-unification race. J. of Automated Reasoning (4), 465–474 (1988)
[14] Burris, S., Yeats, K.: The saga of the high school identities. Algebra Universalis 52, 325–342 (2004) · Zbl 1083.03038 · doi:10.1007/s00012-004-1900-2
[15] Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic Series, vol. 31. Kluwer Academic Publisher (2004) · Zbl 1085.03009 · doi:10.1007/978-1-4020-2653-9
[16] Caferra, R., Zabel, N.: Extending Resolution for Model Construction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol. 478, pp. 153–169. Springer, Heidelberg (1991) · Zbl 0797.03009 · doi:10.1007/BFb0018439
[17] Claessen, K., Sörensson, N.: New techniques that improve Mace-style finite model finding. In: Model Computation – Principles, Algorithms, Applications, CADE-19 Workshop W4, Miami, Florida, USA (2003)
[18] Dénes, J., Keedwell, A.D.: Latin squares and their applications. Academic Press, New York (1974) · Zbl 0283.05014
[19] Du, B.: Self-orthogonal diagonal Latin square with missing subsquare. JCMCC 37, 193–203 (2001) · Zbl 0987.05030
[20] Een, N., Svrensson, N.: Minisat: A SAT solver with conflict-clause minimization. In: SAT 2005 (2005) (poster paper)
[21] Fujita, M., Slaney, J., Bennett, F.: Automatic generation of some results in finite algebra. In: Proc. Int’l Joint Conf. on Artificial Intelligence (IJCAI 1993), pp. 52–57 (1993)
[22] Galton, A.: Note on a lemma of Ladkin. Journal of Logic and Computation 6(1), 1–4 (1996) · Zbl 0838.03014 · doi:10.1093/logcom/6.1.1
[23] Hasegawa, R., Koshimura, M., Fujita, H.: MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. In: Kapur, D. (ed.) CADE-11. LNCS, vol. 607, pp. 776–780. Springer, Heidelberg (1992) · doi:10.1007/3-540-55602-8_223
[24] Huang, Z., Zhang, H., Zhang, J.: Improving first-order model searching by propositional reasoning and lemma learning. In: The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada (May 2004)
[25] Jia, X., Zhang, J.: A Powerful Technique to Eliminate Isomorphism in Finite Model Search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 318–331. Springer, Heidelberg (2006) · Zbl 1222.68365 · doi:10.1007/11814771_29
[26] Kapur, D., Zhang, H.: An Overview of RRL: Rewrite Rule Laboratory. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 513–529. Springer, Heidelberg (1989) · doi:10.1007/3-540-51081-8_138
[27] Kim, S., Zhang, H.: ModGen: Theorem proving by model generation. In: Proc. of National Conference of American Association on Artificial Intelligence (AAAI 1994), Seattle, WA, pp. 162–167. MIT Press (1994)
[28] Kumar, V.: Algorithms for constraint satisfaction problems: A survey. AI Magazine 13(1), 32–44 (1992)
[29] Kunen, K.: The structure of conjugacy closed loops. Transactions of the American Mathematical Society 352(6), 2889–2911 (2000) · Zbl 0962.20048 · doi:10.1090/S0002-9947-00-02350-3
[30] Leech, J.: Skew lattices in rings. Algebra Universalis 26, 48–72 (1989) · Zbl 0669.06006 · doi:10.1007/BF01243872
[31] Manthey, R., Bry, F.: SATCHMO: A Theorem Prover Implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 415–434. Springer, Heidelberg (1988) · Zbl 0668.68104 · doi:10.1007/BFb0012847
[32] McCune, W.: Experiments with discrimination tree indexing and path indexing for term retrieval. J. of Automated Reasoning 9(2), 147–167 (1992) · Zbl 0781.68101 · doi:10.1007/BF00245458
[33] McCune, W.: MACE 2.0 Reference Manual and Guide. Technical Memorandum No. 249, ANL/MCS-TM-249, Argonne National Lab, Argonne, IL, USA (1994), http://www-unix.mcs.anl.gov/AR/mace2/
[34] McCune, W.: Otter 3.3 Reference Manual, Technical Memorandum No. 263, Argonne National Laboratory, Argonne, IL, USA (August 2003), http://www-unix.mcs.anl.gov/AR/otter/otter33.pdf
[35] McCune, W.: Mace4 reference manual and guide, Technical Memorandum No. 264, Argonne National Laboratory, Argonne, IL, USA (August 2003), http://www.cs.unm.edu/ mccune/prover9/
[36] McCune, W.: Library for Automated Deduction Research (2009), http://www.cs.unm.edu/ mccune/prover9/
[37] McCune, W.: Solution of the Robbins problem. J. of Automated Reasoning 19(3), 263–276 (1997) · Zbl 0883.06011 · doi:10.1023/A:1005843212881
[38] McCune, W., Henschen, L.J.: Experiments with semantic paramodulation. J. of Automated Reasoning 1(3), 231–261 (1985) · Zbl 0615.68064 · doi:10.1007/BF00244271
[39] Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980) · Zbl 0441.68111 · doi:10.1145/322186.322198
[40] Pichler, R.: Algorithms on Atomic Representations of Herbrand Models. In: Dix, J., Fariñas del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol. 1489, pp. 199–215. Springer, Heidelberg (1998) · Zbl 0929.03021 · doi:10.1007/3-540-49545-2_14
[41] Slaney, J.: Finder: Finite Domain Enumerator. In: Bundy, A. (ed.) CADE-12. LNCS, vol. 814, pp. 798–801. Springer, Heidelberg (1994) · doi:10.1007/3-540-58156-1_63
[42] Slaney, J., Fujita, M., Stickel, M.: Automated reasoning and exhaustive search: Quasigroup existence problems. Computers & Math. with Appl. 29(2), 115–132 (1995) · Zbl 0827.20083 · doi:10.1016/0898-1221(94)00219-B
[43] Slaney, J., Lusk, E.L., McCune, W.: SCOTT: Semantically Constrained Otter (System Description). In: Bundy, A. (ed.) CADE-12. LNCS, vol. 814, pp. 764–768. Springer, Heidelberg (1994) · doi:10.1007/3-540-58156-1_56
[44] Spinks, M.: On middle distributivity for Skew lattices. Semigroup Forum 61(3), 341–345 (2000) · Zbl 0964.06004 · doi:10.1007/PL00006032
[45] Stein, S.K.: On the foundations of quasigroups. Trans. Amer. Math. Soc. 85, 228–256 (1957) · Zbl 0079.02402 · doi:10.1090/S0002-9947-1957-0094404-6
[46] Tammet, T.: Using Resolution for Deciding Solvable Classes and Building Finite Models. In: Barzdins, J., Bjorner, D. (eds.) Baltic Computer Science. LNCS, vol. 502, pp. 33–64. Springer, Heidelberg (1991) · doi:10.1007/BFb0019355
[47] Tammet, T.: Finite model building: improvements and comparisons. In: Model Computation – Principles, Algorithms, Applications, CADE-19 Workshop W4, Miami, Florida, USA (2003)
[48] Zhang, H.: Sato: An Efficient Propositional Prover. In: McCune, W. (ed.) CADE-14. LNCS, vol. 1249, pp. 272–275. Springer, Heidelberg (1997) · doi:10.1007/3-540-63104-6_28
[49] Zhang, H.: Specifying Latin squares in propositional logic. In: Veroff, R. (ed.) Automated Reasoning and Its Applications, Essays in Honor of Larry Wos. MIT Press (1997)
[50] Zhang, H.: Combinatorial designs by SAT solvers. In: Biere, A., Heule, M., Van Haaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 17. IOS Press (2009)
[51] Zhang, H., Stickel, M.: Implementing the Davis-Putnam method. J. of Automated Reasoning 24, 277–296 (2000) · Zbl 0967.68148 · doi:10.1023/A:1006351428454
[52] Zhang, J.: Problems on the Generation of Finite Models. In: Bundy, A. (ed.) CADE-12. LNCS, vol. 814, pp. 753–757. Springer, Heidelberg (1994) · doi:10.1007/3-540-58156-1_54
[53] Zhang, J.: Constructing finite algebras with Falcon. J. of Automated Reasoning 17(1), 1–22 (1996) · Zbl 0877.68103 · doi:10.1007/BF00244457
[54] Zhang, J.: On the relational translation method for propositional modal logics. Technical Report ISCAS-LCS-96-12, Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (December 1996)
[55] Zhang, J.: Showing the independence of an axiom for temporal intervals by model generation. Association for Automated Reasoning Newsletter, No. 40 (1998), http://www.aarinc.org/Newsletters/040-1998-06.html
[56] Zhang, J.: System Description: MCS: Model-Based Conjecture Searching. In: Ganzinger, H. (ed.) CADE-16. LNCS (LNAI), vol. 1632, pp. 393–397. Springer, Heidelberg (1999) · doi:10.1007/3-540-48660-7_37
[57] Zhang, J.: Test problem and Perl scripts for finite model searching. Association for Automated Reasoning Newsletter, No. 47 (April 2000), http://www.aarinc.org/Newsletters/047-2000-04.html
[58] Zhang, J.: Computer Search for Counterexamples to Wilkie’s Identity. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 441–451. Springer, Heidelberg (2005) · Zbl 1135.68562 · doi:10.1007/11532231_32
[59] Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Proc. 14th Int’l Joint Conf. on Artif. Intel. (IJCAI), pp. 298–303 (1995)
[60] Zhang, J., Zhang, H.: Constraint Propagation in Model Generation. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol. 976, pp. 398–414. Springer, Heidelberg (1995) · doi:10.1007/3-540-60299-2_24
[61] Zhang, J., Zhang, H.: Extending Finite Model Searching with Congruence Closure Computation. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 94–102. Springer, Heidelberg (2004) · Zbl 1109.68643 · doi:10.1007/978-3-540-30210-0_9
[62] Zhang, X.: Incomplete perfect Mendelsohn designs with block size four. Discrete Mathematics 254, 565–597 (2002) · Zbl 0999.05011 · doi:10.1016/S0012-365X(01)00342-9
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.