非表示:
キーワード:
-
要旨:
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.
