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.