Paul E. Black and Phillip J. Windley,
Automatically Synthesized Term Denotation Predicates: A Proof
Higher Order Logic Theorem Proving and Its Applications (HOL '95),
Aspen Grove, Utah, USA (September 1995),
edited by E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss,
Springer-Verlag, Berlin, Germany, 1995, pages 46-57.
In goal-directed proofs, such as those used in HOL, tactics often must
operate on one or more specific assumptions. But goals often have
many assumptions. Currently there is no good way to select or denote
assumptions in HOL88. Most mechanisms are sensitive to
inconsequential changes or are difficult to use.
Denoting assumptions by filters (matching) makes it easier to maintain
large proofs and reuse pieces. But writing the filter predicate can
be time-consuming and distracting.
We describe an aid to proof building which synthesizes filter functions
from terms. Given examples of terms which should and should not be
matched, the function creates an ML predicate which can be used, for
example, with filter or FILTER_ASM_REWRITE_TAC.
This paper reviews past discussions on denotation methods, the design
and implementation of the filter synthesizer, applicable AI
classification techniques, and possible application to more general
term handling and recognition.
Get the paper in
Postscript (120k) or
This page's URL is /~black/Papers/hol95.html
Wed Jul 10 10:26:46 2002
by Paul E. Black
Black's papers or
NIST home page.