Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Proof Representations for Higher Order Logic
Christine Rizkallah
IMPRS-CS
Master Seminar Talk
IMPRS-CS Master Student
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 12 January 2009
12:00
60 Minutes
E1 4
024
Saarbrücken
Abstract
Jitpro is an interactive theorem prover for higher order logic that outputs tableau proofs. Holitmus is a proof checker which takes as input claims and corresponding proof terms.
My task is to build an algorithm that translates tableau proofs into proof terms. This allows us to use Holitmus for checking the proofs outputted by Jitpro.
In my first talk I will give a quick overview on refutation calculus and on the proof term calculus that we are using. Then, explain how we want to give the translation.
My task is to build an algorithm that translates tableau proofs into proof terms. This allows us to use Holitmus for checking the proofs outputted by Jitpro.
In my first talk I will give a quick overview on refutation calculus and on the proof term calculus that we are using. Then, explain how we want to give the translation.
Contact
Stephanie Jörg
0681 93 25 225
--email hidden
passcode not visible
logged in users only
Stephanie Jörg, 01/12/2009 08:45
Stephanie Jörg, 01/09/2009 13:10 -- Created document.
Stephanie Jörg, 01/09/2009 13:10 -- Created document.