Date: Wed, 5 Jul 2006 08:36:29 -0500
From: Sandip Ray

Greetings, 

Sorry for the delay in sending out the abstract.  There will be an ACl2 meeting
today at the usual time and place. I will be talking and I will present some
proofs showing how certain general forms of recursive defining equations can be
admitted to the ACL2 logic. I think the talk will be short, so there should be
plenty of time for round-table discussions.

Here is an abstract for the talk.

There has been several recent work in ACL2 showing that certain forms of
recursive equations can be uniformly introduced in the logic. The work started
arguably with the so-called "defpun" work by Manolios and Moore in 2000, which
showed that tail-recursive defining equations can be always introduced in the
logic. Their results have since been extended by others, most notably Cowles
and Gamboa, with more general forms of defining equations. I will consider a
certain form of generic recursive equations and present a sufficient condition
under which they can be introduced in the logic. The proof of this
admissibility has parallels with Manolios and Moore's proof and I will discuss
the connection between the two forms of equations.

This is joint work with J Strother Moore.

Again, I apologize for the delay.

--- Sandip.