
\begin{comment}

Abstract for this week's ACL2 talk

Hi,

At this week's ACL2 meeting, I'll talk about some improvements that Sol Swords
and I made to the UBDD library over the summer.

UBDDs are a canonical way to represent Boolean functions introduced by Warren
Hunt and Bob Boyer.  The core UBDD operations only take up a couple of pages to
define, but when memoized they produce a fairly efficient BDD package.  Today,
UBDDs are used extensively at Centaur: they are an integral part of the "G"
system (both the current version and Sol's "GL" revision); they are also a
fundamental part of the hardware description language, E, which our analysis is
based on.

A good part of the talk will have little to do with UBDDs, but instead will be
about the supporting utilities that we have come up with.  These include:

   (1) a better alternative to deftheory, 
   (2) an automatic tool for introducing "flag" functions for mutual-recursion,
   (3) a generalization clause processor which can be useful for computed hints,
       and 
   (4) an optimization called "opportunistic laziness" which may be useful in 
       improving the efficiency of your functions

All of these are lightly used in our new version of the UBDD library, and they
are all publically available via the acl2-books repository.

The remainder of the talk will be about some new approaches we have developed
for reasoning about UBDDs.  These techniques center around the isomorphism
between a Boolean function and the set of vectors which satisfy it.  That is,
we can transform the question of whether ``f = g'' into ``f(v) = g(v) for an
arbitrary v.''  This allows us to avoid dealing with the peculiar structure of
UBDDs, and instead reason about them abstractly.  

We have developed some elaborate techniques (computed hints, clause processors,
or hints, etc.) that allow us to effectively, automatically use this approach.
As a result, we have been able to eliminate many lemmas and hints from some
previously-accomplished UBDD proofs.  Also, Sol is now using our most advanced
approach in his GL work, and it is successfully proving hundreds (thousands?)
of subgoals automatically.

Jared

\end{comment}
