36
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Extending a system in the calculus of structures with a self-dual quantifier

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          We recall that SBV, a proof system developed under the methodology of deep inference, extends multiplicative linear logic with the self-dual non-commutative logical operator Seq. We introduce SBVQ that extends SBV by adding the self-dual quantifier Sdq. The system SBVQ is consistent because we prove that (the analogous of) cut elimination holds for it. Its new logical operator Sdq operationally behaves as a binder, in a way that the interplay between Seq, and Sdq can model {\beta}-reduction of linear {\lambda}-calculus inside the cut-free subsystem BVQ of SBVQ. The long term aim is to keep developing a programme whose goal is to give pure logical accounts of computational primitives under the proof-search-as-computation analogy, by means of minimal, and incremental extensions of SBV.

          Related collections

          Most cited references8

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          Non-commutativity and MELL in the Calculus of Structures

            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            A Purely Logical Account of Sequentiality in Proof Search

              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              A Non-commutative Extension of MELL

                Bookmark

                Author and article information

                Journal
                18 December 2012
                Article
                10.1093/logcom/exu033
                1212.4483
                961bf17d-6ae0-4fe9-aa52-afc889ed6312

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                29 pages
                cs.LO

                Comments

                Comment on this article