×

zbMATH — the first resource for mathematics

First-order automated reasoning with theories: when deduction modulo theory meets practice. (English) Zbl 07268893
Summary: We discuss the practical results obtained by the first generation of automated theorem provers based on Deduction modulo theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with the introduction of a rewrite feature. Deduction modulo theory is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We introduce two automated reasoning systems that have been built to extend other provers with Deduction modulo theory. The first one is Zenon Modulo, a tableau-based tool able to deal with polymorphic first-order logic with equality, while the second one is iProverModulo, a resolution-based system dealing with first-order logic with equality. We also provide some experimental results run on benchmarks that show the beneficial impact of the extension on these two tools and their underlying proof search methods. Finally, we describe the two backends of these systems to the Dedukti universal proof checker, which also relies on Deduction modulo theory, and which allows us to verify the proofs produced by these tools.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial, JR, The B-Book, Assigning Programs to Meanings (1996), Cambridge: Cambridge University Press, Cambridge · Zbl 0915.68015
[2] Andreoli, JM, Logic programming with focusing proofs in linear logic, J. Log. Comput., 2, 3, 297-347 (1992) · Zbl 0764.03020
[3] Assaf, A.: A framework for defining computational higher-order logics. Ph.D. Thesis, École polytechnique (2015)
[4] Assaf, A.: Conservativity of embeddings in the \(\lambda \varPi\) calculus modulo rewriting. In: Typed lambda calculi and applications (TLCA), LIPIcs, vol. 38, pp. 31-44. SchlossDagstuhl, Leibniz-Zentrum fuer Informatik, Warsaw (2015) · Zbl 1367.68047
[5] Assaf, A., Burel, G.: Translating HOL to Dedukti. In: Proof eXchange for theorem proving (PxTP), EPTCS, vol. 186, pp. 74-88. Open Publishing Association, Berlin (2015)
[6] Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., Saillard, R.: Dedukti: a logical framework based on the \(\lambda \varPi \)-calculus modulo theory (2016). http://www.lsv.ens-cachan.fr/ dowek/Publi/expressing.pdf. Accessed 2 Sept 2019
[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] Bachmair, L.; Ganzinger, H.; Waldmann, U., Refutational theorem proving for hierarchic first-order theories, Appl. Algebra Eng. Commun. Comput., 5, 193-212 (1994) · Zbl 0797.03008
[9] Barendregt, H.; Barendsen, E., Autarkic computations in formal proofs, J. Autom. Reason., 28, 3, 321-336 (2002) · Zbl 1002.68156
[10] Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press, Cambridge (2013). ISBN 9780521766142 · Zbl 1347.03001
[11] Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects (FMCO), LNCS, vol. 4111, pp. 364-387. Springer, Amsterdam (2005)
[12] Barrett, CW; Sebastiani, R.; Seshia, SA; Tinelli, C.; Biere, A.; Heule, M.; Van Maaren, H.; Walsh, T., Satisfiability modulo theories, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 825-885 (2009), Amsterdam: IOS Press, Amsterdam
[13] Barrett, CW; Tinelli, C.; Clarke, EM; Henzinger, ThA; Veith, H.; Bloem, R., Satisfiability modulo theories, Handbook of Model Checking, 305-343 (2018), Berlin: Springer, Berlin
[14] Baumgartner, P.: A Model elimination calculus with built-in theories. In: German Conference on Artificial Intelligence (GWAI), LNCS, vol. 671, pp. 30-42. Springer, Bonn (1992) · Zbl 0925.03050
[15] Baumgartner, P.: An order theory resolution calculus. In: Logic Programming and Automated Reasoning (LPAR), LNCS, vol. 624, pp. 119-130. Springer, St. Petersburg (1992) · Zbl 0920.03016
[16] Baumgartner, P., Bax, J., Waldmann, U.: Beagle—a hierarchic superposition theorem prover. In: Conference on Automated Deduction (CADE), LNCS, vol. 9195, pp. 367-377. Springer, Berlin (2015) · Zbl 06515519
[17] Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Conference on Automated Deduction (CADE), LNCS, vol. 7898, pp. 39-57. Springer, Lake Placid (2013) · Zbl 1381.03017
[18] Beckert, B., Semantic tableaux with equality, J. Log. Comput., 7, 1, 39-58 (1997) · Zbl 0876.03008
[19] Beckert, B., Pape, C.: Incremental theory reasoning methods for semantic tableaux. In: Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX), LNCS, vol. 1071, pp. 93-109. Springer, Terrasini (1996) · Zbl 1412.68208
[20] Beth, EW, The Foundations of Mathematics: A Study in the Philosophy of Science (1959), Amsterdam: North-Holland, Amsterdam
[21] Beth, EW, Formal Methods: An Introduction to Symbolic Logic and to the Study of Effective Operations in Arithmetic and Logic, Synthese Library (1962), Dordrecht: D. Reidel, Dordrecht
[22] Blanchette, JC; Böhme, S.; Popescu, A.; Smallbone, N., Encoding monomorphic and polymorphic types, Log. Methods Comput. Sci., 12, 4, 1-52 (2016) · Zbl 1445.68327
[23] Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Conference on Automated Deduction (CADE), LNCS, vol. 7898. Springer (2013) · Zbl 1381.68260
[24] Blanqui, F., Jouannaud, J.P., Okada, M.: The calculus of algebraic constructions. In: Rewriting Techniques and Applications (RTA), LNCS, vol. 1631. Springer, Trento (1999) · Zbl 0943.68153
[25] Bläsius, K.H., Hedtstück, U., Rollinger, C.R. (eds.): Sorts and Types in Artificial Intelligence, Workshop, Eringerfeld, FRG, April 24-26, 1989, Proceedings, LNCS, vol. 418. Springer (1989) · Zbl 0743.68016
[26] Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: International Workshop on Intermediate Verification Languages (Boogie), Wrocław, Poland, pp. 53-64 (2011)
[27] Boespflug, M., Burel, G.: CoqinE: translating the calculus of inductive constructions into the \(\lambda \varPi \)-calculus modulo. Proof eXchange for Theorem Proving (PxTP), CEUR Workshop Proceedings, vol. 878, pp. 44-50. David Pichardie and Tjark Weber, Manchester (2012)
[28] Boespflug, M., Carbonneaux, Q., Hermant, O.: The \(\lambda \varPi \)-calculus modulo as a universal proof language. In: Proof Exchange for Theorem Proving (PxTP), pp. 28-43. Manchester (2012)
[29] Bonichon, R.: TaMeD: a tableau method for deduction modulo. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 3097, pp. 445-459. Springer, Cork (2004) · Zbl 1126.68560
[30] Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Logic for Programming. Artificial Intelligence, and Reasoning (LPAR), LNCS/LNAI, vol. 4790, pp. 151-165. Springer, Yerevan (2007) · Zbl 1137.68572
[31] Bonichon, R., Hermant, O.: A semantic completeness proof for TaMeD. In: Logic for Programming. Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 4246, pp. 167-181. Springer, Phnom Penh (2006) · Zbl 1165.68451
[32] Bonichon, R., Hermant, O.: On constructive cut admissibility in deduction modulo. In: Types for Proofs and Programs (TYPES), LNCS, vol. 4502, pp. 33-47. Springer, Nottingham (2006) · Zbl 1178.03021
[33] Boyer, R.S., Moore, J.S.: A theorem prover for a computational logic. In: Conference on Automated Deduction (CADE), vol. 449, pp. 1-15. Springer, Kaiserslautern (1990) · Zbl 0708.68060
[34] Brauner, P., Houtmann, C., Kirchner, C.: Principles of superdeduction. In: Logic in Computer Science (LICS), pp. 41-50. IEEE Computer Society Press, Wrocław (2007) · Zbl 1186.03021
[35] Burel, G.: Embedding deduction modulo into a prover. In: Computer Science Logic (CSL), LNCS, vol. 6247, pp. 155-169. Springer, Brno (2010) · Zbl 1287.68152
[36] Burel, G.: Consistency implies cut admissibility. In: Proof-Search in Axiomatic Theories and Type Theories (PSATTT), Wrocław, Poland (2011)
[37] Burel, G., Efficiently simulating higher-order arithmetic by a first-order theory modulo, Log. Methods Comput. Sci., 7, 1, 1-31 (2011) · Zbl 1218.03007
[38] Burel, G.: A shallow embedding of resolution and superposition proofs into the \(\lambda \varPi \)-calculus modulo. In: Proof eXchange for Theorem Proving (PxTP), EPiC Series, vol. 14, pp. 43-57. EasyChair (2013)
[39] Burel, G.: Cut admissibility by saturation. In: Rewriting Techniques and Applications (RTA) and Typed Lambda Calculi and Applications (TLCA), LNCS, vol. 8560, pp. 124-138. Springer, Vienna (2014) · Zbl 1416.68154
[40] Burel, G.; Kirchner, C., Regaining cut admissibility in deduction modulo using abstract completion, Inf. Comput., 208, 2, 140-164 (2010) · Zbl 1191.68359
[41] Bury, G., Cauderlier, R., Halmagrand, P.: Implementing polymorphism in Zenon. in: International Workshop on the Implementation of Logics (IWIL), EPiC Series in Computing, vol. 40, pp. 15-20. EasyChair, Suva (2015)
[42] Bury, G., Cruanes, S., Delahaye, D.: SMT solving modulo tableau and rewriting theories. In: Satisfiability Modulo Theories (SMT). Oxford (2018)
[43] Bury, G., Cruanes, S., Delahaye, D., Euvrard, P.L.: An automation-friendly set theory for the B method. Abstract State Machines, Alloy, B, VDM, and Z (ABZ), LNCS, vol. 10817, pp. 409-414. Springer, Southampton (2018)
[44] Bury, G., Delahaye, D.: Integrating simplex with tableaux. In: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), LNCS, vol. 9323, pp. 86-101. Springer, Wrocław (2015) · Zbl 06519936
[45] Bury, G., Delahaye, D., Doligez, D., Halmagrand, P., Hermant, O.: Automated deduction in the B set theory using typed proof search and deduction modulo. Logic for programming. In: Artificial Intelligence and Reasoning (LPAR), Short Papers, EPiC Series in Computing, vol. 35, pp. 42-58. EasyChair, Suva (2015)
[46] Cauderlier, R.: Object-oriented mechanisms for interoperability between proof systems. Ph.D. Thesis, Conservatoire National des Arts et Métiers (CNAM) (2016)
[47] Cauderlier, R., Dubois, C.: ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Boogie. In: International Colloquium on Theoretical Aspects of Computing (ICTAC), LNCS, vol. 9965, pp. 459-468. Springer, Taipei (2016) · Zbl 06667722
[48] Cauderlier, R., Halmagrand, P.: Checking Zenon Modulo proofs in Boogie. In: Proof eXchange for Theorem Proving (PxTP). EPTCS, vol. 186, pp. 57-73. Open Publishing Association, Berlin (2015)
[49] Chvátal, V., Linear Programming. Series of Books in the Mathematical Sciences (1983), New York: W. H. Freeman and Company, New York
[50] ClearSy: Atelier B 4.2.1 (2015). http://www.atelierb.eu/
[51] Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Typed Lambda Calculi and Applications (TLCA), LNCS, vol. 4583, pp. 102-117. Springer, Paris (2007) · Zbl 1215.03021
[52] Davis, M.; Logemann, G.; Loveland, DW, A machine program for theorem-proving, Commun. ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002
[53] Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 7, 3, 201-215 (1960) · Zbl 0212.34203
[54] De Moura, L.M., Bjørner, N.: Efficient E-matching for SMT solvers. In: Conference on Automated Deduction (CADE), LNCS, vol. 4603, pp. 183-198. Springer, Bremen (2007) · Zbl 1213.68578
[55] Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: when achilles outruns the tortoise using deduction modulo. In: Logic for Programming. Artificial Intelligence, and Reasoning (LPAR), LNCS/ARCoSS, vol. 8312, pp. 274-290. Springer, Stellenbosch (2013) · Zbl 1406.68105
[56] Delahaye, D., Dubois, C., Marché, C., Mentré, D.: The BWare Project: building a proof platform for the automated verification of B proof obligations. In: Abstract State Machines, Alloy, B, VDM, and Z (ABZ), LNCS, vol. 8477, pp. 126-127. Springer, Toulouse (2014)
[57] Detlefs, D.; Nelson, G.; Saxe, JB, Simplify: a theorem prover for program checking, J. ACM, 52, 3, 365-473 (2005) · Zbl 1323.68462
[58] Dowek, G.: Confluence as a cut elimination property. In: Rewriting Techniques and Applications (RTA), LNCS, vol. 2706, pp. 2-13. Springer (2003) · Zbl 1038.03054
[59] Dowek, G.: Polarized resolution modulo. Theoretical computer science (TCS). In: IFIP Advances in Information and Communication Technology, vol. 323, pp. 182-196. Springer, Brisbane (2010) · Zbl 1202.68215
[60] Dowek, G.; Hardin, T.; Kirchner, C., Theorem proving modulo, J. Autom. Reason., 31, 1, 33-72 (2003) · Zbl 1049.03011
[61] Dowek, G.; Werner, B., Proof normalization modulo, J. Symb. Logic, 68, 4, 1289-1316 (2003) · Zbl 1059.03062
[62] Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Rewriting Techniques and Applications (RTA), LNCS, vol. 3467, pp. 423-437. Springer, Nara (2005) · Zbl 1078.03046
[63] Fitting, M., First-Order Logic and Automated Theorem Proving (1996), Berlin: Springer, Berlin · Zbl 0848.68101
[64] Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI), pp. 234-245. ACM, Berlin (2002)
[65] Gaanzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Logic in Computer Science (LICS), pp. 55-64. IEEE Computer Society, Ottawa (2003)
[66] Ganzinger, H., Korovin, K.: Theory instantiation. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 4246, pp. 497-511. Springer, Phnom Penh (2006) · Zbl 1165.03315
[67] Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Conference on Automated Deduction (CADE), LNCS, vol. 4603, pp. 167-182. Springer, Bremen (2007) · Zbl 1213.68376
[68] Giese, M.: Incremental closure of free variable tableaux. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 2083, pp. 545-560. Springer, Siena (2001) · Zbl 0988.03019
[69] Halmagrand, P.: Soundly proving B method formulae using typed sequent calculus. In: International Colloquium on Theoretical Aspects of Computing (ICTAC), LNCS, vol. 9965, pp. 196-213. Springer, Taipei (2016) · Zbl 06667708
[70] Harper, R.; Honsell, F.; Plotkin, GD, A framework for defining logics, J. ACM, 40, 1, 143-184 (1993) · Zbl 0778.03004
[71] Hermant, O.: Semantic cut elimination in the intuitionistic sequent calculus. In: Typed Lambda-Calculi and Applications (TLCA), LNCS, vol. 3461, pp. 221-233. Springer, Nara (2005) · Zbl 1114.03044
[72] Hermant, O., Resolution is cut-free, J. Autom. Reason., 44, 3, 245-276 (2010) · Zbl 1197.03010
[73] Hintikka, J., Notes on the quantification theory, Societas Scientiarum Fennica, Commentationes Physico-Mathematicae, 17, 12, 1-13 (1955) · Zbl 0067.25002
[74] Hintikka, J., Two papers on symbolic logic: form and content in quantification theory and reductions in the theory of types, Societas Philosophica, Acta philosophica Fennica, 8, 7-55 (1955)
[75] Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Tableaux modulo theories using superdeduction: an application to the verification of B proof rules with the Zenon automated theorem prover. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 7364, pp. 332-338. Springer, Manchester (2012) · Zbl 1358.68255
[76] Jacquel, M.; Berkani, K.; Delahaye, D.; Dubois, C., Tableaux modulo theories using superdeduction, Glob. J. Adv. Softw. Eng., 1, 1-13 (2014)
[77] Kifer, M., Wu, J.: A first-order theory of types and polymorphism in logic programming. In: Logic in Computer Science (LICS), pp. 310-321. IEEE Computer Society, Amsterdam (1991)
[78] Korovin, K.: iProver—an instantiation-based theorem prover for first-order logic (system description). In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 5195, pp. 292-298. Springer, Sydney (2008) · Zbl 1165.68462
[79] Lipton, J.; DeMarco, M., Completeness and cut-elimination in the intuitionistic theory of types, J. Log. Comput., 15, 821-854 (2005) · Zbl 1095.03056
[80] Maehara, S., Lattice-valued representation of the cut-elimination theorem, Tsukuba J. Math., 15, 2, 509-521 (1991) · Zbl 0758.03026
[81] Marques Silva, JP; Lynce, I.; Malik, S.; Biere, A.; Heule, M.; Van Maaren, H.; Walsh, T., Conflict-driven clause learning SAT solvers, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 131-153 (2009), Amsterdam: IOS Press, Amsterdam
[82] Mentré, D., Marché, C., Filliâtre, J.C., Asuka, M.: Discharging proof obligations from Atelier B using multiple automated provers. In: Abstract State Machines, Alloy, B, VDM, and Z (ABZ), LNCS, vol. 7316, pp. 238-251. Springer, Pisa (2012)
[83] Murray, NV; Rosenthal, E., Theory links: applications to automated theorem proving, J. Symb. Comput., 4, 2, 173-190 (1987)
[84] Nelson, G.; Oppen, DC, Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst., 1, 2, 245-257 (1979) · Zbl 0452.68013
[85] Nelson, G.; Oppen, DC, Fast decision procedures based on congruence closure, J. ACM, 27, 2, 356-364 (1980) · Zbl 0441.68111
[86] Nerode, A.; Shore, RA, Logic for Applications. Texts and Monographs in Computer Science (1993), Berlin: Springer, Berlin
[87] Ohlbach, HJ; Siekmann, JH; Lassez, J-L; Plotikin, G., The Markgraf Karl refutation procedure, Computational Logic, Essays in Honor of Alan Robinson, 41-112 (1991), Cambridge: The MIT Press, Cambridge
[88] Okada, M., Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic, Theor. Comput. Sci., 227, 333-396 (1999) · Zbl 0951.03058
[89] Oppacher, F.; Suen, E., HARP: a tableau-based theorem prover, J. Autom. Reason., 4, 1, 69-100 (1988)
[90] Petermann, U.: Towards a connection procedure with built in theories. In: Logics in AI, European Workshop JELIA, LNCS, vol. 478, pp. 444-543. Springer, Amsterdam (1990) · Zbl 0796.03011
[91] Plotkin, GD, Building-in equational theories, Mach. Intell., 7, 73-90 (1972) · Zbl 0262.68036
[92] Prawitz, D., Natural Deduction. A Proof-Theoretical Study. Studies in Philosophy (1965), Stockholm: Almquist & Wiksell, Stockholm · Zbl 0173.00205
[93] Rabe, F.: First-order logic with dependent types. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 4130, pp. 377-391. Springer, Seattle (2006) · Zbl 1222.03016
[94] Robinson, JA, A machine-oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41 (1965) · Zbl 0139.12303
[95] Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 5330, pp. 274-289. Springer, Doha (2008) · Zbl 1182.03035
[96] Saillard, R.: Typechecking in the \(\lambda \varPi \)-calculus modulo: theory and practice. Ph.D. Thesis, École Nationale Supérieure des Mines de Paris (2015)
[97] Schmitt, P.H., Wernecke, W.: Tableau calculus for order sorted logic. In: Sorts and Types in Artificial Intelligence, pp. 49-60. Springer, Berlin (1989) · Zbl 0747.68083
[98] Schultz, S.: System description: E 0.81. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 3097, pp. 223-228. Springer, Cork (2004) · Zbl 1126.68578
[99] Schwichtenberg, H.; Troelstra, AS, Basic Proof Theory (2000), Cambridge: Cambridge University Press, Cambridge
[100] Shankar, N.: Little engines of proof. In: Formal Methods Europe (FME), LNCS, vol. 2391, pp. 1-20. Springer, Copenhagen (2002) · Zbl 1064.68558
[101] Shostak, RE, Deciding combinations of theories, J. ACM, 31, 1, 1-12 (1984) · Zbl 0629.68089
[102] Stickel, ME, Automated deduction by theory resolution, J. Autom. Reason., 1, 4, 333-355 (1985) · Zbl 0616.68076
[103] Strub, P.-Y.: Coq modulo theory. In: Computer Science Logic (CSL), LNCS, vol. 6247, pp. 529-543. Springer, Brno (2010) · Zbl 1287.68154
[104] Sutcliffe, G., The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0, J. Autom. Reason., 43, 4, 337-362 (2009) · Zbl 1185.68636
[105] Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 7180, pp. 406-419. Springer, Mérida (2012) · Zbl 1352.68217
[106] Szabo, ME, Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundation of Mathematics (1969), Amsterdam: North-Holland, Amsterdam
[107] The BWare Project (2012). http://bware.lri.fr/
[108] Tinelli, C., Cooperation of background reasoners in theory reasoning by residue sharing, J. Autom. Reason., 30, 1, 1-31 (2003) · Zbl 1019.03004
[109] Walther, C.: Many-sorted inferences in automated theorem proving. In: Sorts and Types in Artificial Intelligence, LNCS, vol. 418, pp. 18-48. Springer, Eringerfeld (1989) · Zbl 0747.68084
[110] Weidenbach, C., First-order tableaux with sorts, Log. J. IGPL, 3, 6, 887-906 (1995) · Zbl 0879.03007
[111] Weidenbach, C.; Robinson, A.; Voronkov, A., Combining superposition, sorts and splitting, Handbook of Automated Reasoning, 1965-2013 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 1011.68129
[112] Wos, L.; Robinson, GA; Carson, DF, Efficiency and completeness of the set of support strategy in theorem proving, J. ACM, 12, 4, 536-541 (1965) · Zbl 0135.18401
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.