Dr Alessio Guglielmi
The following projects fit into a more general, multi-year, multi-person research project called `Deep Inference and the Calculus of Structures┤. You can find up-to-date, complete information on deep inference at http://alessio.guglielmi.name/res/cos. The projects do not presuppose any previous knowledge of deep inference or proof theory. However, some exposure to logic and proof theory, like, for example, the sequent calculus and natural deduction, is very helpful, especially because it can provide the initial motivation for getting into a project.
Some of the following projects should be attractive for mathematically oriented students who wish to learn quickly about a growing research field with many applications in computer science. The projects might naturally lead into more difficult, open research problems in deep inference, like those listed in http://alessio.guglielmi.name/res/cos/crt.html. Some other projects only require a superficial knowledge of proof theory and are instead focused on developing programs useful for the community of researchers in deep inference. In this case, we will usually further develop the GraPE system, an excellent open source project.
Deep inference is a new, breakthrough methodology in proof theory. Proof theory is the mathematical discipline that studies mathematical proofs as mathematical objects. It has profound connections with two main computer science areas: the design of computer languages and computational complexity. It also has connections with computational linguistics.
Deep inference is better than the traditional proof theoretic approaches for two main reasons: 1) it allows for the simple expression and analysis of a much greater range of logics, some of which very important for computer science; 2) it yields exponentially shorter proofs for large classes of formulae.
The calculus of structures (CoS) is now a completely developed proof theoretic formalism adopting the deep inference methodology. Like in the sequent calculus or natural deduction, we can design deductive systems in CoS. One of the differences is that, in CoS, it is usually much easier to design deductive systems than in the other formalisms.
The original motivations of this research come from certain ideas about symmetry inspired by physics (see the introductory parts of the paper http://www.computational-logic.org/~guglielm/p/SystIntStr.pdf). There is an enthusiastic, young, international community doing research in deep inference, which is kept together by regular meetings and the mailing list Frogs: http://ProofTheory.ORG/frogs.
The ideas below are meant to be just suggestions, any other idea / modification / improvement is negotiable, based on the interests of the student.
- Graphical interface to CoS theorem provers (several projects are possible under this heading)
- People are developing theorem provers for several logics expressed in CoS; for an overview, see the page http://www.informatik.uni-leipzig.de/~ozan/maude_cos.html. Maude and TOM are the systems into which the existing CoS implementations are expressed. The GraPE system is an interface to the Maude implementations which is being actively developed as an open source project. We can focus projects on the development of one or more new features into GraPE. These will be essentially features of the graphical interface, programmed in Java. Some knowledge of Maude will be acquired during the project, of course. Much of these projects will be about implementing the interface, but, to be effective, the student must know CoS and what people would like to do with it.
- New, graphical representation of CoS proofs
- Proofs in any CoS system tend to be typographically rather unfriendly, because they just consist of possibly long formulae chained together in possibly long queues. However, the `real┬┤ structure of these proofs is a graph. The problem is to extract the graph information (in a certain minimalistic way) from any CoS proof, and display the result. The output should be in the form of graphs displayable on the web and compilable by TeX (for inclusion in papers, for example). For this, the definition of an intermediate language for describing the graphs might be useful. This project does not require a deep knowledge of CoS or of proof theory, the emphasis will be on the good quality of the output.
- Representing proofs in wired deduction
- Wired deduction is a new deep inference formalism, currently being developed (see http://www.computational-logic.org/~guglielm/p/AG14.pdf). A proof in wired deduction consists of certain primitive graphs joined together according to certain rules. While a rigorous definition of composition for these graphs is possible, there currently is no high level language for representing wired deduction proofs: they can be drawn on paper, but they cannot be conveniently described. The goal of the project is to design such a language, and then use it as a basis for a set of TeX macros for drawing wired deduction proofs. This project does not require a deep knowledge of CoS or of proof theory, the emphasis will be on the good quality of the language and, slightly less importantly, on the good quality of the TeX output.
- Experiments with classical logic in CoS
- Deep inference allows for a huge new range of possible strategies when searching for proofs. So far, no extensive experimental study has been accomplished about the new possibilities. We know that for many classes of tautologies, analytic CoS presentations of classical logic admit polynomial size proofs instead of the exponential ones that are only possible in other analytic formalisms. We don't know whether these shorter proofs can also be found efficiently. This project focuses on propositional classical logic in CoS, and its goal is to make an extensive study of the most promising strategies. We want to learn, concretely!, when and how deep inference helps in finding short proofs efficiently. The starting point will be the Maude implementations of Ozan Kahramanogullari http://www.informatik.uni-leipzig.de/~ozan and some of his papers on the subject. This project requires a good understanding of deep inference, CoS, propositional classical logic, and a great deal of intuition and ability in interpreting experimental data.