Note: |
|
(LaTeX) Abstract: |
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. |
URL for the Abstract: |
|
Categories,
Keywords: |
automatic programming, formal logic, theorem proving, metatheoretic facilities, first-order theories, generic proof systems, Isabelle, declared logics, derived rules, formula solving, metavariables, program synthesis, conservative extension, computer-assisted proof, logical frameworks, second-order logic |
HyperLinks / References / URLs: |
|
Copyright Message: |
|
Personal Comments: |
|
Download
Access Level: |
|
|