This report describes DECLARE, a prototype implementation of a declarative proof system for simple higher order logic. The purpose of DECLARE is to explore mechanisms of specification and proof that may be incorporated into toher theorem provers. It has been developed to aid with reasoning about operational descriptions of systems and languages. Proofs in DECLARE are expressed as proof outlines, in a language that approximates written mathematics. The proof language includes specialised constructs for (co-)inductive types and relations. The system includes an abstract/article mechanism that provides a way of isolating the process of formalization from what results, and simultaneously allow the efficient separate processing of work units. After describing the system we discuss our approach to two subsidiary issues: automation and the interactive environment provided to the user.

PostScript file

Details