Greetings [and apologies if you get multiple copies]: The fifth ACL2 Workshop will be held November 18-19, 2004, in Austin Texas, USA, in conjunction with (and immediately following) FMCAD. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend. ACL2 is a state-of-the-art automated reasoning system, which grew out of the Boyer-Moore theorem prover and has been used successfully on a number of industrial and academic projects. ACL2 is described at http://www.cs.utexas.edu/users/moore/acl2. The ACL2 workshops provide a forum for the presentation and discussion of projects using ACL2 as well as the evolution of the tool. For more information, including a schedule of talks and general information (including registration, which costs less prior to October 15, and lodging), see: http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/ Regards, Matt Kaufmann and J Moore (Organizing Committee)