and D. Basin S. Matthews Max-Planck-Institut fur Informatik, Im Stadtwald, D-66123 Saarbrucken, Germany
Generic proof systems like
Isabelleprovide 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. Computer assisted proof, logical frameworks, metatheoretic extensibility, second-order logic, proof theory.
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Last updated 08 Jan 97
Part of the OUP Journals World Wide Web service.
Copyright Oxford University Press, 1997