The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #557

Title:Synthesizing Hardware: Configuration Via Proof
Date:Nov 1991
Presented:Submitted to CADE-92
Abstract:Configuring large computer hardware systems is a complex task and efforts to automate it have spawned knowledge based systems which have proved difficult to maintain. This paper describes a logical formalism for configuration and the use of a proofs as configurations approach analogous to program synthesis via proofs as programs. Meta-level control is achieved through proof plans, which embody common strategies for guiding inference. As well as ensuring soundness, in that only legal configurations can be synthesized, the system also facilitates maintenance because of its clean separation of object-level knowledge, heuristics, and control strategies.

[Search These Pages] [DAI Home Page] [Comment]