Abstract
In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. We then show that for most of the systems under consideration the labelling mechanism can be avoided by choosing an appropriate way of structuring theories. One peculiar feature of our proof systems is the use of restart rules which allow to re-ask the original goal of a deduction. In case of K, K4, S4 and G, we can eliminate such a rule, without loosing completeness. In all the other cases, by dropping such a rule, we get an intuitionistic variant of each system. The present results are part of a larger project of a goal directed proof theory for non-classical logics; the purpose of this project is to show that most implicational logics stem from slight variations of a unique deduction method, and from different ways of structuring theories. Moreover, the proof systems we present follow the logic programming style of deduction and seem promising for proof search [Gabbay and Reyle 84, Miller et al. 91].
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
M. Abadi, Z. Manna, ‘Modal theorem proving’, in Proc. 8th Int Conf. on Automated Deduction, LNCS 230, p. 172–189, Springer-Verlag, 1986.
P. Balbiani, A. Herzig, ‘A translation from modal logic G into K4’, J. Applied Non-Classical Logics 4(1): 73–77 (1994).
A. W. Bollen, ‘Relevant logic programming’, J. Automated Reasoning 7: 563–585 (1991)
G. Boolos, The Unprovability of Consistency — an essay in modal logic, Cambridge University Press, 1979.
C. Cerrato, ‘Modal sequents for normal modal logics’, Mathematical Logic Quarterly 39: 231–240 (1993).
C. Cerrato, ‘Natural deduction based upon strict implication for normal modal logics’, Notre Dame J. of Formal logic, 35(4): 471–495 (1994).
G. Corsi, ‘Weak logics with strict implication’, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33: 389–406 (1987).
K. Do{ie277-2}en, ‘Sequent systems for modal logic’, J. of Symbolic Logic 50: 149–168 (1985).
K. Do{ie277-4}en, ‘Logical constants as punctuation marks’, Notre Dame J. of Formal Logic 30(3): 363–381 (1989).
W. B. Ewald, ‘Intuitionistic tense and modal logic’, J. Symbolic Logic 51(1): 166–179 (1986).
L. FariÑas del Cerro, ‘MOLOG: a system that extends Prolog with modal logic’, New Generation Computing 4: 35–50 (1986).
M. Fitting, Proof Methods for Modal and Intuitionistic Logic, vol. 169 of Synthese Library, D. Reidel, Dorderecht, 1983.
M. Fitting, ‘Destructive modal resolution’, J. Logic and Computation 1(1): 83–98 (1990).
D. M. Gabbay, Elementary Logic — a procedural perspective, Lecture Notes, Imperial College 1984. Expanded version to appear, Prentice-Hall.
D. M. Gabbay, U. Reyle, ‘N-Prolog: an extension of Prolog with hypothetical implications I’, J. Logic Programming 4: 319–355 (1984).
D. M. Gabbay, ‘N-Prolog: an extension of Prolog with hypothetical implications. II. Logical foundations and negation as failure’, J. Logic Programming 4: 251–283 (1985).
D. M. Gabbay, ‘Modal and temporal logic programming’, in A. Galton (ed.), Temporal Logics and Their Applications, Academic Press, 1987.
D. M. Gabbay, ‘Algorithmic proof with diminishing resources’, in Proc. of CSL '90, LNCS vol. 533, p. 156–173, Springer-Verlag, 1991.
D. M. Gabbay, ‘Elements of algorithmic proof’, in S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (eds.), Handbook of Logic in Theoretical Computer Science, Oxford University Press, 1992.
D. M. Gabbay, ‘General theory of structured consequence relations’, in P. Schroeder-Heister, K. Dosen (eds.), Substructural Logics. Studies in Logic and Computation, p. 109–151, Oxford University Press, 1993.
D. M. Gabbay, ‘Fibred Semantics and the Weaving of Logics. Part I: modal and intuitionistic logic’, J. Symbolic Logic 61: 1057–1120 (1996).
D. M. Gabbay, F. Kriwaczek, ‘A family of goal-directed theorem-provers based on conjunction and implication’, J. of Automated Reasoning 7: 511–536 (1991).
D. M. Gabbay, N. Olivetti, ‘Goal-directed algorithmic proof theory’, Technical Report, Imperial College of Science, Technology and Medicine, London, 1996.
D. M. Gabbay, L. Giordano, A. Martelli, N. Olivetti, ‘A language for handling hypothetical updates and inconsistency’, J. of The IGPL 4(3): 385–416 (1996).
D. M. Gabbay, Labelled Deductive Systems (vol. I), Oxford Logic Guides, Oxford University Press, 1996.
L. Giordano, A. Martelli, ‘A modal reconstruction of blocks and modules in Logic Programming’, in Proc. of the 1991 International Logic Programming Symposium, San Diego, October, p. 239–253, 1991.
R. Gore, ‘Cut-free sequent and tableaux systems for propositional normal modal logics’, Technical Report 257, University of Cambridge, England, 1991.
R. Gore, ‘Tableaux for modal logics’, to appear in Handbook of Tableaux, D'Agostino et al. (eds.), Kluwer Academic Publisher.
J. Harland, D. Pym, ‘The uniform proof-theoretic foundation of linear logic programming’, in Proc. of the 1991 International Logic Programming Symposium, San Diego, October, p. 304–318, 1991.
J. Hodas, D. Miller, ‘Logic programming in a fragment of intuitionistic linear logic’, in G. Kahn (ed.), Sixth Annual Symposium on Logic in Computer Science, Amsterdam, 1991.
J. Hudelmaier, ‘On a contraction-free sequent calculus for modal logic S4’, in TABLEAUX94, 3rd Workshop on Theorem Proving with Analytic Tabelaux and Related Methods, Abingdon, UK, 1994.
D. W. Loveland, ‘Near-Horn Prolog and beyond’, J. of Automated Reasoning 7(1): 1–26 (1991).
D. W. Loveland, ‘A comparison of three Prolog extensions’, J. Logic Programming, 12: 25–50 (1992).
A. Masini, ‘2-Sequent calculus: a proof theory of modality’, Annals of Pure and Applied Logics 59: 115–149 (1992).
F. Massacci, ‘Strongly analytic tableau for normal modal logics’, in LNAI 814, p. 723–737, 1994.
L. T. McCarty, ‘Clausal intuitionistic logic. II. Tableau proof procedures’, J. of Logic Programming 5(2): 93–132 (1988).
C. A. Meredith, A. N. Prior, ‘Investigations into implicational S5’, Zeitschrift für Logik und Grundlagen der Mathematik 10: 203–220, 1964.
P. Miglioli, U. Moscato, M. Ornaghi, ‘Refutation systems for propositional modal logics’, in Proceeding of the Fourth Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, p. 95–115, Springer-Verlag, 1995.
D. A. Miller, ‘A logical analysis of modules in logic programming’, J. of Logic Programming 6: 79–108 (1989).
D. A. Miller, G. Nadathur, F. Pfenning, A. Scedrov, ‘Uniform proofs as a foundation for logic programming’, Annals of Pure and Applied Logic 51: 125–157 (1991).
D. A. Miller, ‘Abstract syntax and logic programming’, in Logic Programming: Proc. of the 2nd Russian Conference, Lecture Notes in Artificial Intelligence vol. 592, p. 322–337, Springer-Verlag, 1992.
A. N. Prior, ‘Some axiom-pairs for material and strict implication’, Zeitschr für Logik und Grundlagen der Mathematik 7: 61–65 (1961).
A. N. Prior, ‘The theory of implication’, Zeitschr für Logik und Grundlagen der Mathematik 9: 1–6 (1963).
H. Salqvist, ‘Completeness and correspondence in first-and second-order semantics of modal logics’, in S. Kanger (ed.), Proc. of the 3rd Scandinavian Logic Symposium, North Holland, 1975.
H. Wansing, ‘Sequent calculi for normal modal propositional logics’, J. of Logic and Computation 4(2): 125–142 (1994).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Gabbay, D.M., Olivetti, N. Algorithmic Proof Methods and Cut Elimination for Implicational Logics Part I: Modal Implication. Studia Logica 61, 237–280 (1998). https://doi.org/10.1023/A:1005077431494
Issue Date:
DOI: https://doi.org/10.1023/A:1005077431494