×

zbMATH — the first resource for mathematics

The disconnection tableau calculus. (English) Zbl 1121.03022
Summary: In this paper we give a comprehensive presentation of the disconnection tableau calculus, a proof method for formulas in classical first-order clause logic. The distinguishing property of this calculus is that it uses unification in such a manner that important proof-theoretic advantages of the classical (i.e., Smullyan-style) tableau calculus are preserved, specifically the termination and model generation characteristics for certain formula classes. Additionally, the calculus is well suited for fully automated proof search. The calculus is described in detail with soundness and completeness proofs, and a number of important calculus refinements developed over the past years are presented. Referring to the model-finding abilities of the disconnection calculus, we explain the extraction and representation of models. We also describe the integration of paramodulation-based equality handling. Finally, we give an overview of related methods.
MSC:
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andrews, P.B.: Theorem proving through general matings. J. Assoc. Comput. Mach. 28, 193–214 (1981) · Zbl 0456.68119
[2] Avenhaus, J.: Reduktionssysteme. Springer, Berlin Heidelberg New York (1995)
[3] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998) · Zbl 0948.68098
[4] Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Ait-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, vol. 2, pp. 1–30. Academic, New York (1989)
[5] Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994) · Zbl 0814.68117
[6] Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmidt, P.H. (eds.) Automated Deduction: A Basis for Applications Foundations: Calculi and Methods, vol. 1, pp. 353–398. Kluwer, Dordrecht, The Netherlands (1998) · Zbl 0973.68215
[7] Baumgartner, P.: Hyper Tableaux – the next generation. In: de Swart, H. (ed.) Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands. Lecture Notes in Computer Science, vol. 1397, pp. 60–76. Springer, Berlin Heidelberg New York (1998) · Zbl 0910.03007
[8] Baumgartner, P.: FDPLL – A first-order Davis–Putnam–Logeman–Loveland procedure. In: McAllester, D. (ed.) Proceedings of the 17th International Conference on Automated Deduction (CADE-17), Pittsburgh. Lecture Notes in Artificial Intelligence, vol. 1831, pp. 200–219. Springer, Berlin Heidelberg New York (2000)
[9] Baumgartner, P., Eisinger, N., Furbach, U.: A confluent connection calculus. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction (CADE), Trento, Italy. Lecture Notes in Computer Science, vol. 1632, pp. 329–343. Springer, Berlin Heidelberg New York (1999) · Zbl 0937.03016
[10] Baumgartner, P., Furbach, U., Niemelä, I.: Hyper tableaux. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds.) Proceedings of the European JELIA Workshop (JELIA-96): Logics in Artificial Intelligence. Lecture Notes in Artificial Intelligence, vol. 1126, pp. 1–17. Springer, Berlin Heidelberg New York (1996)
[11] Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) Automated Deduction – CADE-19. Lecture Notes in Artificial Intelligence, vol. 2741, pp. 350–364. Springer, Berlin Heidelberg New York (2003) · Zbl 1278.68249
[12] Baumgartner, P., Tinelli, C.: The model evolution calculus with equality. In: Nieuwenhuis, R. (ed.) CADE-20 – The 20th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 3632, pp. 392–408. Springer, Berlin Heidelberg New York (2005) · Zbl 1135.03325
[13] Beckert, B.: Rigid E-unification. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction – A Basis for Applications. Foundations, vol. 1, pp. 265–289. Kluwer, Dordrecht, The Netherlands (1998) · Zbl 0973.68213
[14] Beckert, B.: Depth-first proof search without backtracking for free-variable clausal tableaux. J. Symb. Comput. 36, 117–138 (2003) · Zbl 1019.03006
[15] Beckert, B., Gerberding, S., Hähnle, R., Kernig, W.: The tableau-based theorem prover \(_{3}{T}^{{{A}}}{P}\) for multiple-valued logics. In: Proceedings, 11th International Conference on Automated Deduction (CADE), Saratoga Springs, NY. Lecture Notes in Computer Science, vol. 607, pp. 758–760. Springer, Berlin Heidelberg New York (1992)
[16] Beckert, B., Hähnle, R.: Analytic tableaux. In: Automated Deduction – A Basis for Applications. Foundations, vol. 1, pp. 11–41. Kluwer, Dordrecht, The Netherlands (1998) · Zbl 0971.03018
[17] Beckert, B., Posegga, J.: leanTAP: lean tableau-based deduction. J. Autom. Reason. 15(3), 339–358 (1995) · Zbl 0838.68097
[18] Beth, E.W.: Semantic entailment and formal derivability. Meded. K. Ned. Akad. Wet. 18(13), 309–342 (1955)
[19] Bibel, W.: On matrices with connections. J. Assoc. Comput. Mach. 633–645 (1981) · Zbl 0468.68097
[20] Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg-Verlag, Braunschweig, Germany (1987)(revised) · Zbl 0639.68092
[21] Billon, J.-P.: The disconnection method: a confluent integration of unification in the analytic framework. In: Proceedings, 5th TABLEAUX. Lecture Notes in Artificial Intelligence, vol. 1, pp. 110–126. Springer, Berlin Heidelberg New York (1996)
[22] Brand, D.: Proving theorems with the modification method. SIAM J. Comput. 4(4), 412–430 (1975) · Zbl 0333.68059
[23] Cohen, J., Trilling, L., Wegner, P.: A nucleus of a theorem-prover described in ALGOL-68. Int. J. Comput. Inf. Sci. 3(1), 1–31 (1974) · Zbl 0276.68038
[24] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5, 394–397 (1962) · Zbl 0217.54002
[25] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. Assoc. Comput. Mach. 7(3), 201–215 (1960) · Zbl 0212.34203
[26] Dershowitz, N., Plaisted, D.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 535–610. Elsevier, Amsterdam, The Netherlands (2001)(Chapt. 9) · Zbl 0992.68123
[27] Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Berlin Heidelberg New York (1996)(revised) · Zbl 0848.68101
[28] Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), Los Alamitos, CA, vol. 9, pp. 55–64. IEEE Computer Society, Washington, DC (2003)
[29] Gentzen, G.: Untersuchungen über das logische Schließen. Math. Z. 39, 176–210, 405–431 (1935) (English translation) In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North Holland, Amsterdam, The Netherlands (1969) · JFM 60.0020.02
[30] Giese, M.: Model generation style completeness proofs for constraint tableaux with superposition. Technical Report 2001-20, Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, Germany (2001)
[31] Giese, M.: Simplification rules for constrained formula tableaux. In: Mayer, M.C., Pirri, F. (eds.) Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Rome, Italy. Lecture Notes in Computer Science, vol. 2796, pp. 65–80. Springer, Berlin Heidelberg New York (2003) · Zbl 1274.03020
[32] Hooker, J., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first-order logic. J. Autom. Reason. 28(5), 371–396 (2002) · Zbl 0995.03010
[33] Lee, S.-J., Plaisted, D.: Eliminating duplication with the hyper-linking strategy. J. Autom. Reason. 9(1), 25–42 (1992) · Zbl 0784.68077
[34] Letz, R.: First-order calculi and proof procedures for automated deduction. Ph.D. Thesis, Technieche Hochschule, Darmstadt (1993)
[35] Letz, R.: On the polynomial transparency of resolution. In: Bajcsy, R. (ed.) Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI), France, Chambery, pp. 123–129. Morgan Kaufmann, San Mateo, CA (1993)
[36] Letz, R.: LINUS: a link instantiation prover with unit support. J. Autom. Reason. 18(2), 205–210 (1997) · Zbl 05468573
[37] Letz, R.: Clausal tableaux. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction – A Basis for Applications. Foundations, vol. 1, pp. 43–72. Kluwer, Dordrecht, The Netherlands (1998) · Zbl 0966.03013
[38] Letz, R.: First-order tableaux methods. In: D’Agostino, M., Gabbay, D., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 125–196. Kluwer, Dordrecht, The Netherlands (1999)
[39] Letz, R., Mayr, K., Goller, C.: Controlled integration of the cut rule into connection Tableau calculi. J. Autom. Reason. 13(3), 297–338 (1994) · Zbl 0816.03005
[40] Letz, R., Stenz, G.: DCTP: a disconnection calculus theorem prover. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2001), Siena, Italy. Lecture Notes in Artificial Intelligence, vol. 2083, pp. 381–385. Springer, Berlin Heidelberg New York (2001) · Zbl 0988.68589
[41] Letz, R., Stenz, G.: Proof and model generation with disconnection tableaux. In: Voronkov, A. (ed.) Proceedings of the 8th LPAR, Havanna, Cuba, vol. 2250, pp. 142–156. Springer, Berlin Heidelberg New York (2001) · Zbl 1275.03081
[42] Letz, R., Stenz, G.: Integration of equality reasoning into the disconnection calculus. In: Proceedings, TABLEAUX-2002, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2381, pp. 176–190. Springer, Berlin Heidelberg New York (2002) · Zbl 1015.68172
[43] Letz, R., Stenz, G.: Generalised handling of variables in disconnection tableaux. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2004), Cork, Ireland. Lecture Notes in Artificial Intelligence, vol. 3097, pp. 289–306. Springer, Berlin Heidelberg New York (2004) · Zbl 1126.03305
[44] Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) 9th International Conference on Automated Deduction (CADE), Argonne, IL, vol. 310, pp. 415–434. Springer, Berlin Heidelberg New York (1988) · Zbl 0668.68104
[45] Massacci, F.: Simplification: a general constraint propagation technique for propositional and modal tableaux. In: de Swart, H. (ed.) Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands, vol. 1397, pp. 217–231. Springer, Berlin Heidelberg New York (1998) · Zbl 0903.03012
[46] Moser, M.: Goal-directed reasoning in clausal logic with equality. Ph.D. Thesis, Fakultät für Informatik, Technische Universität München, München, Germany (1996)
[47] Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J., Mayr, K.: SETHEO and E-SETHEO – the CADE-13 systems. J. Autom. Reason. 18(2), 237–246 (1997) · Zbl 05468577
[48] Moser, M., Steinbach, J.: STE-modification revisited. AR-Report AR-97-03, Fakultät für Informatik, Technische Universität München (1997)
[49] Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 371–443. Elsevier, Amsterdam, The Netherlands (2001)(Chapt. 7) · Zbl 0997.03012
[50] Nutt, W., Réty, P., Smolka, G.: Basic narrowing revisited. J. Symb. Comput. 7(3–4), 295–318 (1989) · Zbl 0682.68094
[51] Oppacher, F., Suen, E.: HARP: a tableau-based theorem prover. J. Autom. Reason. 4, 69–100 (1988)
[52] Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reason. 25(3), 167–217 (2000) · Zbl 0959.68115
[53] Prawitz, D.: An improved proof procedure. Theoria 26, 102–139 (1960) (Reprinted in [58]) · Zbl 0099.00801
[54] Prawitz, D.: Advances and problems in mechanical proof procedures. In: Automation of Reasoning, 1983, pp. 285–297. Springer, Berlin Heidelberg New York (1969) (reprinted) · Zbl 0257.68082
[55] Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 23–41 (1965) · Zbl 0139.12303
[56] Schulz, S., Sutcliffe, G.: System description: GrAnDe 1.0. In: Voronkov, A. (ed.) Proceedings of the 18th CADE, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2392, pp. 280–284. Springer, Berlin Heidelberg New York (2002) · Zbl 1072.68590
[57] Shostak, R.E.: Refutation graphs. Artif. Intell. 7, 51–64 (1976) · Zbl 0328.68080
[58] Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning. Springer, Berlin Heidelberg New York (1983) (Two volumes) · Zbl 0567.03002
[59] Smullyan, R.: First-order logic. Springer, Berlin Heidelberg New York (1968) · Zbl 0172.28901
[60] Stenz, G.: DCTP 1.2 – system abstract. In: Proceedings of TABLEAUX-2002, Copenhagen, Denmark. Lecture Notes in Artificial Intelligence, vol. 2381, pp. 335–340. Springer, Berlin Heidelberg New York (2002) · Zbl 1015.68542
[61] Stenz, G.: The disconnection calculus. Dissertation, Fakultät für Informatik, Technische Universität München, Logos Verlag, Berlin (2002)
[62] Tseitin, G.: On the complexity of proofs in propositional logics. Semin. Math. 8, (1970)
[63] Zhang, H.: SATO: an efficient propositional prover. In: McCune, W. (ed.) Proceedings of the 14th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 1249, pp. 272–275. Springer, Berlin Heidelberg New York (1997)
[64] Zhang, H., Stickel, M.E.: An efficient algorithm for unit propagation. In: Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH’96), pp. 166–169. Fort Lauderdale, FL (1996)
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.