Date: Wed, 03 Nov 2004 12:27:22 -0600
From: Jared Davis
Subject: ACL2 Meeting Today


Hi,

At today's meeting, I will give a practice run of my talk on finite 
set theory for the ACL2 workshop.  Last february I talked during the 
meeting about the same topic, and it took 3 meetings for me to finish. 
  This time, the talk will only take 30 minutes (to fit the 
constraints for the workshop), and as a result it will be much less 
involved.

After the practice talk, if there is interest, I'd like to discuss 
some new extensions to the library.  These include an instantiable 
theory of quantification of predicates over sets, filtering sets based 
on predicates, and mapping functions over sets.  (Incidentally, 
similar theories are available for lists.)  Using these theories, I'll 
show you a very preliminary graph theory model written in the style of 
"higher order" programming within an ACL2 context.  I hope to convince 
you that despite the huge difficulties in developing these 
instantiable theories, there is great promise in this sort of approach 
for being able to develop models quickly.

Hope to see you there,

    Jared