Abstract
We define sequent-style calculi for nominal tense logics characterized by classes of modal frames that are first-order definable by certain П 01 -formulae and П 02 -formulae. The calculi are based on d’Agostino and Mondadori’s calculus KE and therefore they admit a restricted cutrule that is not eliminable. A nice computational property of the restriction is, for instance, that at any stage of the proof, only a finite number of potential cut-formulae needs to be taken under consideration. Although restrictions on the proof search (preserving completeness) are given in the paper and most of them are theoretically appealing, the use of those calculi for mechanization is however doubtful. Indeed, we present sequent calculi for fragments of classical logic that are syntactic variants of the sequent calculi for the nominal tense logics.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. Baldoni. Normal Multimodal Logics: Automated Deduction and Logic Programming. PhD thesis, Università degli Studi di Torino, 1998.
J. van Benthem. Modal logic and classical logic. Bibliopolis, 1983.
B. Beckert and R. Goré. Free variable tableaux for propositional modal logics. In TABLEAUX’97, pages 91–106. LNAI 1227, Springer, 1997.
N. Bonnette and R. Goré. A labelled sequent systems for tense logic Kt. In Australian Joint Conference of Articifial Intelligence, pages 71–82. LNAI 1502, Springer, 1998.
P. Blackburn. Nominal tense logic. Notre Dame Journal of Formal Logic, 34(1):56–83, 1993.
P. Blackburn. Internalizing labeled deduction. Technical Report 102, Computerlinguistik, Universität des Saarlandes, 1998.
D. Basin, S. Matthews, and L. Viganò. Labelled propositional modal logics: Theory and practice. J. of Logic and Computation, 7(6):685–717, 1997.
D. Basin, S. Matthews, and L. Viganò. Natural deduction for non-classical logics. Studia Logica, 60(1):119–160, 1998.
G. Boolos. Don’t eliminate cut. J. of Philosophical Logic, 13:373–378, 1984.
M. Castilho, L. Fariñas del Cerro, O. Gasquet, and A. Herzig. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae, 32(3/4):281–297 1997.
M. d’Agostino. Investigations into the complexity of some propositional calculi. PhD thesis, Oxford University Computing Laboratory, 1990.
S. Demri and R. Goré. Cut-free display calculi for nominal tense logics. In this volume, 1999.
M. d’Agostino and M. Mondadori. The taming of the cut. Classical refutations with analytic cut. J. of Logic and Computation, 4(3):285–319, 1994.
M. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel Publishing Co., 1983.
D. Gabbay. Labelled Deductive Systems. Oxford University Press, 1996.
I. Gent. Analytic proof systems for classical and modal logics of restricted quantification. PhD thesis, University of Warwick, 1992.
G. Gargov and V. Goranko. Modal logic with names. J. of Philosophical Logic, 22(6):607–636, 1993.
H. Ganzinger, U. Hustadt, and R. Meyer and C. Schmidt. A resolution-based decision procedure for extensions of K4. In 2nd Workshop on Advances in Modal Logic, 1998. to appear.
R Goré. Tableaux methods for modal and temporal logics. In Handbook of Tableaux Methods. Kluwer, Dordrecht, 1999. to appear.
G. Governatori. Labelled tableaux for multi-modal logics. In TABLEAUX-4, pages 79–94. LNAI 918, Springer, 1995.
A. Heuerding. Sequent Calculi for Proof Search in Some Modal Logics. PhD thesis, University of Bern, 1998.
J. Hudelmaier. Improved decision procedures for the modal logics K, KT and S4. In CSL’95, pages 320–334. LNCS 1092, Springer, 1996.
B. Konikowska. A logic for reasoning about relative similarity. Studia Logica, 58(1):185–226, 1997.
M. Kracht. Power and weakness of the modal display calculus. In H. Wansing, editor, Proof theory of modal logic, pages 93–121. Kluwer Academic Publishers, 1996.
S. Kripke. Semantical analysis of modal logic I: normal modal propositional calculi. Zeitschrift für Mathematik Logik und Grundlagen der Mathematik, 9:67–96, 1963.
F. Massacci. Strongly analytic tableaux for normal modal logics. In CADE-12, pages 723–737. Springer, LNAI 814, 1994.
Z. Ognjanović. A tableau-like proof procedure for normal modal logics. TCS, 129:167–186, 1994.
A. Prior. Time and Modality. Clarendon Press, Oxford, 1957.
N. Rescher and A. Urquhart. Temporal Logic. Springer-Verlag, 1971.
A. Russo. Modal logics as labelled deductive systems. PhD thesis, Imperial College, London, 1996.
M. Tzakova. Tableau calculi for hybrid logics. In this volume, 1999.
L. Wallen. Automated Deduction in Nonclassical Logics. MIT Press, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Demri, S. (1999). Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_15
Download citation
DOI: https://doi.org/10.1007/3-540-48754-9_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66086-6
Online ISBN: 978-3-540-48754-8
eBook Packages: Springer Book Archive