Adding metatheoretic facilities to first-order theories
David Basin · Journal of Logic and Computation · 1996
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.