Abstract
A dialogue algorithm is described that executes Prolog-style rules in an attempt to achieve a goal. The algorithm selects paths in the proof in an attempt to achieve success and proves subgoals on the basis of internally available information where possible. Where “missing axioms” are discovered, the algorithm interacts with the user to solve subgoals, and it uses the received information from the user to attempt to complete the proof. A multimedia grammar codes messages sent to and received from the user into a combination of speech, text, and voice tokens.This theory is the result of a series of dialogue projects implemented in our laboratory. These will be described including statistics that measure their levels of success.