Alessio Guglielmi's Research and Teaching

Electric lamps were not invented by improving candles

Perhaps you were looking for the Deep Inference pages?

1 Overview of Research

I do proof theory from a theoretical computer science perspective. I am mainly interested in deep inference, a new methodology in proof theory that my collaborators and I have introduced.

Theoretical computer science mainly helps proof theory by bringing to it quantitative and semantic ideas, and proof theory mainly helps computer science by supporting the design of programming languages and the verification of software correctness.

The heart of what I do in proof theory is normalisation. This is still a mysterious combinatorial phenomenon, that is intimately connected to fundamental questions about how much we can compress information. Proof-theoretic research takes place in the purest setting where these problems can be defined, and, as such, it is a fundamental study that has and will continue to have far-reaching applications in computer science.

Two problems motivated the development of this research: understanding normalisation and the identity of proofs.

1.1 Normalisation and Proof Complexity

One research objective is to understand normalisation in propositional logics (first order and, at a later time, second order). Deep inference reveals finer and finer structure in the inference rules. With the methods developed for deep inference, we can see that cut elimination is only a special instance of a much broader normalisation phenomenon. Our techniques unveil new properties of derivations, impossible to be observed in the sequent calculus. One of the most interesting discoveries is that deep-inference rules show an unprecedented regularity in the shape of inference rules of very different logics. In what I call 'subatomic proof theory', it seems possible to describe most of the known logics by just one, simple inference rule.

I'm also interested in proof complexity: since deep inference generalises the sequent calculus, proofs in deep inference can only be shorter than in the sequent calculus. Indeed, on some classes of tautologies, like Statman's ones, there is an exponential speed-up of an analytic deep-inference system over all analytic sequent-calculus ones. We started only recently to study the proof complexity of deep inference. Deep inference is a powerful methodology in this respect, on par with Frege-Hilbert systems (but with better properties). We wonder whether deep inference could give good insights into the many open questions in proof complexity.

We are obtaining a broad theory of normalisation and, more in general, of the design of deductive systems, which are based on more basic and simple principles than traditional proof theory offers.

1.2 Identity of Proofs and Deductive Nets

Another research objective is to come up with useful, interesting notions of identity of proofs. It is embarrassing for proof theory that the natural question of 'when are two proofs to be considered identical?' lacks good answers. (This question is tightly connected to the equally non-well-understood problem of deciding when two algorithms are the same.) One reason for our embarrassment is that the notion of normalisation available, viz. cut elimination, is inadequate to decide the question; I believe that the problem is that this is the only (reasonable) normalisation notion available in the sequent calculus and natural deduction. Thanks to its finer granularity, deep inference offers several natural new notions of normalisation, this way improving our ability to study new concepts of identity.

The calculus of structures is now a fully developed deep inference formalism, but I don't believe that it is the natural setting where to study the proof identity problem: there still is too much bureaucracy in it. I believe that deductive nets will be the right place where to work. Proof nets eliminate, in fact, much of the bureaucracy of calculi like the sequent calculus or the calculus of structures. But which proof nets? Linear logic proof nets are certainly inadequate, because of the poor way they deal with 'sharing', and then because they are not deductive, in the sense that they are not a proof system. We need a much more refined notion, suitable also to classical logic.

We observed that deep inference yields some interesting notions towards deductive nets. In fact, deep inference allows us to design deductive systems whose rules are all local, i.e., their computational complexity is constant (this is provably impossible in traditional proof theory). This property lends itself naturally to a geometric understanding of proofs. In other words, we can now see a geometric structure lurking behind the syntax, and we can control this structure thanks to our local inference rules. We are already able to use part of this geometric structure to control normalisation, by what we call atomic flows. I think that in a few years we will be able to exploit the full potential of the geometry behind proofs in order to have a satisfactory, topological answer to the problem of the identity of proofs.

1.3 Summary

Deep inference reveals regularities that traditional formalisms cannot detect, and it offers new proof theoretical properties, of special interest for normalisation. My colleagues and I are exploiting these regularities and properties in a unified theory of several logics. This will yield deductive nets, for which the problem of identity of proofs will be solved in a satisfactory way.

I have three main reasons to work in this area: 1) It is beautiful; this research involves working with beautiful, elegant mathematical objects. 2) It is interesting; it addresses important, challenging problems in proof theory, and they are difficult. 3) It is useful for designing computer science languages; in fact, my research started from questions raised by computer languages for concurrency.

I believe that mathematics is mostly about finding the right definitions, those that affect the way we see things.

The following web page contains more details about my current research: Deep Inference (FAQ, papers, notes, etc.).

2 Politics

This is something I feel strongly about:

Knowledge cannot be measured. As soon as measuring knowledge is attempted, researchers, who are not self-confident enough to resist, try to improve their score (number of papers, h-index, grant money, etc.), and the result is uninspired, incremental research of little value. Unfortunately, most politicians and all managers come from a business culture where everything is thought to be measurable, including knowledge.

Academic freedom is declining. As a result of its success in generating technology and economic power, science is now considered a commodity by governments. They are now predominantly financing research with demonstrable short-term impact on the economy. Therefore, research is now dominated by a class of technology-oriented researchers whose main drive is not curiosity but career progress and commercial exploitation of research. These people are subservient to governments and do not understand and support research with revolutionary potential. Academics have historically been a strong force of change, but they are now sadly becoming another branch of the establishment. What is even sadder is that most younger researchers do not even realise this.

Researchers should resist the business culture because, when applied to science, it is morally wrong and it stifles progress. This paper by Smaldino and McElreath (published by the Royal Society) shows how a culture of poor research methods is created by current incentives, and illustrates all of the above points: The Natural Selection of Bad Science.

• I boycott Elsevier.
• I signed the San Francisco Declaration on Research Assessment.
• I wrote a letter to The Guardian.
• I pledged No free view? No review!
• I signed the Pledge for Sustainable Research in Theoretical Computer Science

I have some more specific opinions on refereeing and conferences here.

3 Recent Papers

• A Subatomic Proof System for Decision Trees
  Chris Barrett and Alessio Guglielmi
  We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is proof-theoretical naturalness: The system consists of all and only the inference rules generated by the single, simple, linear scheme of the recently introduced subatomic logic. Thanks to this regularity, cuts are eliminated via a natural construction. The second reason is that the system generates efficient proofs. Indeed, we show that a certain class of tautologies due to Statman, which cannot have better than exponential cut-free proofs in the sequent calculus, have polynomial cut-free proofs in our system. We achieve this by using the same construction that we use for cut elimination. In summary, by expanding the language of propositional logic, we make its proof theory more regular and generate more proofs, some of which are very efficient.
  That design is made possible by considering atoms as superpositions of their truth values, which are connected by self-dual, non-commutative connectives. A proof can then be projected via each atom into two proofs, one for each truth value, without a need for cuts. Those projections are semantically natural and are at the heart of the constructions in this article. To accommodate self-dual non-commutativity, we compose proofs in deep inference.
  Pdf 30 June 2022
  ACM Transactions on Computational Logic, 23 (4:26) 2022, pp. 1–25
• 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
• 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, LIPIcs 82, pp. 9:1–17
• 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.
  • Journal version pdf 3 May 2016
    Logical Methods in Computer Science 12 (1:5) 2016, pp. 1–30
  • Conference version pdf 25 June 2010
    LPAR-16, LNCS 6355, pp. 136–153
    The title of this version is A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
• Deep Inference
  Alessio Guglielmi
  Pdf 30 November 2014
  All About Proofs, Proofs for All, Mathematical Logic and Foundations, College Publications, pp. 164–172, 2015
• A Logical Basis for Quantum Evolution and Entanglement
  Richard F. Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden and Lutz Straßburger
  We reconsider discrete quantum causal dynamics where quantum systems are viewed as discrete structures, namely directed acyclic graphs. In such a graph, events are considered as vertices and edges depict propagation between events. Evolution is described as happening between a special family of spacelike slices, which were referred to as locative slices. Such slices are not so large as to result in acausal influences, but large enough to capture nonlocal correlations.
  In our logical interpretation, edges are assigned logical formulas in a special logical system, called BV, an instance of a deep inference system. We demonstrate that BV, with its mix of commutative and noncommutative connectives, is precisely the right logic for such analysis. We show that the commutative tensor encodes (possible) entanglement, and the noncommutative seq encodes causal precedence. With this interpretation, the locative slices are precisely the derivable strings of formulas. Several new technical results about BV are developed as part of this analysis.
  Pdf 18 July 2013
  In Categories and Types in Logic, Language, and Physics, LNCS 8222, pp. 90–107
• A System of Interaction and Structure V: The Exponentials and Splitting
  Alessio Guglielmi and Lutz Straßburger
  System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other, recent works, show that system NEL is Turing-complete, it is able to directly express process algebra sequential composition and it faithfully models causal quantum evolution. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. Together with a 'decomposition' theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.
  Pdf 21 September 2010
  Mathematical Structures in Computer Science 21 (3) 2011, pp. 563–584
  This paper is the second part resulted from splitting into two parts the paper A System of Interaction and Structure IV: The Exponentials (which was previously titled A Non-commutative Extension of Multiplicative Exponential Linear Logic and was the journal version of A Non-commutative Extension of MELL).
• A System of Interaction and Structure IV: The Exponentials and Decomposition
  Lutz Straßburger and Alessio Guglielmi
  We study a system, called NEL, which is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials. Equivalently, NEL is MELL augmented with the non-commutative self-dual connective seq. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs.
  Pdf 27 July 2010
  ACM Transactions on Computational Logic 12 (4:23) 2011, pp. 1–39
  This paper is the first part resulted from splitting into two parts the paper A System of Interaction and Structure IV: The Exponentials (which was previously titled A Non-commutative Extension of Multiplicative Exponential Linear Logic and was the journal version of A Non-commutative Extension of MELL).
• Breaking Paths in Atomic Flows for Classical Logic
  Alessio Guglielmi, Tom Gundersen and Lutz Straßburger
  This work belongs to a wider effort aimed at eliminating syntactic bureaucracy from proof systems. In this paper, we present a novel cut elimination procedure for classical propositional logic. It is based on the recently introduced atomic flows: they are purely graphical devices that abstract away from much of the typical bureaucracy of proofs. We make crucial use of the path breaker, an atomic-flow construction that avoids some nasty termination problems, and that can be used in any proof system with sufficient symmetry. This paper contains an original 2-dimensional-diagram exposition of atomic flows, which helps us to connect atomic flows with other known formalisms.
  Pdf 29 April 2010
  LICS 2010 Proceedings (IEEE), pp. 284–293
• A Proof Calculus Which Reduces Syntactic Bureaucracy
  Alessio Guglielmi, Tom Gundersen and Michel Parigot
  In usual proof systems, like sequent calculus, only a very limited way of combining proofs is available through the tree structure. We present in this paper a logic-independent proof calculus, where proofs can be freely composed by connectives, and prove its basic properties. The main advantage of this proof calculus is that it allows to avoid certain types of syntactic bureaucracy inherent to all usual proof systems, in particular sequent calculus. Proofs in this system closely reflect their atomic flow, which traces the behaviour of atoms through structural rules. The general definition is illustrated by the standard deep-inference system for propositional logic, for which there are known rewriting techniques that achieve cut elimination based only on the information in atomic flows.
  Pdf 12 April 2010
  RTA 2010, LIPIcs 6, pp. 135–150
  This paper supersedes the note Formalism A.
• Personal Portrait of Giorgio Levi
  Alessio Guglielmi
  Pdf 23 October 2009
  Theoretical Computer Science 410 (46) 2009, pp. 4605–4607
  2013 update: Giorgio plunged into the fountain.
• On the Proof Complexity of Deep Inference
  Paola Bruscoli and Alessio Guglielmi
  We obtain two results about the proof complexity of deep inference: 1) deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; 2) there are analytic deep-inference proof systems that exhibit an exponential speed-up over analytic Gentzen proof systems that they polynomially simulate.
  Pdf 19 April 2009
  ACM Transactions on Computational Logic 10 (2:14) 2009, pp. 1–34
• Normalisation Control in Deep Inference via Atomic Flows
  Alessio Guglielmi and Tom Gundersen
  We introduce 'atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.
  Pdf 31 March 2008
  Logical Methods in Computer Science 4 (1:9) 2008, pp. 1–36
• A System of Interaction and Structure
  Alessio Guglielmi
  This paper introduces a logical system, called BV, which extends multiplicative linear logic by a non-commutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulae subject to certain equational laws typical of sequents. The calculus of structures is obtained by generalising the sequent calculus in such a way that a new top-down symmetry of derivations is observed, and it employs inference rules that rewrite inside structures at any depth. These properties, in addition to allowing the design of BV, yield a modular proof of cut elimination.
  Pdf 27 January 2007
  ACM Transactions on Computational Logic, Vol. 8 (1:1) 2007, pp. 1–64
  The journal version has been butchered by the editorial process, but the preprint (linked here) is fine.
  At the end of 2012, this was the most cited article appeared in ACM TOCL in the previous five years.
• On Structuring Proof Search for First Order Linear Logic
  Paola Bruscoli and Alessio Guglielmi
  Full first order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the 'proof search as computation'; paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.
  • Conference version pdf 10 September 2003
    LPAR '03, LNCS 2850, pp. 389–406
  • Full paper pdf 22 November 2005
    Theoretical Computer Science 360 (1–3) 2006, pp. 42–76
• A Non-commutative Extension of MELL
  Alessio Guglielmi and Lutz Straßburger
  We extend multiplicative exponential linear logic (MELL) by a non-commutative, self-dual logical operator. The extended system, called NEL, is defined in the formalism of the calculus of structures, which is a generalisation of the sequent calculus and provides a more refined analysis of proofs. We should then be able to extend the range of applications of MELL, by modelling a broad notion of sequentiality and providing new properties of proofs. We show some proof theoretical results: decomposition and cut elimination. The new operator represents a significant challenge: to get our results we use here for the first time some novel techniques, which constitute a uniform and modular approach to cut elimination, contrary to what is possible in the sequent calculus.
  Pdf 9 August 2002
  LPAR 2002, LNCS 2514, pp. 231–246
• A First Order System with Finite Choice of Premises
  Kai Brünnler and Alessio Guglielmi
  We present an inference system for classical first order logic in which each inference rule, including the cut, only has a finite set of premises to choose from. The main conceptual contribution of this paper is the possibility of separating different sources of infinite choice, which happen to be entangled in the traditional cut rule.
  Pdf 1 December 2003
  Presented at First Order Logic 75 under the title A Finitary System for First Order Logic; appeared in Hendricks et al., editor, First-Order Logic Revisited, Logos Verlag, Berlin, 2004, pp. 59–74
• A Tutorial on Proof Theoretic Foundations of Logic Programming
  Paola Bruscoli and Alessio Guglielmi
  Abstract logic programming is about designing logic programming languages via the proof theoretic notion of uniform provability. It allows the design of purely logical, very expressive logic programming languages, endowed with a rich meta theory. This tutorial intends to expose the main ideas of this discipline in the most direct and simple way.
  Pdf 10 September 2003
  Invited tutorial at ICLP '03, LNCS 2916, pp. 109–127
• Non-commutativity and MELL in the Calculus of Structures
  Alessio Guglielmi and Lutz Straßburger
  We introduce the calculus of structures: it is more general than the sequent calculus and it allows for cut elimination and the subformula property. We show a simple extension of multiplicative linear logic, by a self-dual non-commutative operator inspired by CCS, that seems not to be expressible in the sequent calculus. Then we show that multiplicative exponential linear logic benefits from its presentation in the calculus of structures, especially because we can replace the ordinary, global promotion rule by a local version. These formal systems, for which we prove cut elimination, outline a range of techniques and properties that were not previously available. Contrarily to what happens in the sequent calculus, the cut elimination proof is modular.
  Pdf 28 June 2001
  CSL 2001, LNCS 2142, pp. 54–68

4 Notes

• Totally Linear Proofs Victoria Barrett and Alessio Guglielmi We show a proof system for propositional classical logic where all the inference rules are linear and there are no unit equations. There is no creation and no destruction inside derivations at all. 16 May 2021 Presented at 5th International Workshop on Trends in Linear Logic and Applications 2021
• A Subatomic Proof System for Decision Trees Chris Barrett and Alessio Guglielmi Recently, several proof systems have been developed in a very principled and regular way according to a methodology called 'subatomic'. The main idea is to consider atoms as non-commutative self-dual connectives representing a superposition of truth values. This way, non-linear inference rules, such as contraction and cut, become linear and obey a unique scheme. Normalisation is, therefore, at the same time, simplified and generalised. The contribution of this paper is that, surprisingly, by completing in the most natural way the standard subatomic proof system for propositional classical logic, we obtain a new proof system for a conservative extension of propositional classical logic and of decision trees. Cut elimination for this system becomes an almost trivial variation of the already known (and also trivial) 'experiment method', which is essentially a truth tabling operation that generates canonical analytic proofs. 7 June 2019 Presented at Structures and Deduction '19
• 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. 13 November 2016
• 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. 31 March 2015 Presented at 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. 30 March 2015 Presented at Proof, Computation, Complexity 2015, then at Women in Logic 2017 (Pdf) and then at SYSMICS-W2 2018 (Pdf)
• A Subatomic Proof System Andrea Aler Tubella and Alessio Guglielmi In this work we show a proof system, called SA, 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 logic in the usual sense, where traditional proof analysis and transformation techniques such as cut elimination can be studied. 5 July 2014
• The Commutative/Noncommutative Linear Logic BV Alessio Guglielmi This brief survey contains an informal presentation of the commutative/noncommutative linear logic BV in terms of a naif space-temporal model. BV improves on the ability of linear logic to model spatial structure by satisfactorily capturing temporal structure in programming languages and quantum physics. I provide a guide to the literature on BV and suggest that the only satisfactory treatment for it can be obtained in the proof-theoretic methodology of deep inference. 8 May 2014
• Polynomial Size Deep-Inference Proofs Instead of Exponential Size Shallow-Inference Proofs Alessio Guglielmi By a simple example, I show how deep inference can provide for an exponential speed-up in the size of proofs with respect to shallow inference. 22 September 2007 Slides Superseded by On the Proof Complexity of Deep Inference
• Finitary Cut Alessio Guglielmi We all know that the traditional cut rule is considered infinitary. But if we reduce the cut rule to atomic form, as we always can do in the calculus of structures, is atomic cut still infinitary? Not really. 22 September 2007 Superseded by A First Order System with Finite Choice of Premises
• On Analytic Inference Rules in the Calculus of Structures Paola Bruscoli and Alessio Guglielmi We discuss the notion of analytic inference rule for propositional logics in the calculus of structures. 25 November 2009 Superseded by On Analyticity in Deep Inference
• Butterflies Alessio Guglielmi If you're interested in NEL and BV, try to find the mistake in this note. 29 July 2005
• Some News on Subatomic Logic Alessio Guglielmi I found a simple explanation for the soundness of the subatomic inference rule. 28 July 2005 Superseded by A Study of Normalisation Through Subatomic Logic
• Red and Blue Alessio Guglielmi The sequent calculus is often colour blind, but not always; the calculus of structures has a consistent behaviour. 26 July 2005
• The Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep Inference Alessio Guglielmi Some discussion and then the first attempt at wired/weird deduction. 17 June 2005 Proceedings of Structures and Deduction '05, pp. 53–68
• Formalism B Alessio Guglielmi Inference rules operate on derivations. 20 December 2004
• Formalism A Alessio Guglielmi I generalise the notion of derivation for taking care of a certain kind of bureaucracy. 23 April 2004 Superseded by A Proof Calculus Which Reduces Syntactic Bureaucracy
• Resolution in the Calculus of Structures Alessio Guglielmi It is possible to search for cut-free proofs by the resolution strategy in the calculus of structures; the sequent calculus does not allow the same freedom. 29 September 2003
• Mismatch Alessio Guglielmi There is a mismatch between meta and object levels in many calculi, like the sequent calculus and natural deduction. The mismatch has undesirable proof theoretical consequences, the most important being the inability to design deductive systems. 24 August 2003 Brief note for the specialist, posted to the Foundations of Mathematics and Proof Theory lists
• Normalisation Without Cut Elimination Alessio Guglielmi I propose a possible notion of equivalence for proofs in classical logic, sort of a normal form for case analysis. 25 February 2003
• Subatomic Logic Alessio Guglielmi One can unify classical and linear logic by using only two simple, linear, 'hyper' inference rules; they generate nice systems for all the fragments, where all rules are local. The various logics are determined by the algebra of their units, for example boolean algebra determines classical logic. We can prove cut elimination easily and once and for all in the two-rule system, and the procedure scales down to all the derived fragments. 21 November 2002 Superseded by A Study of Normalisation Through Subatomic Logic
• On Lafont's Counterexample Alessio Guglielmi Lafont's counterexample shows why cut elimination in the sequent calculus of classical logic is not confluent. I show here that the counterexample doesn't work in the calculus of structures. 1 November 2002
• Recipe Alessio Guglielmi A family of tautologies that hold in most logics can be used, following a simple recipe, to produce deductive systems where all rules are local, including cut. 27 October 2002
• Goodness, Perfection and Miracles Alessio Guglielmi I argue about three properties closely related to cut elimination and interpolation theorems.  18 October 2002

5 Recent Talks

• Substitutions and U-Turns StrIP Kick-Off Workshop (Birmingham) 9 June 2022
• Totally Linear Proofs for Classical Logics Proof Society 15 December 2021
• Concerto pour une Voix Seventh TICAMORE Meeting (Vienna) 17 June 2021
• Subatomic Proof Systems and Decision Trees Online Worldwide Seminar on Logic and Semantics 5 May 2021
• Towards Substitution Via Linearity and Projection University of Bath 23 March 2021
• Towards a New Proof Theory of Quantification EECS Theory Seminar, Queen Mary, London 16 July 2020
• Roy Dyckhoff Was a Rare Nonconformist Journeys in Computational Logic: Tributes to Roy Dyckhoff, London 3 September 2019
• Two Design Questions PCC 2019, Djursholm 17 July 2019
• Proposal for a New Approach to Quantification Second FISP Meeting, Paris 10 June 2017
• What Is Wrong with Analyticity in Gentzen's Proof Theory and How to Fix It Proof Meets Truth – Bath-Bristol Workshop on Foundations of Mathematics and Computer Science, Bath 12 May 2017
• Decoupling Normalisation Mechanisms with an Eye Towards Concurrency Università di Torino 14 February 2017 École Normale Supérieure de Lyon 18 April 2017 Inria Saclay 21 April 2017
• On Analyticity in Deep Inference Dale Fest! 60th, Paris 15 December 2016
• Making Several Computation/Normalisation Mechanisms Coexist FISP Kick-off 2016, Innsbruck 16 November 2016
• Designing a Proof System Around a Normalisation Procedure ALCOP 2016, Wien and (with additions) PCC 2016, München 6 May 2016
• A Proposal for a New Foundation for Proof Theory University of Oxford 11 March 2016
• The Quest for Better Languages Talk for the UCAS days (prospective undergraduate students) 25 November 2015
• A Subatomic Proof System Israeli Workshop on Non-Classical Logics and Their Applications, Haifa 29 September 2014
• Introduction to Deep Inference Israeli Workshop on Non-Classical Logics and Their Applications, Haifa 29 September 2014
• Introducing Substitution in Proof Theory Nonclassical Proofs: Theory, Applications and Tools, Vienna Summer of Logic 20 July 2014
• Proof Composition Mechanisms and their Geometric Interpretation Theory and Application of Formal Proofs, LIX Colloquium 2013 (École Polytechnique) 5 November 2013
• Geometric Ideas in the Design of Efficient and Natural Proof Systems Third Workshop of the Amadeus Project on Proof Compression (INRIA Nancy-Grand Est) and Workshop on Algebraic Proof Theory (Gudauri) 16 and 24 September 2013
• Towards More Efficient and Natural Proof Systems 14th Wessex Theory Seminar 27 June 2012
• Redesigning Logical Syntax with a Bit of Topology Technische Universität Dresden 31 May 2011
• Removing Syntax From Proof Theory University of Bath (videolink with Swansea) 9 December 2010
• Some Ideas on How to Find Better Proof Representations University of Bath 28 November 2010
• Geometric Normalisation with Atomic Flows Journées GEOCAL-LAC, Nice 16 March 2010
• Normalisation with Atomic Flows Università di Bologna e di Torino 20-21 January 2010
• Ten Years of Deep Inference Università di Pisa 19 January 2010
• Some News on the Proof Complexity of Deep Inference University of Bath 11 November 2009
• Beyond University of Oslo, invited talk at Gentzen Systems and Beyond, workshop co-located with Tableaux 2009 6 July 2009

6 Research Students

• 2021–2025 Cameron Allett (PhD, 2nd supervisor).
• 2021–2025 Daniel Castle (PhD, 2nd supervisor).
• 2019–2023 Georgina Majury (PhD, 2nd supervisor).
• 2019–2023 Victoria Barrett (PhD, supervisor).
• 2018–2021 Chris Barrett (PhD, 2nd supervisor).
• 2015–2019 William John Gowers (PhD, 2nd supervisor).
• 2013–2019 Daniel Schmitter (PhD, 2nd supervisor).
• 2015–2019 Alessio Santamaria (PhD, 2nd supervisor).
• 2015–2019 David R. Sherratt (PhD, 2nd supervisor).
• 2014–2019 Benjamin Pring (PhD, 2nd supervisor).
• 2014–2018 Benjamin Ralph (PhD, supervisor). Now a senior lecturer at the University of Bath. Thesis (Pdf).
• 2013–2016 Andrea Aler Tubella (PhD, supervisor). Now a post-doc at Umeå University. Thesis (Pdf).
• 2010–2013 Anupam Das (PhD, supervisor). Now an associate professor at the University of Birmingham. Thesis (Pdf).
• 2006–2009 Tom Gundersen (PhD, supervisor). Until December 2013 a post-doc at the PPS lab of Paris VII/CNRS. Thesis (Pdf).
• 2003–2006 Ozan Kahramanoğulları (PhD, supervisor). Now an assistant professor at the University of Trento. Thesis (Pdf).
• 2000–2003 Kai Brünnler (PhD, supervisor). Now a professor at Berner Fachhochschule. Thesis (Pdf).
• 2000–2003 Lutz Straßburger (PhD, supervisor). Now a research director at LIX & INRIA–Saclay-Île-de-France, École Polytechnique, Palaiseau (Paris). Thesis (Pdf).
• 2000–2001 Alwen Tiu (MSc, supervisor). Now an associate professor at Australian National University in Canberra. Thesis (Pdf).

7 Recent Grants

• Efficient and Natural Proof Systems 2013–2016. Three-year EPSRC research project at University of Bath. 756,061 GBP (full economic costing, including indexation and a research studentship funded by the University of Bath). Principal investigator is Alessio Guglielmi, co-investigator is Guy McCusker.
• Sharing and Sequentiality in Proof Systems with Locality 2012–2014. Two-year Royal Society International Exchanges Scheme. Exchange programme between University of Bath and Università di Torino. The two sides get 11,960 GBP. Principal investigators: Alessio Guglielmi and Luca Roversi.
• REDO: Redesigning Logical Syntax 2009–2010. INRIA—Action de Recherche Collaborative. Two-year project of the teams Calligramme/Démosthène and Parsifal (INRIA) and the Computer Science Department of the University of Bath. The project gets 80,000 EUR. Principal investigators are Alessio Guglielmi, François Lamarche and Lutz Straßburger (coordinator).
• Identity and Geometric Essence of Proofs (Démosthène) ANR—Chaire d'excellence 2008–2010. Two-year project at LORIA. The project gets about 355,000 EUR from the Agence Nationale de la Recherche, out of a total cost of 750,448 EUR, the rest of which is covered by INRIA. Principal investigator is Alessio Guglielmi.
• Complexity and Non-Determinism in Deep Inference 2007–2008. 17 month project at University of Bath. 118,072 GBP (out of a total cost of 147,591 GBP) from the Engineering and Physical Sciences Research Council (EPSRC) Principal investigator is Alessio Guglielmi, co-investigator is Paola Bruscoli.
• New Deductive Systems, Normalisation Methods and Semantics for Deep Inference  2006–2007. Alliance—Franco-British Partnership Programme. Two-year exchange programme between the University of Bath and the PPS group in Paris. Bath gets 4,300 GBP from the British Council (principal investigator Alessio Guglielmi) and PPS gets 6,250 EUR from the French MAE and the Ministry of Research (principal investigator Michel Parigot).
• Analyticity and Proof Search for Modal Logics in Deep Inference 2006–2008. British-German Academic Research Collaboration Programme. Two-year exchange programme between the University of Bath and the Technische Universität Dresden. Bath gets 2,650 GBP from the British Council (principal investigator Alessio Guglielmi) and Dresden gets 5,694 EUR from the German Academic Exchange Service (principal investigator Steffen Hölldobler).

8 Mailing Lists

I help running a mailing list devoted to proof theory:

• More on the Proof Theory mailing list

I also manage a mailing list specifically devoted to structural proof theory and deep inference:

• More on the Frogs mailing list

Groucho is here.

9 Teaching

In my teaching, I insist on the practical motivations behind science. One of my deepest convictions is that being grounded in practice is an essential ingredient also for interesting research. I tend to build my courses around 'important questions'. I ask students to think about natural questions and problems and explore different paths and possible lines of attack before showing the solution. I privilege concrete knowledge over abstract one: I prefer to insist on some core concepts and the ability to solve (perhaps conceptual) exercises rather than showing one more theorem. I also try to convey the idea that abstraction might become necessary in order to be effective at solving practical problems. It worked for me with the conception of deep inference, where the desire of managing certain concrete problems of concurrent languages led me to reformulate the very foundations of proof theory. In summary, I prefer to transmit basic and general methods whenever it is possible. I am sure that a solid education in the fundamentals is useful also for the majority of students, who do not intend to pursue a research career: higher education should provide mental flexibility, not just notions.

In the past, I taught, among others, Formal Logic and Semantics, Logic and Its Applications, Computability and Decidability, Proof Theory and Deep Inference, Complexity Theory, Logic, Deep Inference and the Calculus of Structures, Sequent Calculus and Abstract Logic Programming, Deduction Systems, Networking and Advanced Programming Principles.

15.5.2023 Alessio Guglielmi email