Abstract

I shall discuss two kinds of sequent calculus: "contraction-free" calculi and "permutation-free" calculi, emphasising the former's suitability for solving decision problems and the latter's suitability for proof search (as in logic programming).

The former have been investigated by Hudelmaier, myself and several others; I report mainly on recent work (joint with Sara Negri) showing how their completeness may (in some cases) be proven by rather routine methods allowing extension with quantifiers or non-logical notions like apartness. The motivation here is not for solution of decision problems but that such calculi have such constrained proofs that some meta-theory, like conservativity theorems, is simplified. An example is given, however, of a terminating contraction-free calculus for (propositional) Godel-Dummett logic, with all rules invertible, where less routine methods still seem preferable.

The latter kinds of calculus are based on work of Herbelin, and have the property that the proofs are in 1-1 correspondence with normal natural deductions. I discuss some recent work (joint with Luis Pinto) extending the ideas to dependent type theory.