max planck institut

informatik

informatik

<< Previous Entry | Next Entry >> | New Event Entry | Edit this Entry | Login to DB (to update, delete) |

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 |

Language: | English |

Date: | Wednesday, 31 July 2019 |
---|---|

Time: | 11:00 |

Duration: | 60 Minutes |

Location: | Saarbrücken |

Building: | E1 4 |

Room: | 024 |

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 |
---|---|

Phone: | 2900 |

EMail: | --email address not disclosed on the web |

Video Broadcast: | No | To Location: |
---|

Note: | |
---|---|

Attachments, File(s): |

- Jennifer Müller, 07/24/2019 02:25 PM -- Created document.