Abstract
For an efficient proof search in non-classical logics, particular in intuitionistic and modal logics, two similar approaches have been established: Wallen's matrix characterization and Ohlbach's resolution calculus. Beside the usual term-unification both methods require a specialized string-unification to unify the so-called prefixes of atomic formulae (in Wallen's notation) or world-paths (in Ohlbach's notation). For this purpose we present an efficient algorithm, called T-String-Unification, which computes a minimal set of most general unifiers. By transforming systems of equations we obtain an elegant unification procedure, which is applicable to the intuitionistic logic J and the modal logic S4. With some modifications we are also able to treat the modal logics D, K, D4, K4, S5, and T. We explain our method by an intuitive graphical presentation, prove correctness, completeness, minimality, and termination and investigate its complexity.
Supported by the Adolf Messer Stiftung
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
H. Abdulrab and J.-P. Pecuchet. Solving word equations. In C. Kirchner, editor, Unification, pages 353–375. Academic Press, London, 1990.
B. Beckert and J. Posegga. leanTAP: Lean tableau-based theorem proving. In Alan Bundy, editor, Proceedings of the 12th Conference on Automated Deduction, LNAI 814, Springer Verlag, 1994.
E. W. Beth. The foundations of mathematics. North-Holland, 1959.
W. Bibel, S. Brüning, U. Egly, T. Rath. Komet. In Alan Bundy, editor, Proceedings of the 12th Conference on Automated Deduction, LNAI 814, pages 783–787. Springer Verlag, 1994.
W. Bibel. On matrices with connections. Jour. of the ACM, 28, p. 633–645, 1981.
W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.
J. J. Herbrand. Recherches sur la théorie de la démonstration. Travaux Soc. Sciences et Lettres Varsovie, Cl. 3 (Mathem., Phys.), page 128 pp., 1930. Engl. transl. in W. D. Goldfarb, ed. J.J. Herbrand — Logical writings, Reidel, 1971.
R. Letz, J. Schumann, S. Bayerl, W. Bibel. Setheo: A high-performance theorem prover. Journal of Automated Reasoning, 8:183–212, 1992.
G. S. Makanin. The problem of solvability of equations in a free semigroup. Math. Sb., 103(145):147–236, 1977. English translation: Math. USSR Sb. 32.
G. S. Makanin. Algorithmic decidability of the rank of constant free equations in a free semigroup. Dokl. Akad. Nauk, SSSR, 243, 1978.
A. Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS), 4:258–282, 1982.
H. J. Ohlbach. A resolution calculus for modal logics. Ph.D. Thesis (SEKI Report SR-88-08), Universität Kaiserslautern, 1988.
H. J. Ohlbach. A resolution calculus for modal logics. In E. Lusk and R. Overbeek, editors, Proceedings of the 9 th Conference on Automated Deduction, LNCS 310, pages 500–515. Springer Verlag, 1988.
J. Otten, C. Kreitz. A connection based proof method for intuitionistic logic. In Proceedings of the 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pp. 122–137, Springer Verlag, 1995.
J. Otten. Ein konnektionenorientiertes Beweisverfahren für intuitionistische Logik. Master's thesis, TH Darmstadt, 1995.
G. Plotkin. Building-in Equational Theories. Machine Intelligence, 7:73–90, Edinburgh University Press, 1972.
J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12(1):23–41, January 1965.
M. Schmidt-Schauss. Unification in a combination of arbitrary disjoint equational theories. In E. Lusk and R. Overbeek, editors, Proceedings of the 9 th Conference on Automated Deduction, LNCS 310, pages 378–392. Springer Verlag, 1988.
L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.
L. Wos et. al. Automated reasoning contributes to mathematics and logic. In Proceedings of the 10 th Conference on Automated Deduction, LNCS 449, pages 485–499. Springer Verlag 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Otten, J., Kreitz, C. (1996). T-string unification: Unifying prefixes in non-classical proof methods. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds) Theorem Proving with Analytic Tableaux and Related Methods. TABLEAUX 1996. Lecture Notes in Computer Science, vol 1071. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61208-4_16
Download citation
DOI: https://doi.org/10.1007/3-540-61208-4_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61208-7
Online ISBN: 978-3-540-68368-1
eBook Packages: Springer Book Archive