[Club2] 01.03.06 !!!!Raum: John von Neumann!!!

[Norbert Schirmer]

Diese Woche,

Mittwoch, 01.03.2006, 15.00 Uhr, im Raum: John v. Neumann  00.11.038

   Makarius:

 Titel: Natural Deduction vs. Natural Induction in Isabelle/Isar

  Abstract:

  In theory, induction is a trivial instance of generic natural deduction 
as represented in the Isabelle/Pure framework.  In practice, there is a 
big difference for complex induction proofs, involving local parameters, 
local premises, local definitions, simultaneous goals and mutual rules 
etc. Traditionally such structure has been encoded within the 
object-logic, and the extra burden imposed here was accepted as a feature 
of tactical theorem proving.  In structured proofs, on the other hand, any 
formal noise that is not part of the actual application is immediately 
exposed in the text -- both the readers and writers will rightly complain.  
We discuss the present version of the "induct" method of Isabelle/Isar, 
which makes complex induction appear as a natural element of structured 
natural deduction.


    Norbert