×

Blocking and other enhancements for bottom-up model generation methods. (English) Zbl 1468.68279

Summary: Model generation is a problem complementary to theorem proving and is important for fault analysis and debugging of formal specifications of security protocols, programs and terminological definitions, for example. This paper discusses several ways of enhancing the paradigm of bottom-up model generation, with the two main contributions being a new range-restriction transformation and generalized blocking techniques. The range-restriction transformation refines existing transformations to range-restricted clauses by carefully limiting the creation of domain terms. The blocking techniques are based on simple transformations of the input set together with standard equality reasoning and redundancy elimination techniques, and allow for finding small, finite models. All possible combinations of the introduced techniques and a classical range-restriction technique were tested on the clausal problems of the TPTP Version 6.0.0 with an implementation based on the SPASS theorem prover using a hyperresolution-like refinement. Unrestricted domain blocking gave best results for satisfiable problems, showing that it is an indispensable technique for bottom-up model generation methods, that yields good results in combination with both new and classical range-restricting transformations. Limiting the creation of terms during the inference process by using the new range-restricting transformation has paid off, especially when using it together with a shifting transformation. The experimental results also show that classical range restriction with unrestricted blocking provides a useful complementary method. Overall, the results show bottom-up model generation methods are good for disproving theorems and generating models for satisfiable problems, but less efficient for unsatisfiable problems.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
03B70 Logic in computer science

References:

[1] Baader, F.; Calvanese, D.; Mcguinness, Dl; Nardi, D.; Patel-Schneider, Pf, Description Logic Handbook (2003), Cambridge: Cambridge University Press, Cambridge · Zbl 1058.68107
[2] Baader, F.; Sattler, U., An overview of tableau algorithms for description logics, Stud. Log., 69, 5-40 (2001) · Zbl 0991.03012
[3] Bachmair, L.; Dershowitz, N., Critical pair criteria for completion, J. Symb. Comput., 6, 1, 1-18 (1988) · Zbl 0651.68030
[4] Bachmair, L.; Ganzinger, H., Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput., 4, 3, 217-247 (1994) · Zbl 0814.68117
[5] Bachmair, L.; Ganzinger, H.; Bibel, W.; Schmitt, Ph, Equational reasoning in saturation-based theorem proving, Automated Deduction-A Basis for Applications, 353-397 (1998), Alphen aan den Rijn: Kluwer, Alphen aan den Rijn · Zbl 0973.68215
[6] Bachmair, L.; Ganzinger, H.; Robinson, A.; Voronkov, A., Resolution theorem proving, Handbook of Automated Reasoning (2001), Amsterdam: North Holland, Amsterdam · Zbl 0993.03008
[7] Bachmair, L.; Ganzinger, H.; Robinson, A.; Voronkov, A., Resolution theorem proving, Handbook of Automated Reasoning, 19-99 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0993.03008
[8] Baumgartner, P.: Logical engineering with instance-based methods. In: Pfenning, F. (ed.) Automated Deduction: CADE-21, volume 4603 of Lecture Notes in Artificial Intelligence, pp. 404-409. Springer, Berlin (2007)
[9] Baumgartner, P., Fröhlich, P., Furbach, U., Nejdl, W.: Semantically guided theorem proving for diagnosis applications. In: Pollack, M. (ed.), Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence: IJCAI 1997, pp 460-465. Morgan Kaufmann, Burlington (1997) · Zbl 1412.68206
[10] Baumgartner, P.; Fuchs, A.; De Nivelle, H.; Tinelli, C., Computing finite models by reduction to function-free clause logic, J. Appl. Log., 7, 1, 58-74 (2009) · Zbl 1171.68040
[11] Baumgartner, P.; Fuchs, A.; Tinelli, C., Implementing the model evolution calculus, Int. J. Artif. Intell. Tools, 15, 1, 21-52 (2006)
[12] Baumgartner, Peter; Furbach, Ulrich; Niemelä, Ilkka, Hyper tableaux, Logics in Artificial Intelligence, 1-17 (1996), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1427.03031
[13] Baumgartner, P., Furbach, U., Pelzer, B.: Hyper tableaux with equality. In: Pfenning, F. (ed.) Automated Deduction: CADE-21, volume 4603 of Lecture Notes in Artificial Intelligence, pp. 492-507. Springer, Berlin (2007) · Zbl 1213.03019
[14] Baumgartner, P.; Furbach, U.; Pelzer, B., The hyper tableaux calculus with equality and an application to finite model computation, J. Log. Comput., 20, 1, 77-109 (2010) · Zbl 1193.03025
[15] Baumgartner, P.; Furbach, U.; Stolzenburg, F., Computing answers with model elimination, Artif. Intell., 90, 1-2, 135-176 (1997) · Zbl 1017.03505
[16] Baumgartner, Peter; Schmidt, Renate A., Blocking and Other Enhancements for Bottom-Up Model Generation Methods, Automated Reasoning, 125-139 (2006), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1222.68357
[17] Bezem, M.: Disproving distributivity in lattices using geometry logic. In: Proceedings of CADE-20 Workshop on Disproving (2005)
[18] Blanchette, Jasmin Christian; Nipkow, Tobias, Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, Interactive Theorem Proving, 131-146 (2010), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1291.68326
[19] Bolander, T.; Bräuner, T., Tableau-based decision procedures for hybrid logic, J. Log. Comput., 16, 6, 737-763 (2006) · Zbl 1122.03006
[20] Bonacina, Mp; Hsiang, J., On the modelling of search in theorem proving: towards a theory of strategy analysis, Inf. Comput., 147, 171-208 (1998) · Zbl 0927.68081
[21] Bonacina, Mp; Lynch, C.; De Moura, Lm, On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reason., 47, 2, 161-189 (2011) · Zbl 1243.68265
[22] Bonacina, Mp; Plaisted, Da, Semantically-guided goal-sensitive reasoning: Inference system and completeness, J. Autom. Reason., 59, 2, 165-218 (2017) · Zbl 1437.68189
[23] Bry, François; Torge, Sunna, A Deduction Method Complete for Refutation and Finite Satisfiability, Logics in Artificial Intelligence, 122-138 (1998), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0928.03031
[24] Bry, F.; Yahya, A., Positive unit hyperresolution tableaux for minimal model generation, J. Autom. Reason., 25, 1, 35-82 (2000) · Zbl 0960.03006
[25] Buchheit, M.; Donini, Fm; Schaerf, A., Decidable reasoning in terminological knowledge representation systems, J. Artif. Intell. Res., 1, 109-138 (1993) · Zbl 0900.68396
[26] Caferra, R.; Leitsch, A.; Peltier, N., Automated Model Building, Volume 31 of Applied Logic (2004), Berlin: Springer, Berlin · Zbl 1085.03009
[27] Caferra, R.; Peltier, N., Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, J. Symb. Comput., 29, 2, 177-211 (2000) · Zbl 0965.03012
[28] Cialdea Mayer, M., Cerrito, S.: Nominal substitution at work with the global and converse modalities. In: Beklemishev, L., Goranko, V., Shehtman, V. (eds.) Advances in Modal Logic, vol. 8, pp. 57-74. College Publications (2010) · Zbl 1254.03030
[29] Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model building. In: Baumgartner, P., Fermüller, C.G. (eds.), Proceedings of CADE-19 Workshop on Model Computation (2003)
[30] de Moura, L.M., Bjørner, N.: Bugs, moles and skeletons: symbolic reasoning for software development. In: Automated Reasoning: IJCAR 2010, volume 6173 of Lecture Notes in Computer Science, pp. 400-411. Springer, Berlin (2010) · Zbl 1291.68377
[31] De Nivelle, H.; Schmidt, Ra; Hustadt, U., Resolution-based methods for modal logics, Log. J. IGPL, 8, 3, 265-292 (2000) · Zbl 0947.03014
[32] Dershowitz, Nachum, A maximal-literal unit strategy for horn clauses, Conditional and Typed Rewriting Systems, 14-25 (1991), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1507.68337
[33] Fermüller, Cg; Leitsch, A., Hyperresolution and automated model building, J. Log. Comput., 6, 2, 173-203 (1996) · Zbl 0861.68086
[34] Fermüller, Cg; Leitsch, A.; Tammet, T.; Zamov, N., Resolution Method for the Decision Problem, volume 679 of Lecture Notes in Computer Science (1993), Berlin: Springer, Berlin · Zbl 0789.03013
[35] Fitting, M., Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese Library (1983), Kufstein: Reidel, Kufstein · Zbl 0523.03013
[36] Fitting, M., First-Order Logic and Automated Reasoning. Graduate Texts in Computer Science (1996), Berlin: Springer, Berlin · Zbl 0848.68101
[37] Fujita, M., Slaney, J., Bennett, F.: Automatic generation of some results in finite algebra. In: Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence: IJCAI 1995, pp. 52-57. Morgan Kaufmann, Burlington (1995)
[38] Gabbay, D.M., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. S. Afr. Comput. J. 7, 35-43, 1992. Also published in Nebel, B., Rich, C., Swartout, W. R. (eds.), Proceedings of the Third International Conference on Principles of Knowledge Representation and Reasoning: KR 1992, pp. 425-436. Morgan Kaufmann, Burlington (1992)
[39] Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of the 18th IEEE Symposium on Logic in Computer Science: LICS 2003, pp. 55-64. IEEE Computer Society Press, Washington (2003)
[40] Ganzinger, Harald; Korovin, Konstantin, Integrating Equational Reasoning into Instantiation-Based Theorem Proving, Computer Science Logic, 71-84 (2004), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1095.68111
[41] Geisler, T.; Panne, S.; Schütz, H., Satchmo: the compiling and functional variants, J. Autom. Reason., 18, 2, 227-236 (1997)
[42] Georgieva, L.; Hustadt, U.; Schmidt, Ra, Hyperresolution for guarded formulae, J. Symb. Comput., 36, 1-2, 163-192 (2003) · Zbl 1020.03007
[43] Hasegawa, Ryuzo; Inoue, Katsumi; Ohta, Yoshihiko; Koshimura, Miyuki, Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving, Automated Deduction—CADE-14, 176-190 (1997), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1430.68410
[44] Hintikka, J., Model minimization: an alternative to circumscription, J. Autom. Reason., 4, 1, 1-13 (1988)
[45] Horrocks, I.; Sattler, U., A description logic with transitive and inverse roles and role hierarchies, J. Log. Comput., 9, 3, 385-410 (1999) · Zbl 0940.03039
[46] Horrocks, I.; Sattler, U., A tableau decision procedure for SHOIQ, J. Autom. Reason., 39, 3, 249-276 (2007) · Zbl 1132.68734
[47] Horrocks, I.; Sattler, U.; Tobies, S., Practical reasoning for very expressive description logics, Log. J. IGPL, 8, 3, 239-263 (2000) · Zbl 0967.03026
[48] Hsiang, J.; Rusinowitch, M., Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method, J. ACM, 38, 3, 559-587 (1991) · Zbl 0799.68170
[49] Hughes, Ge; Cresswell, Mj, An Introduction to Modal Logic (1968), Abingdon: Routledge, Abingdon · Zbl 0205.00503
[50] Hustadt, U., Schmidt, R.A.: On the relation of resolution and tableaux proof systems for description logics. In: Dean, T. (ed.) Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence: IJCAI 1999, pp. 110-115. Morgan Kaufmann, Burlington (1999)
[51] Hustadt, Ullrich; Schmidt, Renate A., Issues of Decidability for Description Logics in the Framework of Resolution, Automated Deduction in Classical and Non-Classical Logics, 191-205 (2000), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0955.03018
[52] Hustadt, Ullrich; Schmidt, Renate A., MSPASS: Modal Reasoning by Translation and First-Order Resolution, Lecture Notes in Computer Science, 67-71 (2000), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0963.68522
[53] Hustadt, U.; Schmidt, Ra, Using resolution for testing modal satisfiability and building models, J. Autom. Reason., 28, 2, 205-232 (2002) · Zbl 1005.03010
[54] Hustadt, U., Schmidt, R. A., Weidenbach, C.: MSPASS: Subsumption testing with SPASS. In: Lambrix, P., Borgida, A., Lenzerini, M., Möller, R., Patel-Schneider, P. (eds.) Proceedings of International Workshop on Description Logics: DL 1999, pp. 136-137. Linköping University, Linköping (1999)
[55] Kaminski, M.; Smolka, G., Terminating tableau systems for hybrid logic with difference and converse, J. Log. Lang. Inf., 18, 4, 437-464 (2009) · Zbl 1188.03013
[56] Khodadadi, M., Schmidt, R.A., Tishkovsky, D.: A refined tableau calculus with controlled blocking for the description logic \(\cal{S}\cal{H}\cal{O}\cal{I} \). In: Galmiche, D., Larchey-Wendling, D. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2013, Volume 8123 of Lecture Notes in Computer Science, pp. 188-202. Springer, Berlin (2013) · Zbl 1401.68307
[57] Korovin, Konstantin, Instantiation-Based Automated Reasoning: From Theory to Practice, Automated Deduction - CADE-22, 163-166 (2009), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[58] Kripke, S., Semantical considerations of modal logic I: normal modal propositional calculi, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 9, 67-96 (1963) · Zbl 0118.01305
[59] Leino, K.R.M., Milicevic, A.: Program extrapolation with Jennisys. In: Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications: OOPSLA 2012, pp. 411-430. ACM, New York (2012)
[60] Leitsch, A., The Resolution Calculus. EATCS Texts in Theoretical Computer Science (1997), Berlin: Springer, Berlin · Zbl 0867.68095
[61] Lorenz, S., A tableaux prover for domain minimization, J. Autom. Reason., 13, 3, 375-390 (1994) · Zbl 0815.03004
[62] Lynch, Christopher, Unsound Theorem Proving, Computer Science Logic, 473-487 (2004), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1095.68112
[63] Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) Automated Deduction: CADE-9, Volume 310 of Lecture Notes in Computer Science, pp. 415-434. Springer, Berlin (1988) · Zbl 0668.68104
[64] Massacci, F., Single step tableaux for modal logics: computational properties, complexity and methodology, J. Autom. Reason., 24, 3, 319-364 (2000) · Zbl 0951.03008
[65] McCune, W.: A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical Report MCS-TM-194, ANL (1994)
[66] McCune, W.: Mace4 reference manual and guide. Technical Memorandum 264, Argonne National Laboratory (2003)
[67] Minica, S., Khodadadi, M., Tishkovsky, D., Schmidt, R.A.: Synthesising and implementing tableau calculi for interrogative epistemic logics. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, Volume 21 of EPiC Series, pp. 109-123. EasyChair, Manchester (2013)
[68] Nieuwenhuis, R.; Rubio, A.; Robinson, A.; Voronkov, A., Paramodulation-based theorem proving, Handbook of Automated Reasoning, 371-443 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0997.03012
[69] Papacchini, F.; Schmidt, Ra, A tableau calculus for minimal modal model generation, Electron. Notes Theor. Comput. Sci., 278, 3, 159-172 (2011) · Zbl 1347.03048
[70] Papacchini, F., Schmidt, R.A.: Computing minimal models modulo subset-simulation for propositional modal logics. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) Proceedings of the 9th International Symposium on Frontiers of Combining Systems: FroCoS 2013, Volume 8152 of Lecture Notes in Artificial Intelligence, pp. 279-294. Springer, Berlin (2013) · Zbl 1398.03095
[71] Peltier, N., A calculus combining resolution and enumeration for building finite models, J. Symb. Comput., 36, 1-2, 49-77 (2003) · Zbl 1019.03009
[72] Pelzer, B., Wernhard, C.: System description: E-KRHyper. In: Pfenning, F. (ed.) Automated Deduction: CADE-21, Volume 4603 of Lecture Notes in Artificial Intelligence, pp. 508-513. Springer, Berlin (2007) · Zbl 1213.68574
[73] Riazanov, A.: Implementing an Efficient Theorem Prover. PhD thesis, Department of Computer Science, The University of Manchester, UK (2003)
[74] Riazanov, A.; Voronkov, A., The design and implementation of VAMPIRE, AI Commun., 15, 2-3, 91-110 (2002) · Zbl 1021.68082
[75] Robinson, Ja, Automatic deduction with hyper-resolution, Int. J. Comput. Math., 1, 3, 227-234 (1965) · Zbl 0158.26003
[76] Schmidt, Ra, A new methodology for developing deduction methods, Ann. Math. Artif. Intell., 55, 1-2, 155-187 (2009) · Zbl 1192.68632
[77] Schmidt, R.A., Hustadt, U.: Solvability with resolution of problems in the Bernays-Schönfinkel class. Presented at Dagstuhl Seminar 05431, 2006, and ARW 2006 in Bristol (2005)
[78] Schmidt, R.A., Stell, J.G., Rydeheard, D.: Axiomatic and tableau-based reasoning for Kt(H, R). In: Goré, R., Kurucz, A. (eds.) Advances in Modal Logic, vol. 10, pp. 478-497. College Publications (2014) · Zbl 1385.03026
[79] Schmidt, R. A., Tishkovsky, D.: Using tableau to decide expressive description logics with role negation. In: Aberer, K., Choi, K.-S., Fridman Noy, N., Allemang, D., Lee, K.-I., Nixon, L.J.B., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P. (eds.) The Semantic Web: ISWC 2007 + ASWC 2007, Volume 4825 of Lecture Notes in Computer Science, pp. 438-451. Springer, Berlin (2007)
[80] Schmidt, R.A., Tishkovsky, D.: A general tableau method for deciding description logics, modal logics and related first-order fragments. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning: IJCAR 2008, Volume 5195 of Lecture Notes in Computer Science, pp 194-209. Springer, Berlin (2008) · Zbl 1165.03319
[81] Schmidt, Ra; Tishkovsky, D., Automated synthesis of tableau calculi, Log. Methods Comput. Sci., 7, 2, 1-32 (2011) · Zbl 1218.03012
[82] Schmidt, Ra; Tishkovsky, D., Using tableau to decide description logics with full role negation and identity, ACM Trans. Comput. Log., 15, 1, 7 (2014) · Zbl 1287.03031
[83] Schulz, Stephan, System Description: E 1.8, Logic for Programming, Artificial Intelligence, and Reasoning, 735-743 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1407.68442
[84] Schulz, S., Bonacina, M.P.: On handling distinct objects in the superposition calculus. In: Konev, B., Schulz, S. (eds.) Proceedings of the 5th International Workshop on the Implementation of Logics: IWIL (2005). http://www4.in.tum.de/ schulz/PAPERS/SB-IWIL-2005.ps.gz
[85] Slaney, J.: FINDER (finite domain enumerator): Notes and guide. Technical Report TR-ARP-1/92, Australian National University (1992)
[86] Smullyan, Rm, First Order Logic (1971), Berlin: Springer, Berlin
[87] Stell, Jg; Schmidt, Ra; Rydeheard, D., A bi-intuitionistic modal logic: Foundations and automation, J. Log. Algebraic Methods Programm., 85, 4, 500-519 (2016) · Zbl 1359.03018
[88] Stickel, Me, Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction, J. Autom. Reason., 13, 2, 189-210 (1994) · Zbl 0819.68113
[89] Sutcliffe, G., The TPTP problem library and associated infrastructure, J. Autom. Reason., 43, 4, 337-362 (2009) · Zbl 1185.68636
[90] Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: MetTeL2: Towards a tableau prover generation platform. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) PAAR-2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, Volume 21 of EPiC Series, pp. 149-162. EasyChair (2012)
[91] Tishkovsky, Dmitry; Schmidt, Renate A.; Khodadadi, Mohammad, The Tableau Prover Generator MetTeL2, Logics in Artificial Intelligence, 492-495 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[92] Weidenbach, C.; Robinson, A.; Voronkov, A., Combining superposition, sorts and splitting, Handbook of Automated Reasoning, 1965-2013 (2001), Amsterdam: North Holland, Amsterdam · Zbl 1011.68129
[93] Weidenbach, Christoph; Dimova, Dilyana; Fietzke, Arnaud; Kumar, Rohit; Suda, Martin; Wischnewski, Patrick, SPASS Version 3.5, Automated Deduction - CADE-22, 140-145 (2009), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[94] Weidenbach, C., Schmidt, R. A., Hillenbrand, T., Rusev, R., Topic, D.: System description: SPASS version 3.0. In: Pfenning, F. (ed.) Automated Deduction: CADE-21, Volume 4603 of Lecture Notes in Artificial Intelligence, pp. 514-520. Springer, Berlin (2007) · Zbl 1213.68577
[95] Wernhard, C.: System description: KRHyper. In: Proceedings of CADE-19 Workshop on Model Computation (2003) · Zbl 1213.68574
[96] Winker, S., Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions, J. ACM, 29, 2, 273-284 (1982) · Zbl 0488.68056
[97] Zawidzki, M.: Deductive systems and decidability problem for hybrid logics. PhD thesis, Faculty of Philosophy and History, University of Lodz (2013) · Zbl 1426.03006
[98] Zhang, H.: SEM: A system for enumerating models. In: Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence: IJCAI 1995, pp. 298-303. Morgan Kaufmann, Burlington (1995)
[99] Zhang, Hantao; Zhang, Jian, MACE4 and SEM: A Comparison of Finite Model Generators, Automated Reasoning and Mathematics, 101-130 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1383.68083
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.