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. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Chaudhuri, K. (2008). Focusing strategies in the sequent calculus of synthetic connectives. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5330 LNAI, pp. 467–481). https://doi.org/10.1007/978-3-540-89439-1_33
Mendeley helps you to discover research relevant for your work.