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 [18] or the work of Manna and Waldinger [11], 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 [16] and to Assumption-Based Truth Maintenance [1].
http://i.stanford.edu/pub/cstr/reports/cs/tr/85/1035/CS-TR-85-1035.pdf