In order to improve the technology of implementing database systems, a mechanical reasoning capability needed to help database systems implementers achieve high efficiency in advanced database systems is developed. Mechanical reasoners are to be used by implementation designers as they map high level database system specifications, in the ADABTPL specification language, into implementation systems such as the University of Wisconsin's EXODUS. The project involves the definition of a formal data transformation language for specifying the semantics of data structures in terms of high level concepts, developing heuristic methods useful to a database implementation designer transforming specifications into implementations, and devising techniques for supplying details missing in incomplete internal schemas. Systems that will benefit from the new technology include design, graphics, control and knowledge based systems.
