Abstract
In this paper, we investigate automated proof construction in classical linear logic (CLL) by giving logical foundations for the design of proof search strategies. We propose common theoretical foundations for top-down, bottom-up and mixed proof search procedures with a systematic formalization of strategies construction using the notions of immediate or chaining composition or decomposition, deduced from permutability properties and inference movements in a proof. Thus, we have logical bases for the design of proof strategies in CLL fragments and then we can propose sketches for their design.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1–2):3–58, 1993.
J.M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.
G. Bellin. Proof nets for multiplicative and additive linear logic. Technical Report ECS-LFCS 91-161, Department of Computer Science, Edinburgh University, May 1991.
J. Chirimar and J. Lipton. Provability in TBLL: a decision procedure. In CSL'91, LNCS 626, pages 53–65, Bern, October 1991.
D. Galmiche and G. Perrier. Automated deduction in additive and multiplicative linear logic. In Logic at Tver'92, Logical Foundations of Computer Science Symposium, LNCS 620, pages 151–162, Tver, Russia, July 1992.
D. Galmiche and G. Perrier. On proof normalisation in linear logic. Research report 93-R-059, CRIN-CNRS, 1992. To be published in Theoretical Computer Science.
J.Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.
J. Harland and D. Pym. On resolution in fragments of classical linear logic. In LPAR'92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 30–41, St. Petersburg, Russia, July 1992.
J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In 6th IEEE Symposium on Logic in Computer Science, pages 32–42, Amsterdam, The Netherlands, July 1991.
N. Kobayashi and A. Yonezawa. ACL — a concurrent linear logic programming paradigm. In Int. Symposium on Logic Programming, pages 279–294, Vancouver, October 1993.
P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56:239–311, 1992.
J. Meseguer and N. Marti-Oliet. From Petri nets to linear logic. In Category Theory and Computer Science, LNCS 389, pages 313–340, Manchester, September 1989.
N. Shankar. Proof search in the intuitionistic sequent calculus. In 11th Conference on Automated DEduction, LNAI 607, pages 522–536, Saratoga Springs, June 1992.
T. Tammet. Proof search strategies in linear logic. Programming Methodology Group Report 70, Chalmers University Group, University of Göteborg, 1993.
L.A. Wallen. Automated Proof search in Non-Classical Logics. MIT Press, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Galmiche, D., Perrier, G. (1994). Foundations of proof search strategies design in linear logic. In: Nerode, A., Matiyasevich, Y.V. (eds) Logical Foundations of Computer Science. LFCS 1994. Lecture Notes in Computer Science, vol 813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58140-5_11
Download citation
DOI: https://doi.org/10.1007/3-540-58140-5_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58140-6
Online ISBN: 978-3-540-48442-4
eBook Packages: Springer Book Archive