Subject: Structured Metatheory and Inductive Definitions
Jour: 22/09/98 (Mardi 22 septembre)

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                    Salle de confe'rence du batiment 11

                          Mardi 22 septembre, 10h30


                            -------------------
                               David Basin
                            -------------------

                     Albert-Ludwigs-Universitaet Freiburg
                                      

        ============================================================
                Structured Metatheory and Inductive Definitions
        ============================================================


 We examine a problem for machine supported metatheory. There are
statements true about a theory that are true of some (but only some)
extensions; however standard theory-structuring facilities do not
support selective inheritance.  Using an example of metatheory for modal
logics, we show how a statement about a theory can explicitly formalize
the closure conditions that extensions should satisfy for it to remain true.
We show how metatheories based on inductive definitions allow theories
and general metatheorems to be organized hierarchically this way, and
report on a case study using both Feferman's FS0 and parameterized inductive
definitions in higher-order logic.

(Work is joint work with Sean Matthews, MPI Saarbruecken.)