Compact representation (left) of an equivalence class of proofs (right)
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:
Subatomic Proof Systems: Splittable Systems
Andrea Aler Tubella and Alessio Guglielmi
This paper presents the first in a series of results that allow us to develop a theory providing finer control over the complexity of normalisation, and in particular of cut elimination. By considering atoms as self-dual non-commutative connectives, we are able to classify a vast class of inference rules in a uniform and very simple way. This allows us to define simple conditions that are easily verifiable and that ensure normalisation and cut elimination by way of a general theorem. In this paper we define and consider splittable systems, which essentially comprise a large class of linear logics, including MLL and BV, and we prove for them a splitting theorem, guaranteeing cut elimination and other admissibility results as corollaries. In papers to follow, we will extend this result to non-linear logics. The final outcome will be a comprehensive theory giving a uniform treatment for most existing logics and providing a blueprint for the design of future proof systems.
Pdf 4 December 2017
ACM Transactions on Computational Logic, 19 (1:5) 2018, pp. 1–33
On the Length of Medial-Switch-Mix Derivations
Paola Bruscoli and Lutz Straßburger
Switch and medial are two inference rules that play a central role in many deep inference proof systems. In specific proof systems, the mix rule may also be present. In this paper we show that the maximal length of a derivation using only the inference rules for switch, medial, and mix, modulo associativity and commutativity of the two binary connectives involved, is quadratic in the size of the formula at the conclusion of the derivation. This shows, at the same time, the termination of the rewrite system.
Pdf 26 June 2017
WoLLIC 2017
Removing Cycles from Proofs
Andrea Aler Tubella, Alessio Guglielmi and Benjamin Ralph
If we track atom occurrences in classical propositional proofs in deep inference, we see that they can form cyclic structures between cuts and identity steps. These cycles are an obstacle to a very natural form of normalisation, that simply unfolds all the contractions in a proof. This mechanism, which we call 'decomposition', has many points of contact with explicit substitutions in lambda calculi. In the presence of cycles, decomposition does not terminate, and this is an obvious drawback if we want to interpret proofs computationally. One way of eliminating cycles is eliminating cuts. However, we could ask ourselves whether it is possible to eliminate cycles independently of (general) cut elimination. This paper shows an efficient way to do so, therefore establishing the independence of decomposition from cut elimination. In other words, cut elimination in propositional logic can be separated into three separate procedures: 1) cycle elimination, 2) unfolding of contractions, 3) elimination of cuts in the linear fragment.
Pdf 20 June 2017
CSL 2017
On Analyticity in Deep Inference
Paola Bruscoli and Alessio Guglielmi
In this note, we discuss the notion of analyticity in deep inference and propose a formal definition for it. The idea is to obtain a notion that would guarantee the same properties that analyticity in Gentzen theory guarantees, in particular, some reasonable starting point for algorithmic proof search. Given that deep inference generalises Gentzen proof theory, the notion of analyticity discussed here could be useful in general, and we offer some reasons why this might be the case.
Pdf 13 November 2016
Dale Fest
Conflict Nets: Locally Canonical P-time Proof Nets for MALL
Dominic Hughes and Willem Heijltjes
We give a new notion of proof net for Multiplicative-Additive Linear Logic, that strikes a subtle balance between efficiency and canonicity. Conflict nets are canonical for all local rule commutations, which are those that do not incur a global duplication. As a consequence they have linear size compared to sequent proofs, avoiding the exponential growth of Hughes and Van Glabbeek's Slice Nets.
Pdf 17 June 2016
LICS 2016
Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot
Jeřá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
We 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.
Pdf 25 July 2015
LICS 2015
Confluent and Natural Cut Elimination in Classical Logic
Alessio Guglielmi and Benjamin Ralph
We 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 pdf 31 March 2015
Proof, Computation, Complexity 2015
Subatomic Proof Systems
Andrea Aler Tubella and Alessio Guglielmi
We 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
Pdf 30 November 2014
All About Proofs, Proofs for All
22–23.4.13 Bruscoli talks about A Quasipolynomial Normalisation Procedure in Deep Inference at the Proof, Computation, Complexity 2013 International Workshop in Toulouse, France.
28.4–3.5.13 Guglielmi visits Tom Gundersen and Michel Parigot at PPS.
29–30.5.13 McCusker attends the SamsonFest conference at University of Oxford.
18–19.7.13 Duchesne and McCusker attend the Games for Logic and Programming (GALOP) workshop at Queen Mary, University of London.
27–31.8.2013 Duchesne attends the International Summer School on Linear Logic and Geometry of Interaction in Turin.
9–11.09.2013 Duchesne attends the Scientific Meeting in Honour of Pierre-Louis Curien in Venice.
16.9.13 Guglielmi 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.13 Guglielmi 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.2013 Aler Tubella attends the Mathematics Research Beyond the Blackboard LMS Computer Science Colloquium in London.
5–7.11.13 Duchesne 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.13 Guglielmi visits Tom Gundersen and Michel Parigot at PPS.
17–24.11.13 Beniamino Accattoli (Università di Bologna) visits us and talks about A Fresh Look at Linear Head Reduction.
21–22.11.13 Norbert Preining (Japan Advanced Institute of Science and Technology) visits us and talks about Gödel Logics – A Short Survey.
27.11.13 Alexis Goyet (PPS, Paris) visits us and talks about A Dual Calculus for Unconstrained Strategies.
5–6.12.13 Stéphane Gimenez (Innsbruck) visits us and talks about The Structure of Interaction.
2–4.12.2013 Duchesne participates in the Bounded Linear Logic Workshop in Fontainebleau.
13–17.1.2014 Duchesne attends the first workshop of Mathematical Structures of Computation in Lyon, on Recent Developments in Type Theory.
25–26.5.14 Guglielmi visits Michel Parigot at PPS.
7–11.7.14 Dominic Hughes (Stanford) visits us and talks about Graphical Proofs.
18-20.7.14 Guglielmi 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.14 Bruscoli visits Luca Paolini and Luca Roversi at Università di Torino.
10–12.9.14 Anupam Das (LIX, Paris) visits us and talks about Some Developments on the Linear Fragment of Propositional Logic.
29.9.14 Guglielmi 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.14 Kai Brünnler visits us.
28.10.14 Ross Duncan (Strathclyde) visits us and talks about Quantum Computation in (Almost) Any Category.
2.12.14 Emmanuel Beffara (Université d'Aix-Marseille) visits us and talks about Proofs as Schedules.
15–18.12.14 Anupam Das (MILYON, Lyon) visits us and talks about On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems.
11–12.5.15 Georg Struth (Sheffield) visits us and talks about Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages.
23–24.5.15 Aler Tubella participates in the Proof, Computation, Complexity 2015 workshop and speaks about Subatomic Proof Systems.
23–24.5.15 Ralph participates in the Proof, Computation, Complexity 2015 workshop and speaks about Confluent and Natural Cut Elimination in Classical Logic.
1–5.6.15 Anupam 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.15 Bruscoli and Guglielmi teach two courses at ESSLLI 2015: Introduction to Deep Inference and Normalisation and Deep Inference.
6–13.9.15 Tom Gundersen (Red Hat) visits us.
7–11.9.15 Dominic Hughes (Stanford) visits us and talks about First-Order Proofs Without Syntax.
14–17.10.15 Ugo Dal Lago (Bologna) visits us.
14–16.12.15 We host the workshop Efficient and Natural Proof Systems.
13–20.12.15 Tom Gundersen (Red Hat) and Michel Parigot (PPS, Paris) visit us.
11.3.16 Guglielmi visits the University of Oxford and talks about A Proposal for a New Foundation for Proof Theory.
7–9.4.16 Aler 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.16 Jamie Vicary (Oxford) visits us and talks about Geometrical Proofs for Linear Logic.
26.4.16 Pino Rosolini (Genova) visits us and talks about Frames from Topology, Algebraically.
5–6.5.16 Aler 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.16 Aler Tubella, Guglielmi and Ralph visit PPS (Paris) and collaborate with Michel Parigot.
9.5.16 Aler 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.
11.11.2022 Alessio Guglielmi email
