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.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,880

External links

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

Through your library

Analytics

Added to PP
2023-08-04

Downloads
18 (#1,125,631)

6 months
5 (#1,080,408)

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