Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Adding Metatheoretic facilities to First-order Theories

MPG-Autoren
/persons/resource/persons44075

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

/persons/resource/persons45002

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

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Basin, D. A., & Matthews, S. (1996). Adding Metatheoretic facilities to First-order Theories. Journal of Logic and Computation, 6(6), 835-849. doi:10.1093/logcom/6.6.835.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-ABC1-8
Zusammenfassung
Generic proof systems like Isabelle provide some limited
but useful metatheoretic facilities for declared logics;
in particular, users can prove simple derived rules
and also `solve' formulae that contain metavariables - a
technique useful for program synthesis. We show how an
arbitrary first-order theory can be conservatively extended
to provide similar facilities, without a supporting
metatheory, and examine what the limitations of this
approach are.