Date: Tue, 14 Sep 2004 10:11:51 -0500
From: J Strother Moore
Subject: ACL2 seminar


In this week's seminar I will give a presentation of exploratory work on
the use of second-order pattern matching to automate functional instantiation.

The talk will start with a brief sketch of functional instantiation.  Like
ordinary instantiation, functional instantiation is a way to derive a new
theorem from an old one by replacing certain symbols by new things.  But
while ordinary instantiation replaces variables by terms, functional
instantiation replaces function symbols by functional expressions.  This is
sound only if the replacements satisfy the same axioms (constraints) as the
replaced symbols.  We'll go through that quickly.

Then I'll just illustrate the Huet-Lang second-order matching algorithm which
is a way to decide the question "Is there an instantiation of this term that
produces that term?"  I won't give the algorithm but just illustrate its
use in several ACL2 examples.

Second-order matching typically produces multiple winning substitutions.

To automate functional instantiation, then, we use second-order matching to
compute some syntactic solutions.  Then we choose between them for the most
likely winners.  Different winners typically produce different constraint
problems.  So, next, for each such winner, we set up a theorem proving
problem to try to establish the constraints.  I'll show examples of
prototypical code supporting this.

But that only brings me to the crux of the problem: how can ACL2 support the
exploration of a disjunction of goals?  That is, we need a version of ACL2
that will undertake to prove this constraint or that constraint or this other
constraint, when each proof attempt may generate more such and/or splits.  So
we need to generalize ACL2's proof orchestration mechanism -- "the waterfall"
-- to support and/or trees.  I'll briefly describe the waterfall, sketch my
thoughts, and solicit yours.