Reductive Logic, Proof-Search, and Coalgebra: A Perspective from Resource Semantics

In Alessandra Palmigiano & Mehrnoosh Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Verlag. pp. 833-875 (2023)
  Copy   BIBTEX

Abstract

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 use this set-up as a basis for exploring how coalgebraic semantics can, in contrast to the basic denotational semantics, be used to describe the concrete operational choices that are an essential part of proof-search. The overall aim, toward which this paper can be seen as an initial step, is to develop a uniform, generic, mathematical framework for understanding the relationship between the deductive structure of logics and the control structures of the corresponding reductive paradigm.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,347

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Reductive logic and proof-search: proof theory, semantics, and control.David J. Pym - 2004 - New York: Oxford University Press. Edited by Eike Ritter.
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.
Reductive Logic and Proof-Search: Proof Theory, Semantics, and Control.David J. Pym & Eike Ritter - 2004 - Oxford, England: Oxford University Press UK. Edited by Eike Ritter.
Intuitionistic Logic Freed of All Metarules.Giovanna Corsi & Gabriele Tassi - 2007 - Journal of Symbolic Logic 72 (4):1204 - 1218.
Proof-Theoretic Semantics and Inquisitive Logic.Will Stafford - 2021 - Journal of Philosophical Logic 50 (5):1199-1229.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.

Analytics

Added to PP
2023-08-04

Downloads
11 (#1,143,633)

6 months
8 (#371,375)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

David Pym
University College London

References found in this work

No references found.

Add more references