-
2Categorical Proof-theoretic SemanticsStudia Logica 1-38. forthcoming.In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic raises some technical and conceptual issues. We relate Sandqvist’s (complete) base-extension semantics of …Read more
-
18Base-extension semantics for modal logicLogic Journal of the IGPL. forthcoming.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…Read more
-
306Base-extension Semantics for Modal LogicLogic Journal of the IGPL. forthcoming.In proof-theoretic semantics, meaning is based on inference. It may be 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 semant…Read more
-
12Reductive Logic and Proof-Search: Proof Theory, Semantics, and ControlOxford University Press UK. 2004.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 scien…Read more
-
The Uniform Proof-Theoretic Foundation of Linear Logic ProgrammingLFCS, Department of Computer Science, University of Edinburgh. 1991.
-
Logic Programming Via Proof-Valued ComputationsLFCS, Department of Computer Science, University of Edinburgh. 1992.
-
On Resolution in Fragments of Classical Linear LogicLFCS, Department of Computer Science, University of Edinburgh. 1992.
-
A Synopsis on the Identification of Linear Logic Programming LanguagesLFCS, Department of Computer Science, University of Edinburgh. 1992.
-
30Reductive logic and proof-search: proof theory, semantics, and controlOxford University Press. 2004.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.
-
11Reductive Logic, Proof-Search, and Coalgebra: A Perspective from Resource SemanticsIn Alessandra Palmigiano & Mehrnoosh Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond, Springer Verlag. pp. 833-875. 2023.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’…Read more
-
17Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional LogicBulletin of the Section of Logic 52 (2): 239-266. 2023.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 collectio…Read more
-
69The logic of bunched implicationsBulletin of Symbolic Logic 5 (2): 215-244. 1999.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.,…Read more
-
18Semantical Analysis of the Logic of Bunched ImplicationsStudia Logica 111 (4): 525-571. 2023.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. Ess…Read more
-
87A note on the proof theory the λII-calculusStudia Logica 54 (2). 1995.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…Read more
-
8Reductive logic and proof-search: proof theory, semantics, and controlOxford University Press. 2004.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 scien…Read more
-
27Why Separation Logic WorksPhilosophy and Technology 32 (3): 483-516. 2019.One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer’s conceptual model of a program’s manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the reasoning task. …Read more
London, England, United Kingdom of Great Britain and Northern Ireland
Areas of Specialization
Science, Logic, and Mathematics |
Areas of Interest
Science, Logic, and Mathematics |