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.

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.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as JSONCSVXML

Archive Staff Only

View Item