Abstract.
We start from the Forum presentation of first order linear logic to design an equivalent system for which proof search is highly structured. We restrict formulae to a language of clauses and goals, without losing expressivity, in such a way that formulae have the same structure of Forum sequents. This means having a very big generalised connective that suffices for all of linear logic. We can then design a system with only two big rules, a left one and a right one. The behaviour of such system in proof search is operationally interesting and makes it suitable for further semantic investigations. We test the mutual harmony of the new rules by showing a cut elimination theorem.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Brünnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 347–361. Springer, Heidelberg (2001), http://www.ki.inf.uni-dresden.de/~kai/LocalClassicalLogic-lpar.pdf
Bruscoli, P.: A purely logical account of sequentiality in proof search. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS (LNAI), vol. 2401, pp. 302–316. Springer, Heidelberg (2002), http://www.ki.inf.uni-dresden.de/~paola/bvl/bvl.pdf
Bruscoli, P., Guglielmi, A.: On structuring proof search for first order linear logic. Technical Report WV-03-10, Technische Universität Dresden (2003), http://www.ki.inf.uni-dresden.de/~paola/sps/sps.pdf
Gallier, J.: Constructive logics. Part I: A tutorial on proof systems and typed λ-calculi. Theoretical Computer Science 110, 249–339 (1993)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Guglielmi, A.: Abstract Logic Programming in Linear Logic—Independence and Causality in a First Order Calculus. PhD thesis, Università di Pisa (1996)
Guglielmi, A.: A system of interaction and structure. Technical Report WV-02-10, Technische Universität Dresden, Submitted to ACM Transactions on Computational Logic (2002), http://www.ki.inf.unidresden.de/~guglielm/Research/Gug/Gug.pdf
Miller, D.: A multiple-conclusion meta-logic. In: Abramsky, S. (ed.) Ninth Annual IEEE Symp. on Logic in Computer Science, Paris, July 1994, pp. 272–281 (1994)
Miller, D.: Forum: A multiple-conclusion specification logic. Theoretical Computer Science 165, 201–232 (1996)
Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157 (1991)
Straßburger, L.: MELL in the calculus of structures. Technical Report WV-01-03, Technische Universität Dresden (2001) (to appear in Theoretical Computer Science), http://www.ki.inf.unidresden.de/~lutz/els.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bruscoli, P., Guglielmi, A. (2003). On Structuring Proof Search for First Order Linear Logic. In: Vardi, M.Y., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2003. Lecture Notes in Computer Science(), vol 2850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39813-4_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-39813-4_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20101-4
Online ISBN: 978-3-540-39813-4
eBook Packages: Springer Book Archive