The last few years has seen a dramatic growth of interest in the application of computer-aided interactive proof checking. The technology underlying interactive proof checking has improved as a result of developments in theorem proving and model checking. There is also a growing awareness of the risks of digital hardware and software systems, the increasing complexity of these systems, and the greater exposure to security threats. Interactive proof checking is still not an effective tool in the hands of nonspecialists because of the lack of insightful explanations from both failed and successful proof attempts. The main problem addressed by this project is that of reconciling the development and maintenance of proofs with the presentation of proofs. The main thesis of this project is that powerful, appropriate, and transparent automation can improve the productivity of proof construction and maintenance while enhancing the value and cogency of the resulting proofs and counterexamples. The project will result in the transparent inference procedures, structured and readable proof presentations, and automated support for counterexample generation.
