de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

A practical implementation of simple consequence relations using inductive definitions

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45002

Matthews,  Seán
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Matthews, S. (1997). A practical implementation of simple consequence relations using inductive definitions. In W. McCune (Ed.), Proceedings of the 14th International Conference on Automated Deduction (CADE-14) (pp. 306-320). Berlin, Germany: Springer.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-39D0-9
Zusammenfassung
Logical frameworks such as the Edinburgh LF or Isabelle are not suitable for general metatheory, since they do not allow induction. On the other hand it is hard to encode a logic in an inductive definition-style framework so that it is usable for object theory. We propose a solution to this problem that borrows techniques from the type-theory tradition of logical frameworks for use with a language of inductive definitions, providing us with a notation suitable for practical object and metatheory both.