RESIDUE: A Deductive Approach to Design

J. J. Finger and Michael R. Genesereth Computer Science Department Stanford University, Stanford, California 94305 1. Introduction Automatic theorem proving methods, such as resolution or backwards-chaining, arc useful for verifying the correctness of a pre-cxisting design, but how might we use theorem proving methods to both generate and verify a design?