Campus Event Calendar
Event Entry
What and Who
Herbrand Sequent Extraction
Bruno Woltzenlogel Paleo
IMPRS-CS
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 2 July 2007
09:00
240 Minutes
E1 4
024
Saarbrücken
Abstract
In automated deduction and automated proof transformation, one frequently deals with formal proofs that are not easily readable or understandable by humans. Two factors contributing to this problem are: 1) that real formal proofs are usually big; 2) that they are full of trivial (structural) inference steps. The key inference steps, of interest to the human reader, are thus hidden in the middle of the proof. In this work we provide solutions for this problem in the case of proofs in sequent caclulus LK for classical first-order logic. We analyze three pre-existing algorithms and we improve them by designing a fourth algorithm. The essential idea behind all four algorithms is the extraction of a Herbrand Sequent, which will shortly contain information about instantiations of quantified variables in the proof. In first-order logic, these instantiations correspond to the crucial and creative inference steps. Therefore, the extracted Herbrand Sequent summarizes the interesting content of the proof.
Contact
IMPRS
225
--email hidden
passcode not visible
logged in users only
Jennifer Gerling, 06/29/2007 13:50
Lourdes Lara-Tapia, 06/27/2007 15:35
Lourdes Lara-Tapia, 06/18/2007 16:01 -- Created document.
Lourdes Lara-Tapia, 06/27/2007 15:35
Lourdes Lara-Tapia, 06/18/2007 16:01 -- Created document.