Exploiting non-canonicity in the sequent calculus
Résumé
Although logic and proof theory have been successfully used as a framework for the specification of computation systems, there is still an important gap between the systems that logic can capture and the systems used in practice. This thesis attempts to reduce this gap by exploiting, in the context of the computation-as-proof-search paradigm, two non-canonical aspects of sequent calculus, namely the polarity assignment in focused proofs and the linear logic exponentials. We exploit these aspects in three different domains of computer science: tabled deduction, logical frameworks, and algorithmic specifications. This thesis provides a proof theoretic explanation for tabled deduction by exploiting the fact that in intuitionistic logic atoms can be assigned arbitrary polarity. A table is a partially ordered set of formulas and is incorporated into a proof via multicut derivations. Here, we consider two cases: the first case is when tables contain only finite successes and the second case is when tables may also contain finite failures. We propose a focused proof system for each one of these cases and show that, in some subsets of logic, the only proofs and open derivations available in these systems are those that do not attempt to reprove tabled formulas. We illustrate these results with some examples, such as simulation, winning strategies, and let polymorphism typechecking. We show that linear logic can be used as a general framework for encoding proof systems for minimal, intuitionistic, and classical logics. First, we demonstrate that with a single linear logic theory, one can faithfully account for natural deduction (normal and non-normal), sequent calculus (with and without cut), natural deduction with general elimination rules, free deduction and tableaux proof systems by using logical equivalences and different polarity assignments to meta-level literals. Then we exploit the fact that linear logic exponentials are not canonical and propose linear logic theories that faithfully encode different proof systems; for example, a multi-conclusion system for intuitionistic logic and several focusing proof systems. The last contribution of this thesis investigates what type of algorithms can be expressed by using linear logic's non-canonical exponentials. In particular, we use different exponentials to