The Focused Calculus of Structures
| Autor: | Chaudhuri, Kaustuv, Guenot, Nicolas, Straßburger, Lutz |
|---|---|
| Přispěvatelé: | Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Marc Bezem, Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France |
| Jazyk: | angličtina |
| Rok vydání: | 2011 |
| Předmět: |
000 Computer science
knowledge general works TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science 010102 general mathematics Computer Science [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 0102 computer and information sciences 0101 mathematics 01 natural sciences |
| Zdroj: | 20th EACSL Annual Conference on Computer Science Logic 20th EACSL Annual Conference on Computer Science Logic, Sep 2011, Bergen, Norway. pp.159-173, ⟨10.4230/LIPIcs.CSL.2011.159⟩ |
| DOI: | 10.4230/LIPIcs.CSL.2011.159⟩ |
| Popis: | International audience; The focusing theorem identifies a complete class of sequent proofs that have no inessential non-deterministic choices and restrict the essential choices to a particular normal form. Focused proofs are therefore well suited both for the search and for the representation of sequent proofs. The calculus of structures is a proof formalism that allows rules to be applied deep inside a formula. Through this freedom it can be used to give analytic proof systems for a wider variety of logics than the sequent calculus, but standard presentations of this calculus are too permissive, allowing too many proofs. In order to make it more amenable to proof search, we transplant the focusing theorem from the sequent calculus to the calculus of structures. The key technical contribution is an incremental treatment of focusing that avoids trivializing the calculus of structures. We give a direct inductive proof of the completeness of the focused calculus of structures with respect to a more standard unfocused form. We also show that any focused sequent proof can be represented in the focused calculus of structures, and, conversely, any proof in the focused calculus of structures corresponds to a focused sequent proof. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|