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.''