Open Architectures for Formal Reasoning and Deductive Technologies for Software Development

摘要

The objective of the first project is to develop an open architecture for formal reasoning systems. One goal is to provide a framework with a clear semantic basis for specification and instantiation of generic components; construction of complex systems by interconnecting components; and for making incremental improvements and tailoring to specific applications. Another goal is to develop methods for specifying component interfaces and interactions to facilitate use of existing and newly built systems as 'off the shelf' components, thus helping bridge the gap between producers and consumers of reasoning systems. In this report we summarize results in several areas: our data base of reasoning systems; a theory of binding structures; a theory of components of open systems; a framework for specifying components of open reasoning system; and an analysis of the integration of rewriting and linear arithmetic modules in Boyer-Moore using the above framework. For Deductive Technology for Software Development, research concentrated on automated and temporal deduction. We developed inferences to rules to achieve abbreviated proofs in theories possessing certain monotonicity properties, such as transitivity and substitutivity. These rules are extensions of the relation replacement and relation matching rules. We developed a deductive system for predicate temporal logic with induction. This deductive system is relatively complete. Program synthesis is the systematic derivation of a computer program to meet a given specification. Here the specification is a general description of the purpose of the desired program, while the program is a detailed description of a method for achieving that purpose. The particular emphasis of this project is on the development of deductive techniques, i.e., techniques based on theorem proving, for program synthesis. These techniques are amenable to automatic implementation, but may be used interactively or for the formal explination of informal derivations discovered by hand.