Proof construction is a pervasive activity in computing mathematics. Although techniques for automated reasoning made it possible to prove theorems with extreme rigor, much the past effort has been directed towards proving difficult, interesting, and often well-known theorems using general- purpose logics and proof techniques. The application of automated reasoning technology to support formal methods in software engineering has fallen well short of original expectations. The main reason for this failure is the overriding emphasis on automatic theorem proving. A completely new approach is required where the focus must from theorems to proofs, and from general-purpose language inference mechanisms to well-integrated, domain-specific mechanisms. Any sufficiently rich application domain, such hardware, real-time, concurrent, or fault-tolerant systems, exploits a host of specialized formalisms in order to encode important concepts and methods and to reduce complexity. project develops multi-modal framework for interactive proof construction to support the use of domain-specific formalisms. The envisaged application is to reason about complex digital systems.
