Abstract
This paper describes a proof search system for a modal substructural (concatenation) logic based on Gabbay's Labelled Deductive System (LDS) as a case study. The logic combines resource (linear or Lambek Calculus) with modal features, and has applications in AI and natural language processing. We present axiomatic and LDS style proof theories and semantics for the logic, with soundness and completeness results. For non-classical logic theorem proving, we show that LDS is flexible and generic, and can be mechanised directly. This partially verifies Gabbay's open claims that LDS is suitable to study combinations of logics. We believe our approach can be extended to any variant which combines substructurality and modality.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Benevides and T. S. E. Maibaum. A constructive presentation for the modal connective of necessity. J. Logic & Comp., 2(1):31–50, 1992.
J. F. A. K. v. Benthem. Language in Action. North-Holland, 1991.
R. A. Bull and K. Segerberg. Basic Modal Logic. In D. Gabbay and F. Guenthner, ed., Handbook of Philosophical Logic, vol II, D. Reidel, 1984.
H. F. Chau. A proof search system for a modal substructural logic based on LDS. Tech. report, Dept. of Comp., Imperial Coll., Jan 1993. 18 pages.
M. D'Agostino and D. M. Gabbay. Labelled refutation systems: A study of substructural logics. Draft Manuscript, Imperial College, Nov 1992.
K. Dosen. A brief survey of frames for the Lambek Calculus. ZML, 38: 179–187, 1992.
M. C. Fitting. Proof Methods for Modal and Intuitionistic Logics. D. Reidel, Dordrecht, 1983.
D. M. Gabbay. Labelled Deductive Systems — Part I. Tech Rep CIS 90-22, CIS, U. München, Dec 1990. Draft Version 5, OUP (Forthcoming).
D. Gabbay and R. de Queiroz. Extending Curry-Howard interpretation to Linear, Relevance and other resource logics. JSL, 57:1319–1365, 1992.
J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50:1–102, 1987.
S. Hölldobler. On deductive planning and the frame problem. In Proceedings of LPAR'92, pages 13–29, July 1992. LNAI, Springer.
N. Kurtonina. On modal extension of the lambek calculus. Manuscript, Cent. Logic, Cath. Univ. Leuven, Dec 1992.
M. Moortgat. Labelled deductive systems for categorial theorem proving (extended abstract). In Proceedings of 8th Amsterdam Colloquium, 1991.
D. Roorda. Lambek Calculus and Boolean Connectives: On the road. Working Papers OTS-WP-CL-92-004, OTS, U. Utrecht, 1992.
Y. Venema. Meeting strength in substructural logics. Logic Group Preprint 38, Dept. of Phil., U. Utrecht,, Jan 1993.
L. A. Wallen. Automated Deduction in Non-Classical Logics. MIT Press, Mass., 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chau, H.F. (1993). A proof search system for a modal substructural logic based on labelled deductive systems. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1993. Lecture Notes in Computer Science, vol 698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56944-8_42
Download citation
DOI: https://doi.org/10.1007/3-540-56944-8_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56944-2
Online ISBN: 978-3-540-47830-0
eBook Packages: Springer Book Archive