@TechReport{Blackburn:1998,
      AUTHOR = {Blackburn, Patrick},
      TITLE = {Internalizing Labeled Deduction},
      YEAR = {1998},
      MONTH = {November},
      NUMBER = {102},
      PAGES = {39},
      ADDRESS = {Saarbrücken},
      TYPE = {CLAUS-Report},
      INSTITUTION = {Universität des Saarlandes},
      URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus102.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus102.dvi},
      ABSTRACT = {This paper shows how to internalize the Kripke satisfaction definition using labeled modal languages and explores the proof theoretic consequences of this. As we shall see, using labeled modal languages enables us to transfer classic Gabbay-style labeled deduction from the metalanguage to the object language, and to handle the required labeling discipline purely logically. Moreover, internalized labeled deduction links neatly with the Gabbay-style rules now widely used in modal Hilbert-systems, completeness results for a wide range of first-order definable frame classes can be obtained automatically, and the method extends straightforwardly to richer languages. The paper discusses related work by Jerry Seligman and Miroslava Tzakova and concludes with some reflections on the status of labeling in modal logic.},
      ANNOTE = {COLIURL : Blackburn:1998:ILD.pdf Blackburn:1998:ILD.ps Blackburn:1998:ILD.dvi}
}