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

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Metalogical frameworks

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

Basin,  David
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

MPI-I-92-205.pdf
(beliebiger Volltext), 162KB

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

Basin, D., & Constable, R. L.(1992). Metalogical frameworks (MPI-I-92-205). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-B1B4-A
Zusammenfassung
In computer science we speak of implementing a logic; this is done in a programming language, such as Lisp, called here the implementation language. We also reason about the logic, as in understanding how to search for proofs; these arguments are expressed in the metalanguage and conducted in the metalogic of the object language being implemented. We also reason about the implementation itself, say to know it is correct; this is done in a programming logic. How do all these logics relate? This paperconsiders that question and more. We show that by taking the view that the metalogic is primary, these other parts are related in standard ways. The metalogic should be suitably rich so that the object logic can be presented as an abstract data type, and it must be suitably computational (or constructive) so that an instance of that type is an implementation. The data type abstractly encodes all that is relevant for metareasoning, i.e., not only the term constructing functions but also the principles for reasoning about terms and computing with them. Our work can also be seen as an approach to the task of finding a generic way to present logics and their implementations, which is for example the goal of the Edinburgh Logical Frameworks (ELF) effort. This approach extends well beyond proof-construction and includes computational metatheory as well.