Alessio Guglielmi's Research and Teaching / Deep Inference

Deep Inference
Web-Based Quantum Bio-Cryptography and Creative Nano-Security for the Cloud

This page tries to be a comprehensive account of the ongoing research on deep inference.

Deep inference started as a personal project, but it is now growing fast and I'm struggling to keep pace with all the developments. Some of them I do not understand in detail.

Please keep in mind that what I wrote below can be very subjective and not reflect the opinions of the people involved in this research.

If you disagree or find inaccuracies, please let me know!

If you are an expert of proof theory and want to quickly understand what deep inference is about, go to Deep Inference in One Minute.

Latest News

19 December 2012The three-year EPSRC project Efficient and Natural Proof Systems at the University of Bath has been approved.

20 January 2012The two-year Royal Society International Exchanges Grant Sharing and Sequentiality in Proof Systems with Locality between the University of Bath and the Università di Torino has been approved.

15-17 June 2011First Structural meeting in Paris.

2 December 2010ANR/FWF three-year project Structural is approved (about 2,324,000 EUR).

14–16 September 2010Meeting REDO: Redesigning Logical Syntax in Bath.

9–20 August 2010Course Introduction to Proof Theory, by Lutz Straßburger, at ESSLLI 2010 in Copenhagen

23–24 February 2010Meeting Geometric and Logic Approaches to Computation in Nancy

Contents

This page contains:

  1. Introduction
    1. Proof Systems
    2. Formalisms
    3. Shallow and Deep Inference
    4. Main Results in Deep Inference
    5. Perspective
    6. History
  2. Frequently Asked Questions and Useful Remarks for Referees
  3. Papers
    1. Classical and Intuitionistic Logic
    2. Proof Complexity
    3. Nested Sequents
    4. Modal Logic
    5. Linear Logic
    6. Commutative/Non-commutative Linear Logic
    7. Proof Nets, Semantics of Proofs and the War to Bureaucracy
    8. Language Design
    9. Implementations
  4. Current Research Topics and Open Problems
  5. Counterexamples
  6. Notes
  7. Mailing List
  8. Grants
  9. Beans
  10. Events
  11. TeX Macros and BibTeX database

Other pages contain more detailed information:

1Introduction

Deep inference is a new methodology in proof theory, which is the discipline that studies mathematical proofs. Deep inference is about designing proof systems and formalisms with excellent properties of analyticity, proof complexity and semantics of proofs. With deep inference, we express logics that elude the traditional methods of proof theory, in particular we represent modal logics and logics related to process algebras. Deep inference provides beautiful and simple proof systems and formalisms.

The following picture illustrates a point of view on deep inference: most of traditional proof theory adopts a methodology that we call shallow inference. The methodologies of shallow and deep inference inspire the design of formalisms, which, in turn, express proof systems for several logics. At the bottom of the picture, solid arrows signal the existence of widely established proof systems in the given formalisms, while dashed arrows stand for a shabbier relationship. Some formalisms in deep inference are under development (dashed border).

We will now explore the concepts in the picture in more detail, and we will summarise the results we obtained so far in deep inference, and the current research themes.

1.1Proof Systems

A formal proof consists in breaking down a mathematical argument into small inference steps and connecting them together. Its validity can then be checked by local inspection of the inference steps, as dictated by syntactic inference rules. Checking a proof is a mechanical procedure, and this is much of its value: human fallacies are ruled out, and computers can be employed for checking and also discovering proofs.

A logic can be considered a class of theorems. Normally, mathematics is performed in first-order classical logic, but, in many cases, we use stronger or weaker systems. In computer science, we use many logics, some of which are rather far apart from classical logic.

A set of inference rules is called a (proof) system. For any given logic, several different proof systems exist, which prove the same theorems. However, they might greatly differ for several properties, notably:

In our research, these three properties of proof systems play a crucial role.

1.2Formalisms

Proof systems can be classified according to the style they adhere to. These classes are not always mathematically defined, but, in practice, they are recognisable. We say that proof systems belong to different formalisms. The most important traditional formalisms are the Frege-Hilbert formalism, the sequent calculus and natural deduction, and there are many others; the sequent calculus* is special because it supports analyticity.

Different formalisms allow for proof systems with different properties. For example, systems in the natural deduction formalism do not lend themselves easily to proof search. Systems with excellent proof search properties, due to analyticity, can be designed in the sequent calculus*; however, they produce proofs which are exponentially bigger than those in natural deduction, on certain classes of theorems.

Often, formalisms entail interesting notions of normalisation inside their proof systems. For example, natural deduction systems possess a notion of normalisation that corresponds closely to a very important notion of computation, in what we call the Curry-Howard correspondence: normalising proofs in certain systems for intuitionistic logic corresponds to computing in the simply-typed lambda-calculus.

It is sometimes very challenging to design proof systems for a given logic in a given formalism: for example, many variations of modal logic, which are easily expressible in Frege-Hilbert systems, only find awkward presentations in sequent-calculus systems. Often, the reason for adopting the sequent calculus* is for getting analyticity; however, in some cases, with great effort, one only gets sequent-calculus systems that are not analytic.

For many logics, like modal logic, it might be necessary to adopt non-traditional formalisms, which allow for more freedom in designing inference rules. For example, many modal logic variations can be expressed with analytic proof systems in a formalism called hypersequents, which is a generalisation of the sequent calculus*.

1.3Shallow and Deep Inference

Formalisms, to a very large extent, dictate the design of inference rules. For example, natural deduction prescribes that, for every connective, two rules are given: one that introduces it and one that eliminates it.

In all traditional formalisms, and in the modern ones derived from them, a methodology that we call shallow inference is adopted. 'Shallow' inference rules operate on connectives that appear in close proximity to the root of formulae, when we consider them as trees. For example, the introduction and elimination rules of natural deduction operate on root connectives of formulae. The sequent calculus usually goes one level deeper than natural deduction, and in some cases two levels deeper. The hypersequents formalism, which is derived from the sequent calculus, does the same.

Shallow inference is a very natural methodology, because it is about generating proofs by a straightforward structural induction on the formulae they prove. However, shallow inference is not optimal regarding the three properties of proof systems mentioned above, and in particular:

Shallow inference also has difficulties in coping with modal logic: modal logic theories can be defined in Frege-Hilbert systems, but obtaining analyticity for them (in sequent systems) can be very difficult, and in some cases unachieved. It is equally difficult or impossible to express proof systems for some logics involving non-commutativity, linearity and other features typical of computer-science concurrency languages, like process algebras.

All these seemingly heterogeneous difficulties can largely be ascribed to one cause: the adoption of the shallow-inference methodology. In fact, and very roughly, all shallow-inference formalisms require the adoption of a so-called meta, or structural, level for organising the 'pieces' of formulae obtained by the structural induction they adopt. For example, the sequent calculus organises these pieces into sets and trees. Because of the historical development of proof theory, the meta level, in a sense, coincides with the algebraic structure of classical logic. This becomes an increasingly serious impediment the more the logics one wants to express depart from classical logic.

Deep inference is based on a very simple idea: formalisms adopt the same algebraic structure of any given logic for keeping organised the pieces of proofs; in other words, there is no meta level. This means that inference rules must be able to operate at any level ('deeply') inside formula trees.

The idea is simple, but the adoption of deep inference poses two difficult challenges:

1.4Main Results in Deep Inference

We developed the proof theory of a deep-inference formalism that we call the calculus of structures. This is the simplest formalism conceivable in deep inference, because inference rules behave as rewrite rules in term rewriting systems. The calculus of structures is a milestone in the development of deep inference, because of its simplicity and its resemblance to traditional formalisms. Moreover, the normalisation techniques of the calculus of structures are applicable also to other formalisms in deep inference, currently under development.

We achieved the following results for the calculus of structures:

The calculus of structures generalises most shallow-inference formalisms, in particular the sequent calculus. This means that every proof in shallow-inference formalisms can be 'mimicked' in the calculus of structures, by preserving complexity and without losing any structural property.

It might be desirable, for example for constraining proof search and reducing non-determinism, to reach a compromise between the sequent calculus and the calculus of structures. A new deep-inference formalism, called nested sequents, has been developed, especially targeting modal logics. In deep sequents (and so, in the calculus of structures), modal logics like B and K5, which do not enjoy analytic presentations in the sequent calculus, find simple analytic systems.

The cirquent calculus, a new formalism recently developed by Giorgi Japaridze, benefits from a deep-inference presentation.

The calculus of structures promoted the discovery of a new class of proof nets for classical and linear logic. Proof nets are not proof systems, because they cannot be checked by local inspection, but they play a crucial role in understanding the semantics of proofs, which is one of the most active research areas in proof theory, in close connection with theoretical computer science.

1.5Perspective

Designing syntax is an eminently semantic activity: the only way to avoid creating monsters is having clear semantic objectives and guidance. The ambition of deep inference is to provide a unifying, simple syntax of proofs, which, above all, reflects the meaning of proofs. The semantics of proofs depends heavily on syntax, because proofs, more than formulae, are objects that are built, they are constructions, not just statements. Because of lack of adequate syntax, at present, we are basically unable to answer questions like Are two given proofs the same? (This is the so-called Hilbert's 24th problem.) The only answers we can give right now are either trivial (and uninteresting) or excessively technical. One of the main objectives of deep inference is to provide a simple answer to this question.

1.6History

Deep inference comes from linear logic and process algebras; more specifically, it comes from seeing proofs as concurrent processes. The first development has been the definition of the calculus of structures and a cut elimination proof for the logic BV, which was studied for being the logical counterpart of the core of the process algebra CCS. We realised that the techniques developed for BV had a much wider applicability, so we broadly developed the calculus of structures and studied its many novel normalisation properties. The initial phase of development took place in Dresden, from 1999 to 2003; now, deep inference is developed in several laboratories around the world. The recent results on modal and intuitionistic logics, proof nets and semantics, and implementations, complete the establishing of deep inference as a solid and comprehensive methodology in proof theory.

2Frequently Asked Questions and Useful Remarks for Referees

Please do not hesitate to ask questions, either by email to me, or, even better, by using our mailing list.

  1. General
    1. What is deep inference?
    2. What is a structure?
    3. Isn't the word 'structure' reserved for semantics?
    4. Proof theory is famous for producing horrible proofs of its own theorems; are you doing any better?
    5. Does the calculus of structures automatically introduce a mix rule in any system?
    6. In proof search, the nondeterminism induced by deep inference is enormous, how can I cope with this?
    7. The good properties of the proofs in the calculus of structures are obtained by an extensive use of hidden equalities; are you cheating?
    8. Aren't proof nets top-down symmetric objects, not differently from proofs in the calculus of structures?
  2. The Calculus of Structures Vs. the Sequent Calculus
    1. Isn't the calculus of structures just a trivial notational variation of the sequent calculus?
    2. Can you do in the calculus of structures anything you can do in the sequent calculus?
    3. There is more bureaucracy in the calculus of structures than in the sequent calculus, and this is why you get more properties: simply because you have more stuff to work with, right?
  3. Cut Elimination and the Subformula Property
    1. You make a big deal of having the cut rule in atomic form; but can't you do the same in the sequent calculus?
    2. What's the point in proving again cut elimination for classical and linear logic?
    3. By the way, what's the point in dedicating an entire paper to such an easy statement as cut elimination for propositional classical logic in the calculus of structures?
    4. Your 'cut-free' systems do not have the subformula property! Are you crazy?
  4. Term Rewriting
    1. Isn't a system in the calculus of structures just a term rewriting system (modulo an equational theory)?
    2. If so, why not using the term rewriting terminology and conventions?
    3. But then what about rewriting logic?
  5. Philosophy
    1. Do the inference rules in the calculus of structures have an associated theory of meaning, like the inference rules in the sequent calculus and natural deduction?

3Papers

The following material is broad in scope; if you are new to deep inference and the calculus of structures, start here:

Abstracts ON or OFF (Javascript required).

In the rest of the section, all the papers I know of are listed according to their subject, in no particular order.

3.1Classical and Intuitionistic Logic

So far, for classical logic in the calculus of structures we achieved:

We can present intuitionistic logic in the calculus of structures with a fully local, cut-free system. The logic of bunched implications BI can be presented in the calculus of structures. Japaridze's cirquent calculus benefits from a deep-inference presentation, in particular in the case of propositional logic.

The following papers exist, in addition to Deep Inference and Its Normal Form of Derivations and Deep Inference and Symmetry in Classical Proofs, mentioned above:

Abstracts ON or OFF (Javascript required).

3.2Proof Complexity

The basic proof complexity properties of propositional logic in the calculus of structures are known. Deep inference is as powerful as Frege systems, and more powerful than Gentzen systems, in the restriction to analytic systems.

The following papers exist:

Abstracts ON or OFF (Javascript required).

3.3Nested Sequents

A new formalism called 'nested sequents' has been defined, which is especially suitable to modal logics.

The following papers exist, in addition to Nested Sequents, mentioned above:

Abstracts ON or OFF (Javascript required).

3.4Modal Logic

We can present systematically several normal propositional modal logics, including S5, B and K5, for which cut elimination is proved. We also investigated geometric theories, some of which we expressed in the calculus of structures.

The following papers exist:

Abstracts ON or OFF (Javascript required).

3.5Linear Logic

Linear logic enjoys presentations in deep inference that obtain the expected properties of locality, with rather astounding decomposition theorems and the usual, general normalisation results.

The following papers exist, in addition to Linear Logic and Noncommutativity in the Calculus of Structures, mentioned above:

Abstracts ON or OFF (Javascript required).

3.6Commutative/Non-commutative Linear Logic

We conservatively extend mixed multiplicative and multiplicative exponential linear logic with a self-dual non-commutative operator. The systems so obtained cannot be presented in the sequent calculus, but they enjoy the usual properties of locality, decomposition and cut elimination available in the calculus of structures. We can present Yetter's cyclic linear logic in the calculus of structures and prove cut elimination; interestingly, cyclicity is naturally subsumed by deep inference. New, purely proof-theoretical, techniques are developed for reducing the non-determinism in the calculus of structures.

The following papers exist, in addition to Linear Logic and Noncommutativity in the Calculus of Structures, mentioned above:

Abstracts ON or OFF (Javascript required).

3.7Proof Nets, Semantics of Proofs and the War to Bureaucracy

Deep inference and the calculus of structures are influencing the design of a new generation of proof nets. Moreover, they offer new insight for semantics of proofs and categorical proof theory. Finally, they open decisive new perspectives in the fight against bureaucracy.

The following papers exist, in addition to A General View of Normalisation Through Atomic Flows and Categorical Models of First Order Classical Proofs, mentioned above:

Abstracts ON or OFF (Javascript required).

3.8Language Design

Thanks to a self-dual non-commutative extension of linear logic one gets the first purely logical account of sequentiality in proof search. The new logical operators make possible a new approach to partial order planning and its relation to concurrency.

The following papers exist, in addition to Nondeterminism and Language Design in Deep Inference, mentioned above:

Abstracts ON or OFF (Javascript required).

3.9Implementations

Ozan Kahramanoğulları, Pierre-Etienne Moreau and Antoine Reilles are implementing calculus-of-structures proof systems in Maude and in Tom. Ozan managed to achieve efficiency without sacrificing proof theoretic cleanliness, and he is obtaining results of independent theoretical interest. There are two slides presentations:

Max Schäfer has built a graphical proof editor in Java, called GraPE, for the Maude modules written by Ozan Kahramanoğulları; this means that one can interactively build and find proofs in several deep-inference systems.

The following papers exist, in addition to Nondeterminism and Language Design in Deep Inference, mentioned above:

Abstracts ON or OFF (Javascript required).

4Current Research Topics and Open Problems

In this page I list all open and currently explored research subjects I am aware of. The solutions to most of these problems are instrumental in reaching the common goal of a comprehensive bureaucracy-free proof theory based on geometric methods.

  1. Introduction
  2. Calculus of Structures
    1. Classical, Intuitionistic and Intermediate Logics
    2. Linear Logic
    3. Modal Logic
    4. Commutative/Non-commutative Linear Logic
    5. Computability Logic
    6. Language Design
    7. Proof Search
    8. Implementations
  3. Formalism A
  4. Formalism B, Deductive Nets and Identity of Derivations
  5. Proof Nets and Semantics of Proofs
  6. Deep Inference and Display Calculus
  7. Deep Inference and Hypersequents
  8. Subatomic Proof Theory
  9. Causal Quantum Evolution

5Counterexamples

Finding counterexamples is one of the funniest sides of our activity. They are typically of a very combinatorial nature, due to the new combinatorial possibilities offered by deep inference.

  1. Classical Logic
    1. Atomic contraction is not achievable in the sequent calculus
    2. Contraction cannot be pushed to the root of sequent calculus proofs
    3. Cocontraction does not replace contraction
    4. Binary tautologies and atomic contraction
  2. Modal Logic
    1. 4 rules cannot be interchanged for K4
  3. BV
    1. BV cannot be expressed in the sequent calculus
    2. Comerge does not permute over merge
    3. Interaction can only be pushed up in the presence of coseq

6Notes

7Mailing List

There is a very friendly mailing list devoted to deep inference, proof nets, structads, the calculus of structures and other amphibians of structural proof theory, named Frogs. Join it!

8Grants

These are the current and recent grants I am aware of, regarding deep inference:

I did not indicate individual travel grants.

9Beans

10Events

Deep inference was one of the main attractions at the following international events:

Deep inference and the calculus of structures have been taught at

11TeX Macros and BibTeX database

The Virginia Lake LaTeX macros help typing deep inference structures, derivations and atomic flows.

The DedStraker TeX macros are now obsolete.

This BibTeX database of deep-inference publications is kept updated.

5.7.2014Alessio Guglielmiemail