Compact representation (left) of an equivalence class of proofs (right)
We are all familiar with the language of classical logic, which is normally used for both mathematical and informal arguments, but there are other important and useful logics. Some nonclassical logics, for example, can be associated with programming languages to help control the behaviour of their programs, for instance via type systems.
In order to define the proofs of a logic we need a proof system consisting of a formal language and some inference rules. We normally design proof systems following the prescriptions of some known formalism that ensures that we obtain desirable mathematical properties. In any case, we must make sure that proofs can be checked for validity with a computational effort that does not exceed certain limits. In other words, we want checking correctness to be relatively easy, also because this property facilitates the design of algorithms for the automatic discovery of proofs.
However, there is a tension between the ease by which proofs can be checked and their size. If a proof is too small, checking it is difficult. Conversely, formalisms that make it very easy to check and to search for proofs create big bureaucratic unnatural proofs. All traditional proof systems suffer to various extents from this problem, because of the rigidity of all traditional formalisms, which impose an excess of structure on proof systems.
We intend to design a formalism, provisionally called Formalism B, in which arbitrary logics can be defined and their proofs described in a way that is at the same time efficient and natural. Formalism B will ideally lie at the boundary between the class of proof systems and that of systems containing proto-proofs that are small and natural, but are too difficult to check. In other words, we want to maximise naturality by retaining as much efficiency as possible in proof representation. A driving force in this effort will be the use of existing algebraic theories that seem to capture some of the structure needed by the new formalism.
There are two main reasons for doing this. One is theoretical: the problem is compelling, and tackling it fits well into a research effort in the theory of computation that tries to define proofs as more abstract mathematical objects than just intricate pieces of syntax. Suffice to say that we are at present unable to decide by an algorithm when two seemingly different proofs of the same statement use the same ideas and so are equivalent, or not. This is a problem that dates back to Hilbert and that requires more abstract ways to describe proofs than traditional syntax provides.
The second reason is practical: we need formal proofs to verify the correctness of complex computer systems. The more powerful computer systems become, the more we need to ensure that they do what they are supposed to do. Formal verification is increasingly adopted as a viable instrument for this, but still much needs to be done in order to make it an everyday tool. We need to invent proof systems that simplify the interaction with proof assistants, and that could represent in some canonical way proofs that are essentially the same, so that no duplication occurs in the search for and storing of proofs in proof libraries.
This project intends to contribute by exploiting proof-theoretic advances of the past ten years. We have developed a new design method for proof systems that reduces the size of inference steps to their minimal terms, in a theory called 'deep inference'. The finer scale of rules allows us to associate proofs with certain purely geometric objects that faithfully abstract away proof structure, and that are natural guides for the design of proof systems whose proofs would not suffer from several forms of bureaucracy.
In short, after a decade in which we broke proofs into their smallest pieces, by retaining their properties, we are now reshaping them in such a way that they still retain all the features we need but do not keep the undesirable ones.
Value of this project: 756,061 GBP (full economic costing, including indexation and one research studentship funded by the University of Bath) plus two research studentships added after the project started.
On the project:
In the Mathematical Foundations group:
Collaborating groups:
Conflict nets: Locally canonical P-time proof nets for MALL
Dominic Hughes and Willem Heijltjes
AbstractWill be available shortly.
LICS 2016
Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot
AbstractJeřábek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between that system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek's result: we give a quasipolynomial-time cut-elimination procedure for classical propositional logic in deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they only trace structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.
Complexity Bounds for Sum-Product Logic Via Additive Proof Nets and Petri Nets
Willem Heijltjes and Dominic Hughes
AbstractWe investigate efficient algorithms for the additive fragment of linear logic. This logic is an internal language for categories with finite sums and products, and describes concurrent two-player games of finite choice. In the context of session types, typing disciplines for communication along channels, the logic describes the communication of finite choice along a single channel. We give a simple linear time correctness criterion for unit-free propositional additive proof nets via a natural construction on Petri nets. This is an essential ingredient to linear time complexity of the second author’s combinatorial proofs for classical logic. For full propositional additive linear logic, including the units, we give a proof search algorithm that is linear-time in the product of the source and target formula, and an algorithm for proof net correctness that is of the same time complexity. We prove that proof search in first-order additive linear logic is NP-complete.
Pdf25 July 2015
LICS 2015
Confluent and Natural Cut Elimination in Classical Logic
Alessio Guglielmi and Benjamin Ralph
AbstractWe show that, in deep inference, there is a natural and confluent cut elimination procedure that has a strikingly simple semantic justification. We proceed in two phases: we first tackle the propositional case with a construction that we call the 'experiments method'. Here we build a proof made of as many derivations as there are models of the given tautology. Then we lift the experiment method to the predicate calculus, by tracing all the existential witnesses, and in so doing we reconstruct the Herbrand theorem. The confluence of the procedure is essentially taken care of by the commutativity and associativity of disjunction.
Abstract pdf31 March 2015
Proof, Computation, Complexity 2015
Subatomic Proof Systems
Andrea Aler Tubella and Alessio Guglielmi
AbstractWe show a proof system that generates propositional proofs by employing a single, linear, simple and regular inference rule scheme. The main idea is to consider atoms as self-dual, noncommutative binary logical relations and build formulae by freely composing units by atoms, disjunction and conjunction. If we restrict proofs to formulae where no atom occurs in the scope of another atom, we fully and faithfully recover a deduction system for propositional logics in the usual sense, where traditional proof analysis and transformation techniques such as cut elimination can be studied.
Deep Inference
Alessio Guglielmi
Pdf30 November 2014
All About Proofs, Proofs for All, College Publications, pp. 164–172, 2015
22–23.4.13Bruscoli talks about A Quasipolynomial Normalisation Procedure in Deep Inference at the Proof, Computation, Complexity 2013 International Workshop in Toulouse, France.
28.4–3.5.13Guglielmi visits Tom Gundersen and Michel Parigot at PPS.
29–30.5.13McCusker attends the SamsonFest conference at University of Oxford.
18–19.7.13Duchesne and McCusker attend the Games for Logic and Programming (GALOP) workshop at Queen Mary, University of London.
27–31.8.2013Duchesne attends the International Summer School on Linear Logic and Geometry of Interaction in Turin.
9–11.09.2013Duchesne attends the Scientific Meeting in Honour of Pierre-Louis Curien in Venice.
16.9.13Guglielmi participates in the Third Workshop of the Amadeus Project on Proof Compression at INRIA Nancy-Grand Est and talks about Geometric Ideas in the Design of Efficient and Natural Proof Systems.
23–27.9.13Guglielmi participates in the Tenth International Tbilisi Symposium on Language, Logic and Computation and talks as an invited speaker in the Workshop on Algebraic Proof Theory with the talk Geometric Ideas in the Design of Efficient and Natural Proof Systems.
29.10.2013Aler Tubella attends the Mathematics Research Beyond the Blackboard LMS Computer Science Colloquium in London.
5–7.11.13Duchesne and Guglielmi participate in the Theory and Application of Formal Proofs LIX Colloquium 2013 at École Polytechnique; Guglielmi talks as an invited speaker about Proof Composition Mechanisms and Their Geometric Interpretation.
8–13.11.13Guglielmi visits Tom Gundersen and Michel Parigot at PPS.
17–24.11.13Beniamino Accattoli (Università di Bologna) visits us and talks about A Fresh Look at Linear Head Reduction.
21–22.11.13Norbert Preining (Japan Advanced Institute of Science and Technology) visits us and talks about Gödel Logics – A Short Survey.
27.11.13Alexis Goyet (PPS, Paris) visits us and talks about A Dual Calculus for Unconstrained Strategies.
5–6.12.13Stéphane Gimenez (Innsbruck) visits us and talks about The Structure of Interaction.
2–4.12.2013Duchesne participates in the Bounded Linear Logic Workshop in Fontainebleau.
13–17.1.2014Duchesne attends the first workshop of Mathematical Structures of Computation in Lyon, on Recent Developments in Type Theory.
25–26.5.14Guglielmi visits Michel Parigot at PPS.
7–11.7.14Dominic Hughes (Stanford) visits us and talks about Graphical Proofs.
18-20.7.14Guglielmi is an invited speaker in the All about Proofs, Proofs for All workshop with the contribution Deep Inference; then he participates in the Nonclassical Proofs: Theory, Applications and Tools workshop with the talk Introducing Substitution in Proof Theory; both events are in the framework of the Vienna Summer of Logic.
29.7–2.8.14Bruscoli visits Luca Paolini and Luca Roversi at Università di Torino.
10–12.9.14Anupam Das (LIX, Paris) visits us and talks about Some Developments on the Linear Fragment of Propositional Logic.
29.9.14Guglielmi participates as an invited speaker in the ISRALOG'14 Israeli Workshop on Non-Classical Logics and Their Applications with the tutorial Introduction to Deep Inference.
20-21.10.14Kai Brünnler visits us.
28.10.14Ross Duncan (Strathclyde) visits us and talks about Quantum Computation in (Almost) Any Category.
2.12.14Emmanuel Beffara (Université d'Aix-Marseille) visits us and talks about Proofs as Schedules.
15–18.12.14Anupam Das (MILYON, Lyon) visits us and talks about On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems.
11–12.5.15Georg Struth (Sheffield) visits us and talks about Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages.
23–24.5.15Aler Tubella participates in the Proof, Computation, Complexity 2015 workshop and speaks about Subatomic Proof Systems.
23–24.5.15Ralph participates in the Proof, Computation, Complexity 2015 workshop and speaks about Confluent and Natural Cut Elimination in Classical Logic.
1–5.6.15Anupam Das (MILYON, Lyon) visits us and talks about A Complete Axiomatisation of MSOL on Infinite Trees and No Complete Linear Rewriting System for Boolean Algebras.
3–14.8.15Bruscoli and Guglielmi teach two courses at ESSLLI 2015: Introduction to Deep Inference and Normalisation and Deep Inference.
6–13.9.15Tom Gundersen (Red Hat) visits us.
7–11.9.15Dominic Hughes (Stanford) visits us and talks about First-Order Proofs Without Syntax.
14–17.10.15Ugo Dal Lago (Bologna) visits us.
14–16.12.15We host the workshop Efficient and Natural Proof Systems.
13–20.12.15Tom Gundersen (Red Hat) and Michel Parigot (PPS, Paris) visit us.
11.3.16Guglielmi visits the University of Oxford and talks about A Proposal for a New Foundation for Proof Theory.
7–9.4.16Aler Tubella, Guglielmi (as an invited speaker) and Ralph participate in the Algebra and Coalgebra meet Proof Theory 2016 workshop and speak about, respectively: Subatomic proof systems, Designing a proof system around a normalisation procedure and Understanding first-order cut elimination and Herbrand’s theorem using deep inference.
20.4.16Jamie Vicary (Oxford) visits us and talks about Geometrical Proofs for Linear Logic.
26.4.16Pino Rosolini (Genova) visits us and talks about Frames from Topology, Algebraically.
5–6.5.16Aler Tubella, Guglielmi and Ralph participate in the Proof, Computation, Complexity 2016 workshop and speak about, respectively: Generalising Cut-Elimination Through Subatomic Proof Systems, Report on a 3-Year Project on Efficient and Natural Proof Systems and Decomposing First-Order Proofs Using Deep Inference.
7–11.5.16Aler Tubella, Guglielmi and Ralph visit PPS (Paris) and collaborate with Michel Parigot.
9.5.16Aler Tubella, Guglielmi and Ralph visit LIX (Paris), together with Michel Parigot, and discuss research with the team Parsifal and Anupam Das (MILYON, Lyon); Aler Tubella and Ralph speak about, respectively: Understanding Cut-Elimination Through Subatomic Logic and Decomposing First-Order Proofs Using Deep Inference.
14.5.2016Alessio Guglielmiemail