Title:  An Entertaining Puzzle
Speaker:  J Moore

Abstract: Suppose you are given two bottles, one measuring
exactly 5 gallons and the other exactly 3.  Can you measure
out exactly 1 gallon?  Generalize the problem to two bottles
of arbitrary size.  Can you measure out 1 gallon?  In this
talk I will describe how I formalized this problem in ACL2
and proved several interesting theorems about ``the bottle
problem.''