Abstract
This work is a study of the inter-translatability of two closely related proof methods, i.e. tableau (or sequent) and connection based, in the case of the propositional modal logics K, K4, T, S4, paying particular attention to the relation between matrix multiplicity and multiple use of ν 0-formulae (contractions) in tableaux/sequent proofs.
The motivation of the work is the following. Since the role of a multiplicity in matrix methods is the encoding of the number of copies of a given formula that are needed in order to prove a valid formula, it is important to find upper bounds for multiplicities in order to reduce as much as possible the search space for proofs. Moreover, it is obviously a crucial issue if the matrix method is to be used as a decision method. We exploit previous results establishing upper bounds on the number of contractions in tableau/sequent proofs [4], in order to establish upper bounds for multiplicities in matrix systems.
We obtain two kinds of upper bounds: in function of the size of the formula to be proved and in function of the number of the atomic paths through the unindexed formula-tree. Such bounds may be non-optimal. However, the method used to establish them may be useful for obtaining finer upper bounds.
This work has been partially supported by the Italian MURST project “Rappresentazione della Conoscenza e Meccanismi di Ragionamento” and by ASI — Agenzia Spaziale Italiana.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Andrews. Transforming matings into natural deduction proofs. In Proc. of CADE-5, pages 281–292, 1980.
W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.
W. Bibel, D. Korn, C. Kreitz, and S. Schmitt. Problem-oriented applications of automated theorem proving. In Proc. of DISCO-96, pages 1–21, 1996.
S. Cerrito and M. Cialdea Mayer. A polynomial translation of S4 into T and contraction free tableaux for S4. Logic Journal of the IGPL, 5(2):287–300, 1997.
M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel Publishing Company, 1983.
M. Fitting. First-order modal tableaux. Journal of Automated Reasoning, 4:191–213, 1988.
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.
A. Heuerding, M. Seyfried, and H. Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. In Proc. of the 5th Int. Workshop on Theorem Proving with Analytic Tableaux and Related Methods (Tableaux '96), 1996.
J. Hudelmaier. Improved decision procedures for the modal logics K, T and S4. In Proc. of the 9th International Workshop, CSL'95, Annual Conference of the EACSL, pages 320–333. Springer Verlag, LNCS 1092, 1995.
G. E. Hughes and M. J. Cresswell. An Introduction to Modal Logic. Methuen & Co., 1968.
R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal of Computation, 6:467–480, 1977.
F. Massacci. Strongly analytic tableaux for normal modal logics. In Proceedings of CADE-12, pages 723–737, 1994.
M. Ohnishi and K. Matsumoto. Gentzen method in modal calculi. Osaka Mathematical Journal, 9:113–130, 1957.
S. Schmitt and C. Kreitz. On transforming intuitionistic matrix proofs into standard sequent proof. In Proc. of the 4th Int. Workshop on Theorem Proving with Analytic Tableaux and Related Methods (Tableaux '95), pages 106–153, 1995.
S. Schmitt and C. Kreitz. Converting non-classical matrix proofs into sequent-style systems. In Proc. of CADE-13, 1996.
L. A. Wallen. Generating connection calculi from tableau-and sequent-based proof systems. In A. G. Cohn and J. R. Thomas, editors, Artificial Intelligence and its Applications, pages 35–50. John Wiley & Sons, 1986.
L. A. Wallen. Matrix proof methods for modal logic. In Proc. of the 10th International Joint Conference on Artificial Intelligence (IJCAI-10), pages 917–923, 1987.
L. A. Wallen. Automated Deduction in Nonclassical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics. MIT Press, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cerrito, S., Mayer, M.C. (1997). Hintikka multiplicities in matrix decision methods for some propositional modal logics. In: Galmiche, D. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1997. Lecture Notes in Computer Science, vol 1227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027410
Download citation
DOI: https://doi.org/10.1007/BFb0027410
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62920-7
Online ISBN: 978-3-540-69046-7
eBook Packages: Springer Book Archive