AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

Proofs are more than just validations of theorems; they can contain
interesting mathematical information like bounds or algorithms. However
this information is frequently hidden and proof transformations are
required to make it explicit. One such transformation on proofs in
sequent calculus is cut-elimination (i.e. the removal of lemmas in
formal proofs to obtain proofs made essentially of the syntactic
material of the theorem). In his famous paper ``Untersuchungen ueber das
logische Schliessen'' Gentzen showed that for cut-free proofs of prenex
end-sequents Herbrand's theorem can be realized via the midsequent
theorem. In fact Gentzen defined a transformation which, given a
cut-free proof p of a prenex sequent S, constructs a cut-free proof p'
of a sequent S' (a so-called Herbrand sequent) which is propositionally
valid and is obtained by instantiating the quantifiers in S. These
instantiations may contain interesting and compact information on the
validity of S. Generally, the construction of Herbrand sequents
requires cut-elimination in a given proof p (or at least the elimination
of quantified cuts). The method CERES (cut-elimination by resolution)
provides an algorithmic tool to compute a Herbrand sequent S' from a
proof p (with cuts) of S even without constructing a cut-free version of
p. A prominent and crucial principle in mathematical proofs is
mathematical induction. However, in proofs with mathematical induction
Herbrand's theorem typically fails. To overcome this problem we replace
induction by recursive definitions and proofs by proof schemata. An
extension of CERES to proof schemata (CERESs) allows to compute
inductive definitions of Herbrand expansions (so-called Herbrand
systems) representing infinite sequences of Herbrand sequents, resulting
in a form of Herbrand's theorem for inductive proofs.

Jennifer Müller

2900

--email hidden

passcode not visible

logged in users only