Paul E. Black and Phillip J. Windley, Automatically Synthesized Term Denotation Predicates: A Proof Aid, 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.

Abstract:

    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 PDF (170k).

This page's URL is /~black/Papers/hol95.html

Updated Wed Jul 10 10:26:46 2002

Go to Black's papers or NIST home page.