Abstract
It is well-known that focusing striates a sequent derivation into phases of like polarity where each phase can be seen as inferring a synthetic connective. We present a sequent calculus of synthetic connectives based on neutral proof patterns, which are a syntactic normal form for such connectives. Different focusing strategies arise from different polarisations and arrangements of synthetic inference rules, which are shown to be complete by synthetic rule permutations. A simple generic cut-elimination procedure for synthetic connectives respects both the ordinary focusing and the maximally multi-focusing strategies, answering the open question of cut-admissibility for maximally multi-focused proofs.
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
Abramsky, S.: Sequentiality vs. concurrency in games and logic. Mathematical Structures in Computer Science 13(4), 531–565 (2003)
Abramsky, S., Melliès, P.-A.: Concurrent games and full completeness. In: 14th Symp. on Logic in Computer Science, pp. 431–442. IEEE Computer Society Press, Los Alamitos (1999)
Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. of Logic and Computation 2(3), 297–347 (1992)
Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 92–106. Springer, Heidelberg (2007)
Chaudhuri, K., Miller, D., Saurin, A.: Canonical sequent proofs via multi-focusing. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) Fifth IFIP International Conference on Theoretical Computer Science. IFIP International Federation for Information Processing, vol. 273, pp. 383–396. Springer, Boston (2008)
Chaudhuri, K., Pfenning, F.: Focusing the inverse method for linear logic. In: Luke Ong, C.-H. (ed.) CSL 2005. LNCS, vol. 3634, pp. 200–215. Springer, Heidelberg (2005)
Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. J. of Automated Reasoning 40(2-3), 133–177 (2008)
Danos, V., Joinet, J.-B., Schellinx, H.: LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. London Mathematical Society Lecture Note Series, vol. 222, pp. 211–224. Cambridge University Press, Cambridge (1995)
Delande, O., Miller, D.: A neutral approach to proof and refutation in MALL. In: Pfenning, F. (ed.) 23th Symp. on Logic in Computer Science, pp. 498–508. IEEE Computer Society Press, Los Alamitos (2008)
Girard, J.-Y.: Locus solum. Mathematical Structures in Computer Science 11(3), 301–506 (2001)
Kleene, S.C.: Permutabilities of inferences in Gentzen’s calculi LK and LJ. Memoirs of the American Mathematical Society 10, 1–26 (1952)
Laurent, O.: Etude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille II (March 2002)
Laurent, O.: Syntax vs. semantics: a polarized approach. Prépublication électronique PPS//03/04//no 17 (pp), Laboratoire Preuves, Programmes et Systèmes (Submitted) (March 2003)
Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science (accepted, 2008)
Miller, D., Saurin, A.: From proofs to focused proofs: A modular proof of focalization in linear logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 405–419. Springer, Heidelberg (2007)
Wadler, P.: Call-by-value is dual to call-by-name. In: 8th Int. Conf. on Functional Programming, pp. 189–201 (2003)
Zeilberger, N.: Focusing and higher-order abstract syntax. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 359–369. ACM, New York (2008)
Zeilberger, N.: On the unity of duality. Ann. of Pure and Applied Logic (to appear, 2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chaudhuri, K. (2008). Focusing Strategies in the Sequent Calculus of Synthetic Connectives. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)