A coalgebraic framework for reductive logic and proof-search (ReLiC)
Lead Research Organisation:
University College London
Department Name: Computer Science
Abstract
While the traditional, deductive approach to logic begins with premisses and in step-by-step fashion applies proof rules to derive conclusions, the complementary reductive approach instead begins with a putative conclusion and searches for premisses sufficient for a legitimate derivation to exist by systematically reducing the space of possible proofs.
Not only does this picture more closely resemble the way in which mathematicians actually prove theorems and, more generally, the way in which people solve problems using formal representations, it also encapsulates diverse applications of logic in computer science such as the programming paradigm known as logic programming, the proof-search problem at the heart of AI and automated theorem proving, precondition generation in program verification and more. It is also reflected at the level of truth-functional semantics --- the perspective on logic utilized for the purpose of model checking and thus verifying the correctness of industrial systems --- wherein the truth value of a formula is calculated according to the truth values of its constituent parts.
Despite the reductive viewpoint reflecting logic as it is actually used, and in stark contrast to deductive logic, a uniform mathematical foundation for reductive logic does not exist. Substantial background is provided by the work of Pym, Ritter, and Wallen, but this is essentially restricted to classical and intuitionistic logic and, even then, lacks an explicit theory of the computational processes involved. We believe coalgebra --- a unifying mathematical framework for computation, state-based systems and decomposition, for which Silva is a leading contributor and exponent --- can be applied to this end. Deduction is essentially captured by inductive constructions, but reduction is captured through the coalgebraic technique of coinduction, which decomposes goals down into subgoals.
Existing work shows that coalgebra generalizes truth-functional semantics and can represent basic aspects of search spaces. We will systematize this work to logics in full generality and, by utilizing the coalgebraic approach to the modelling of computation, also capture the control procedures required for proof-search. The algebraic properties of coalgebra should ensure that all aspects of this modelling, including the definitions of logics, their search spaces, and their search procedures, will be compositional.
Beyond this advance on the state of the art in semantic approaches to proof-search,
we can hope to utilize coalgebraic presentations of computation to achieve much more. By interfacing coalgebraic models of proof-search with coalgebraic models of, for example, probabalistic computation or programming languages, we can hope to give a clean, generic and modular presentation of applications of the reductive logic viewpoint as diverse as inductive logic programming and abduction-based Separation Logic tools such as Facebook's Infer.
Abstracting the key features of such systems into a modular semantic framework can help with more than simply understanding how existing tools work and can be improved. Such a framework can also guide the design and implementation of new tools. Thus, in tandem with our theoretical development, we will develop efficient, semantically driven automated reasoning support with wide application. In doing so we can thus hope to implement tools capable of deployment for a large range of reasoning problems and guide the design of theorem provers for specific logics.
Not only does this picture more closely resemble the way in which mathematicians actually prove theorems and, more generally, the way in which people solve problems using formal representations, it also encapsulates diverse applications of logic in computer science such as the programming paradigm known as logic programming, the proof-search problem at the heart of AI and automated theorem proving, precondition generation in program verification and more. It is also reflected at the level of truth-functional semantics --- the perspective on logic utilized for the purpose of model checking and thus verifying the correctness of industrial systems --- wherein the truth value of a formula is calculated according to the truth values of its constituent parts.
Despite the reductive viewpoint reflecting logic as it is actually used, and in stark contrast to deductive logic, a uniform mathematical foundation for reductive logic does not exist. Substantial background is provided by the work of Pym, Ritter, and Wallen, but this is essentially restricted to classical and intuitionistic logic and, even then, lacks an explicit theory of the computational processes involved. We believe coalgebra --- a unifying mathematical framework for computation, state-based systems and decomposition, for which Silva is a leading contributor and exponent --- can be applied to this end. Deduction is essentially captured by inductive constructions, but reduction is captured through the coalgebraic technique of coinduction, which decomposes goals down into subgoals.
Existing work shows that coalgebra generalizes truth-functional semantics and can represent basic aspects of search spaces. We will systematize this work to logics in full generality and, by utilizing the coalgebraic approach to the modelling of computation, also capture the control procedures required for proof-search. The algebraic properties of coalgebra should ensure that all aspects of this modelling, including the definitions of logics, their search spaces, and their search procedures, will be compositional.
Beyond this advance on the state of the art in semantic approaches to proof-search,
we can hope to utilize coalgebraic presentations of computation to achieve much more. By interfacing coalgebraic models of proof-search with coalgebraic models of, for example, probabalistic computation or programming languages, we can hope to give a clean, generic and modular presentation of applications of the reductive logic viewpoint as diverse as inductive logic programming and abduction-based Separation Logic tools such as Facebook's Infer.
Abstracting the key features of such systems into a modular semantic framework can help with more than simply understanding how existing tools work and can be improved. Such a framework can also guide the design and implementation of new tools. Thus, in tandem with our theoretical development, we will develop efficient, semantically driven automated reasoning support with wide application. In doing so we can thus hope to implement tools capable of deployment for a large range of reasoning problems and guide the design of theorem provers for specific logics.
Planned Impact
The impact of this project will be primarily academic, thus we expand further on the communities highlighted in Academic Beneficieries. Correspondingly, we identify five specific kinds of academic impact.
1. In formal or mathematical logic. The establishment of the reductive view of logic --- which corresponds to much of the use of logic as a practical reasoning tool --- as a first-class component in the landscape of logical theory, with the first-steps in a comparable meta-theory.
2. In philosophical logic. Authors such as Martin-Lof, Prawitz, Sundholm, Negri and, latterly, Negri and Van Plato, have considered the proof-theoretic basis for the meanings of logical connectives and the justifications of the logical laws (rules). The essential point is that natural deduction rules and systems of rules, subject to certain design principles, have sufficient inductive structure to define fully the meanings
of operators (connectives, modalities, quantifiers) and proofs.
The shift to a conceptually rigorous view of reductive logic raises the question, for instance, of what is the impact of concepts such as indeterminacy and control on the meaning of the operators; for example, the input-output model of resource distribution renders multiplicative conjunction as being, to some extent at least, essentially non-commutative.
3. In coalgebraic theory. While we expect to be users rather than developers of coalgebraic theory, we can expect that out work will broaden and deepen the general understanding of the applicability of coalgebraic methods in logic, push the theory well beyond its starting point in Kripke semantics and transition systems for process and action logics.
4. In program logic and verification. Our work will provide a basis for a conceptual systematization of the now-large space of separation logics
which lacks a coherent foundation. As a consequence, we can expect to provide a basis for a uniform framework for designing tools (such as verifiers, analysers, and model checkers) for these program logics.
5. In models of computation. The canon of work in programming language semantics, in particular in the denotational tradition/approach for imperative and functional languages, couches much of its theory these days in terms of monads/comonads. Our coalgebraic approach to models of computation based on reductive logic --- and on proof-search in particular --- will connect their semantics to the traditional approach.
In order to promote this work to these communities we plan to host a major program semantics/coalgebra conference and/or workshop at our institute during the period of the grant (for example MFPS-CALCO). We also plan a textbook building on the work in the research monograph "Reductive Logic and Proof-Search: Proof Theory, Semantics and Control" by the PI Pym and Ritter but instead pitched at a postgraduate audience and advocating the new coalgebraic approach. We plan also three technical workshops over the life of the project.
We also believe the research we carry out can have industrial impact, including in the design of verification tools in industry: for example, extracting design principles from Facebook's Infer to implement similar tools for concurrent separation logic.
1. In formal or mathematical logic. The establishment of the reductive view of logic --- which corresponds to much of the use of logic as a practical reasoning tool --- as a first-class component in the landscape of logical theory, with the first-steps in a comparable meta-theory.
2. In philosophical logic. Authors such as Martin-Lof, Prawitz, Sundholm, Negri and, latterly, Negri and Van Plato, have considered the proof-theoretic basis for the meanings of logical connectives and the justifications of the logical laws (rules). The essential point is that natural deduction rules and systems of rules, subject to certain design principles, have sufficient inductive structure to define fully the meanings
of operators (connectives, modalities, quantifiers) and proofs.
The shift to a conceptually rigorous view of reductive logic raises the question, for instance, of what is the impact of concepts such as indeterminacy and control on the meaning of the operators; for example, the input-output model of resource distribution renders multiplicative conjunction as being, to some extent at least, essentially non-commutative.
3. In coalgebraic theory. While we expect to be users rather than developers of coalgebraic theory, we can expect that out work will broaden and deepen the general understanding of the applicability of coalgebraic methods in logic, push the theory well beyond its starting point in Kripke semantics and transition systems for process and action logics.
4. In program logic and verification. Our work will provide a basis for a conceptual systematization of the now-large space of separation logics
which lacks a coherent foundation. As a consequence, we can expect to provide a basis for a uniform framework for designing tools (such as verifiers, analysers, and model checkers) for these program logics.
5. In models of computation. The canon of work in programming language semantics, in particular in the denotational tradition/approach for imperative and functional languages, couches much of its theory these days in terms of monads/comonads. Our coalgebraic approach to models of computation based on reductive logic --- and on proof-search in particular --- will connect their semantics to the traditional approach.
In order to promote this work to these communities we plan to host a major program semantics/coalgebra conference and/or workshop at our institute during the period of the grant (for example MFPS-CALCO). We also plan a textbook building on the work in the research monograph "Reductive Logic and Proof-Search: Proof Theory, Semantics and Control" by the PI Pym and Ritter but instead pitched at a postgraduate audience and advocating the new coalgebraic approach. We plan also three technical workshops over the life of the project.
We also believe the research we carry out can have industrial impact, including in the design of verification tools in industry: for example, extracting design principles from Facebook's Infer to implement similar tools for concurrent separation logic.
Publications
Allen A
(2022)
Developing a well-received pre-matriculation program: the evolution of MedFIT.
in Discover education
Bao J
(2021)
A Bunched Logic for Conditional Independence
Ciabattoni A
(2023)
Cut-restriction: from cuts to analytic cuts
Ciabattoni A
(2023)
Cut-Restriction: From Cuts to Analytic Cuts
Costa D
(2021)
Non-dual modal operators as a basis for 4-valued accessibility relations in Hybrid logic
in Journal of Logical and Algebraic Methods in Programming
David Pym
(2024)
Categorical Proof-theoretic Semantics
in Studia Logica
Docherty, S
(2019)
Stone-type dualities for separation logics
in Logical Methods in Computer Science
Eckhardt T
(2024)
Base-extension semantics for modal logic
in Logic Journal of the IGPL
Galmiche D
(2019)
A substructural epistemic resource logic: theory and modelling applications
in Journal of Logic and Computation
Gheorghiu A
(2023)
Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic
in Bulletin of the Section of Logic
Gheorghiu A
(2022)
Provability in BI's Sequent Calculus is Decidable 1
Gheorghiu A
(2022)
Generalizing Rules via Algebraic Constraints
Gheorghiu A
(2023)
Semantical Analysis of the Logic of Bunched Implications
in Studia Logica
Gheorghiu A
(2023)
Defining Logical Systems via Algebraic Constraints on Proofs
Gheorghiu A
(2023)
Samson Abramsky on Logic and Structure in Computer Science and Beyond
Gheorghiu A
(2021)
Focused Proof-search in the Logic of Bunched Implications (Accepted)
Gheorghiu A
(2023)
Defining Logical Systems via Algebraic Constraints on Proofs
in Journal of Logic and Computation
Gheorghiu A
(2022)
Semantical Analysis of the Logic of Bunched Implications
Jana Wagemaker
(2020)
31st International Conference on Concurrency Theory (CONCUR 2020)
Kuznets R
(2021)
Justification Logic for Constructive Modal Logic
in Journal of Applied Logics
Description | We have identified an important connection between reductive logic and proof-theoretic semantics. Our insight suggests that an appropriate to think about proof-theoretic semantics --- in which model-theoretic validity is replaced by proof-theoretic validity, based on proof-theoretic structures --- is in terms of the reductive logic. We believe this correspondence extends to proof-search (which is seen as reductive logic + control). One early consequence of this insight is expected to be a proof-theoretic semantics for Milner's conception of tactical proof. A further step will be to integrate these ideas with our coalgebraic approach to the proof theory and semantics of proof-search. We have now established the team derived from the ReLiC project as a centre for proof-theoretic semantics that is not only developing its logical theory quite substantially, but also exploring its role as a foundation for informatics through initial studies of systems and security examples. |
Exploitation Route | We expect that the scope and range of applications of proof-theoretic semantics will significantly enhanced. Connections to the foundations of logic programming are proving to be illuminating. |
Sectors | Other |
Description | Birmingham |
Organisation | University of Birmingham |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Collaborative research and dissemination. |
Collaborator Contribution | Collaborative research and dissemination. |
Impact | Categorical Proof-theoretic Semantics. In press, Studia Logica, 2024. |
Start Year | 2021 |
Description | QMUL |
Organisation | Queen Mary University of London |
Department | Queen Mary Innovation |
Country | United Kingdom |
Sector | Private |
PI Contribution | Pym and Ritter are work with Robinson on a category-theoretic analysis of proof-theoretic semantics. |
Collaborator Contribution | Pym and Ritter are work with Robinson on a category-theoretic analysis of proof-theoretic semantics. |
Impact | Pending. |
Start Year | 2021 |
Description | Tübingen |
Organisation | Eberhard Karls University of Tübingen |
Country | Germany |
Sector | Academic/University |
PI Contribution | Pym has collaborated with Piecha and Schroeder-Heister to submit a grant proposal to the DFG about proof-theoretic semantics and its application to substructural logics and its application to the reductive view of logics. |
Collaborator Contribution | Pym has collaborated with Piecha and Schroeder-Heister to submit a grant proposal to the DFG about proof-theoretic semantics and its application to substructural logics and its application to the reductive view of logics. |
Impact | Pending. |
Start Year | 2019 |
Description | Keynote Lecture by David Pym at SYSMICS 2018, Vienna |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Substructural logics: semantics, proof theory, and applications 26-28 February 2018, Vienna (Austria) Second SYSMICS Workshop Invited Lecture: David Pym Title: Logic as a modelling technology: resource semantics, systems modelling, and security Abstract: The development of BI, the logic of bunched implications, together with its resource semantics, led to the formulation of Separation Logic, which forms the basis of the Infer program analyser deployed in Facebook's code production. However, this rather successful story sits within a broader, quite systematic logical context. I will review the (family of) logics, including process logics, that are supported by resource semantics, explaining their more-or-less uniform meta-theoretic basis and illustrating their uses in a range of modelling applications, including access control, systems security, and workflow simulation. |
Year(s) Of Engagement Activity | 2018 |
URL | https://sysmics.logic.at/invited |
Description | Lecture Course at SYSMICS Summer School, Les Diablerets, 2018 |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Four lectures on logic as a modelling technology. Impact on PhD students. https://www.dropbox.com/sh/jl3wr3vgx68ajvb/AAA_tT9b7tglSm0fTRHJEqNia?dl=0 |
Year(s) Of Engagement Activity | 2018 |
URL | https://mathsites.unibe.ch/sysmics/ |
Description | Marin Gothenburg |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Talk at the Logic Seminar in Gothenburg (virtual) |
Year(s) Of Engagement Activity | 2021 |
Description | Marin Lyon |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Talk at the ChoCoLa Seminar in Lyon (virtual) |
Year(s) Of Engagement Activity | 2021 |
Description | Marin TULIPS |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Talk at the TULIPS Seminar in Utrecht (virtual). |
Year(s) Of Engagement Activity | 2021 |
Description | Marin WoLLiC |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Talk at WoLLiC (virtual) |
Year(s) Of Engagement Activity | 2021 |
URL | https://wollic.org/wollic2021/ |
Description | Marin Worldwide |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Talk at the Online Worldwide Seminar on Logic and Semantics (Young Researcher Track) |
Year(s) Of Engagement Activity | 2021 |
Description | UCL PPLV Seminar on Cyclic Proofs |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | Local |
Primary Audience | Postgraduate students |
Results and Impact | A regular seminar to build knowledge and generate research activity in the area of cyclic proofs, which are an important emerging phenonemon in program verification and which are susceptible to the methods being developed by this project. |
Year(s) Of Engagement Activity | 2019,2020 |
Description | UNESCO World Logic Day 2022 |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | The meaning of proofs: Celebrating the UNESCO World Logic Day 2022 In proof-theoretic semantics, the meaning of the logical constants can be specified by the inference rules that determine their correct use in proofs. This informal meeting aims at discussing the basics about logic, validity, and proof systems. |
Year(s) Of Engagement Activity | 2022 |
URL | https://sites.google.com/view/wdl-ucl2022/home |