Report Number: CS-TR-85-1035
Institution: Stanford University, Department of Computer Science
Title: RESIDUE: a deductive approach to design synthesis
Author: Finger, J. J.
Author: Genesereth, Michael R.
Date: January 1985
Abstract: We present a new approach to deductive design synthesis, the
Residue Approach, in which designs are represented as sets of
constraints. Previous approaches, such as PROLOG  or the
work of Manna and Waldinger , express designs as bindings
on single terms. We give a complete and sound procedure for
finding sets of propositions constituting a legal design. The
size of the search space of the procedure and the advantages
and disadvantages of the Residue Approach are analysed. In
particular we show how Residue can avoid backtracking caused
by making design decisions of overly coarse granularity. In
contrast, it is awkward for the single term approaches to do
the same. In addition we give a rule for constraint
propagation in deductive synthesis, and show its use in
pruning the design space. Finally, Residue is related to
other work, in particular, to Default Logic  and to
Assumption-Based Truth Maintenance .