The aim of this research project is to increase the benefits and to reduce the costs of automated reasoning across a wide variety of applications. The project both supports and derives motivation from the ongoing development of the Larch Prover (LP), an interactive proof assistant for multisorted first order logic. Experience with previous versions of LP suggests four important ways to improve the cost/benefit ratio: reducing the amount of detail required in proofs, supporting modular descriptions of theories and proofs, closing the gap between the logical and operational meaning of theories, and integrating LP into applications. To reduce the amount of detail required in proofs, the project seeks to combine different reasoning techniques in seamless and efficient ways. Early versions of LP emphasized equational term-rewriting. A recent version reduced the length of many proofs by using cooperating decision procedures for the theory of equality and for linear arithmetic. The project is exploring fruitful interactions between equational term-rewriting and decision procedures. The project is addressing both logical and operational issues for using independently developed logical modules in larger proofs and for ensuring that proof scripts are replayable after changes to formalizations. For almost all applications of automated reasoning, there is an unavoidable gap between logical content (e.g., the consequences of a specification) and operational content (e.g., the proof techniques and/or sequence of lemmas required to prove a particular consequence). The project is studying how to narrow this gap, where possible, and how to provide useful information about the nature of the gap, particularly when proofs fail. Finally, the project is seeking to improve the cost/benefit ratio for formal reasoning by integrating LP into applications. The goals of tighter integration are to enable users to think in application-specific terms, to make LP work better in the context of particular applications, and to understand the interface reasoning tools should present to applications. The project is seeking to achieve tighter integration by eliminating the need for transcribing designs and by developing application specific improvements in LP's expressive and deductive power (e.g., for reasoning about probability).
