Volume 6: January - December 1996

Issue 6: December 1996


Adding metatheoretic facilities to first-order theories

  • Adding metatheoretic facilities to first-order theories
  • D. Basin and S. Matthews Max-Planck-Institut fur Informatik, Im Stadtwald, D-66123 Saarbrucken, Germany


    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.

    Keywords: Computer assisted proof, logical frameworks, metatheoretic extensibility, second-order logic, proof theory.

    Pages: 835 - 849

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    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