UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

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

Gheorghiu, A; Docherty, S; Pym, D; (2023) Reductive Logic, Proof-search, and Coalgebra: A Perspective from Resource Semantics. In: Parmigiano, A and Sadrzadeh, M, (eds.) Samson Abramsky on Logic and Structure in Computer Science and Beyond. (pp. 833-875). Springer Nature: Cham, Switzerland.

[thumbnail of Reductive logic, Proof-search, and Coalgebra.pdf] Text
Reductive logic, Proof-search, and Coalgebra.pdf - Accepted Version
Access restricted to UCL open access staff until 3 August 2025.

Download (339kB)

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.

Type: Book chapter
Title: Reductive Logic, Proof-search, and Coalgebra: A Perspective from Resource Semantics
ISBN-13: 978-3-031-24116-1
DOI: 10.1007/978-3-031-24117-8_23
Publisher version: https://doi.org/10.1007/978-3-031-24117-8_23
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10128192
Downloads since deposit
3Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item