Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Algorithmic Analysis of Proofs via CERES
Speaker:Alexander Leitsch
coming from:TU Wien
Speakers Bio:
Event Type:Talk
Visibility:D1, D2, D3, INET, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 31 July 2019
Duration:60 Minutes
Building:E1 4
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.
Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Jennifer Müller, 07/24/2019 02:25 PM -- Created document.