Deep inference for temporal logics

Lutz Straßburger, INRIA Futurs

LIX, Ecole Polytechnique, Palaiseau

Temporal logics are nowadays widely used in formal verification of hardware and software. So far, most fundamental investigations into temporal logics have been carried out from the model theoretic aspect, and not from the proof theoretic aspect. The main reason for neglecting the proof theory of temporal logic seems to be the difficulty to design a proof theoretically well-behaved deductive system for temporal logics in standard formalisms like natural deduction or sequent calculus.

Deep inference is a recently developped paradigm for presenting deductive systems. It has successfully be applied for various logics, like classical logic, linear logic, intuitionistic logic, and modal logics. The novelty is that inference rules are allowed to be applied like rewrite rules deep inside formulas. This is not possible with shallow inference systems like sequent calculus or natural deduction.

This suggests the possibility of using deep inference for giving deductive systems for temporal logics and investigating their proof theory.

Knowledge either in deep inference or in temporal logics should be present.

The following bibliography is indicative of the kind of papers that will be part of this research effort.

1. Kai Brünnler. Deep Inference and Symmetry for Classical Proofs. Phd Thesis, TU Dresden, 2003.
2. Charles Stewart and Phiniki Stouppa. A Systematic Proof Theory for Several Modal Logics. Advances in Modal Logic, Volume 5, pp. 309--333, 2005.
3. Lutz Straßburger. Deep Inference for Hybrid Logic. International Workshop on Hybrid Logic 2007, part of ESSLLI'07, Dublin, 2007.

Lutz Straßburger's list of problems
Parsifal's web page
Alessio Guglielmi's web page on deep inference