11 found
Order:
  1.  59
    The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
    We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   28 citations  
  2.  15
    Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic.Alexander V. Gheorghiu & David J. Pym - 2023 - Bulletin of the Section of Logic 52 (2):239-266.
    Proof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-eS). This semantics is given by a relation called support, explaining the meaning of the logical constants, which is parameterized by systems of rules called bases that provide the semantics of atomic propositions. In this paper, we interpret bases as collections of definite formulae and use (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  3.  9
    Reductive Logic, Proof-Search, and Coalgebra: A Perspective from Resource Semantics.Alexander V. Gheorghiu, Simon Docherty & David J. Pym - 2023 - In Alessandra Palmigiano & Mehrnoosh Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Verlag. pp. 833-875.
    The reductive, as opposed to deductive, view of logic is the form of logic that is, perhaps, most widely employed in practical reasoning. In particular, it is the basis of logic programming. Here, building on the idea of uniform proof in reductive logic, we give a treatment of logic programming for BI, the logic of bunched implications, giving both operational and denotational semantics, together with soundness and completeness theorems, all couched in terms of the resource interpretation of BI’s semantics. We (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  10
    Base-extension semantics for modal logic.Timo Eckhardt & David J. Pym - forthcoming - Logic Journal of the IGPL.
    In proof-theoretic semantics, meaning is based on inference. It may seen as the mathematical expression of the inferentialist interpretation of logic. Much recent work has focused on base-extension semantics, in which the validity of formulas is given by an inductive definition generated by provability in a ‘base’ of atomic rules. Base-extension semantics for classical and intuitionistic propositional logic have been explored by several authors. In this paper, we develop base-extension semantics for the classical propositional modal systems |$K$|⁠, |$KT$|⁠, |$K4$| and (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  5.  29
    Reductive logic and proof-search: proof theory, semantics, and control.David J. Pym - 2004 - New York: Oxford University Press. Edited by Eike Ritter.
    This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search including proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  5
    Reductive Logic and Proof-search: Proof Theory, Semantics, and Control.David J. Pym & Eike Ritter - 2004 - New York: Oxford University Press. Edited by Eike Ritter.
    This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search, areas of logic that are becoming important in computer science. A systematic foundational text on these emerging topics, it includes proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences. Suitable for researchers and graduate students in mathematical, computational and philosophical logic, and in (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  14
    Semantical Analysis of the Logic of Bunched Implications.Alexander V. Gheorghiu & David J. Pym - 2023 - Studia Logica 111 (4):525-571.
    We give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with eigenworlds (i.e., generic representatives of worlds) in an arbitrary model. This reasoning is captured by a sequent calculus for a _meta_-logic (in this case, first-order classical logic) expressive enough to capture the semantics of the object-logic. Essentially, one has a calculus of validity for the (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  8. A Synopsis on the Identification of Linear Logic Programming Languages.J. A. Harland & David J. Pym - 1992 - LFCS, Department of Computer Science, University of Edinburgh.
     
    Export citation  
     
    Bookmark  
  9. On Resolution in Fragments of Classical Linear Logic.J. A. Harland & David J. Pym - 1992 - LFCS, Department of Computer Science, University of Edinburgh.
     
    Export citation  
     
    Bookmark  
  10.  83
    A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
    The lambdaPi-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the lambdaPi-calculus and prove the cut-elimination theorem. The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting considered (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  11. Logic Programming Via Proof-Valued Computations.David J. Pym & Lincoln A. Wallen - 1992 - LFCS, Department of Computer Science, University of Edinburgh.
     
    Export citation  
     
    Bookmark   1 citation