Alessio Guglielmi's Research and Teaching

Electric lamps were not invented by improving candles

Perhaps you were looking for the Deep Inference pages?

Contents Overview of Research Normalisation and Proof Complexity Identity of Proofs and Deductive Nets Summary Recent Papers Notes Recent Talks Research Students Recent Grants Mailing Lists Teaching

Address Department of Computer Science University of Bath Bath BA2 7AY United Kingdom fax: +44 (1225) 383 493 AlessioATGuglielmi.name

1Overview 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.1Normalisation 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 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 design of deductive systems, which are based on more basic and simple principles than traditional proof theory offers.

1.2Identity 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.3Summary

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.

The following web pages contain more details about my current research:

• Deep Inference (FAQ, papers, notes, etc.)
• Deep Inference—Current Research Topics and Open Problems

Perhaps you might be interested in my political opinions.

2Recent Papers

Abstracts ON or OFF (Javascript required).

• A Logical Basis for Quantum Evolution and Entanglement
  Richard F. Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden and Lutz Straßburger
  AbstractWe reconsider discrete quantum casual 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.
  Pdf12 May 2011
  Submitted

• A Quasipolynomial Normalisation Procedure in Deep Inference
  Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot
  AbstractJeřábek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek’s result: we give a quasipolynomialtime cut-elimination procedure in propositional-logic 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 trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure. We also show how the technique can be extended to obtain a more general notion of normalisation called streamlining.

  • Journal version pdf18 April 2011
    Submitted
  • Conference version pdf25 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
  • Original preprint pdf25 January 2010
    The title of this version is Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae; it has some constructions that appear nowhere else

• A System of Interaction and Structure V: The Exponentials and Splitting
  Alessio Guglielmi and Lutz Straßburger
  AbstractSystem 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.
  Pdf21 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
  AbstractWe 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.
  Pdf27 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
  AbstractThis 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.
  Pdf29 April 2010
  LICS 2010 Proceedings (IEEE), pp. 284–293

• A Proof Calculus Which Reduces Syntactic Bureaucracy
  Alessio Guglielmi, Tom Gundersen and Michel Parigot
  AbstractIn 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.
  Pdf12 April 2010
  RTA 2010, Leibniz International Proceedings in Informatics (LIPIcs) 6, pp. 135–150
  This paper supersedes the note Formalism A.

• Personal Portrait of Giorgio Levi
  Alessio Guglielmi
  Pdf23 October 2009
  Theoretical Computer Science 410 (46) 2009, pp. 4605–4607

• On the Proof Complexity of Deep Inference
  Paola Bruscoli and Alessio Guglielmi
  AbstractWe 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.
  Pdf19 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
  AbstractWe 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.
  Journal page (pdf/postscript)31 March 2008
  Logical Methods in Computer Science 4 (1:9) 2008, pp. 1–36

• A System of Interaction and Structure
  Alessio Guglielmi
  AbstractThis 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.
  Pdf27 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
  AbstractFull 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 pdf10 September 2003
    LPAR '03, LNCS 2850, pp. 389–406
  • Full paper pdf22 November 2005
    Theoretical Computer Science 360 (1–3) 2006, pp. 42–76

• A Non-commutative Extension of MELL
  Alessio Guglielmi and Lutz Straßburger
  AbstractWe 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.
  Pdf9 August 2002
  LPAR 2002, LNCS 2514, pp. 231–246

• A First Order System with Finite Choice of Premises
  Kai Brünnler and Alessio Guglielmi
  AbstractWe 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.
  Pdf1 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
  AbstractAbstract 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.
  Pdf10 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
  AbstractWe 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.
  Pdf28 June 2001
  CSL 2001, LNCS 2142, pp. 54–68

3Notes

• Polynomial Size Deep-Inference Proofs Instead of Exponential Size Shallow-Inference ProofsAlessio GuglielmiBy 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 2007SlidesSuperseded by On the Proof Complexity of Deep Inference

• Finitary CutAlessio GuglielmiWe 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 2007Superseded by A First Order System with Finite Choice of Premises

• On Analytic Inference Rules in the Calculus of StructuresPaola Bruscoli and Alessio GuglielmiWe discuss the notion of analytic inference rule for propositional logics in the calculus of structures.25 November 2009

• ButterfliesAlessio GuglielmiIf you're interested in NEL and BV, try and find the mistake in this note.29 July 2005

• Some News on Subatomic LogicAlessio GuglielmiI found a simple explanation for the soundness of the subatomic inference rule.28 July 2005

• Red and BlueAlessio GuglielmiThe 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 InferenceAlessio GuglielmiSome discussion and then the first attempt at wired/weird deduction.17 June 2005Proceedings of Structures and Deduction '05, pp. 53–68

• Formalism BAlessio GuglielmiInference rules operate on derivations.20 December 2004

• Formalism AAlessio GuglielmiI generalise the notion of derivation for taking care of a certain kind of bureaucracy.23 April 2004Superseded by A Proof Calculus Which Reduces Syntactic Bureaucracy

• Resolution in the Calculus of StructuresAlessio GuglielmiIt 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

• MismatchAlessio GuglielmiThere 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 2003Brief note for the specialist, posted to the Foundations of Mathematics and Proof Theory lists

• Normalisation Without Cut EliminationAlessio GuglielmiI propose a possible notion of equivalence for proofs in classical logic, sort of a normal form for case analysis.25 February 2003

• Subatomic LogicAlessio GuglielmiOne 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

• On Lafont's CounterexampleAlessio GuglielmiLafont'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

• RecipeAlessio GuglielmiA 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 MiraclesAlessio GuglielmiI argue about three properties closely related to cut elimination and interpolation theorems. 18 October 2002

4Recent Talks

• Towards More Efficient and Natural Proof Systems14th Wessex Theory Seminar27 June 2012

• Redesigning Logical Syntax with a Bit of TopologyTechnische Universität Dresden31 May 2011

• Removing Syntax From Proof TheoryUniversity of Bath (videolink with Swansea)9 December 2010

• Some Ideas on How to Find Better Proof RepresentationsUniversity of Bath28 November 2010

• Geometric Normalisation with Atomic FlowsJournées GEOCAL-LAC, Nice16 March 2010

• Normalisation with Atomic FlowsUniversità di Bologna e di Torino20-21 January 2010

• Ten Years of Deep InferenceUniversità di Pisa19 January 2010

• Some News on the Proof Complexity of Deep InferenceUniversity of Bath11 November 2009

• BeyondUniversity of Oslo, invited talk at Gentzen Systems and Beyond, workshop co-located with Tableaux 20096 July 2009

5Research Students

• 2010–2013Anupam Das (PhD). University of Bath.

• 2006–2009Tom Gundersen (PhD). University of Bath. Now a post-doc at the LIX & INRIA–Saclay-Île-de-France, École Polytechnique, Palaiseau (Paris). Thesis (Pdf).

• 2003–2006Ozan Kahramanogullari (PhD). Now a researcher at The Microsoft Research-University of Trento Centre for Computational and Systems Biology, Trento. Thesis (Pdf).

• 2000–2003Kai Brünnler (PhD). Until 2011 a researcher at the University of Bern. Thesis (Pdf).

• 2000–2003Lutz Straßburger (PhD). Now a researcher at LIX & INRIA–Saclay-Île-de-France, École Polytechnique, Palaiseau (Paris). Thesis (Pdf).

• 2000–2001Alwen Tiu (MSc). Now a researcher at Australian National University (Canberra). Thesis (Pdf).

6Recent Grants

• Efficient and Natural Proof Systems2013–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 Locality2012–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 Syntax2009–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 Inference2007–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 Inference2006–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).

7Mailing Lists

I help running a mailing list devoted to proof theory: click here to subscribe or here to unsubscribe.

• More on the Proof Theory mailing list

I also manage a mailing list specifically devoted to structural proof theory and deep inference: click here to subscribe or here to unsubscribe.

• More on the Frogs mailing list

8Teaching

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 of solving (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.

I am teaching Networking and Advanced Programming Principles.

5.3.2013Alessio Guglielmiemail