Paul E. Black and Phillip J. Windley, Some Theorem Proving Aids, in Theorem Proving in Higher Order Logics: Emerging Trends, Supplemental Proceedings of The 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98), edited by Jim Grundy and Malcolm Newey, pages 19-30, Joint Computer Science TR 98-08, The Australian National University, Canberra, Australia (September 1998).

Abstract:

    Theorem proving can be a very useful formal method. However it currently takes a lot of time and study to learn how to use a theorem prover, and proving even apparently simple theorems can be tedious. Theorem proving, and its benefits in software and hardware development, should be accepted more readily and widely if new users can do larger proofs of more complete models earlier in their training and with less work.

    We present some generally applicable tools which we found helpful in formally verifying a secure web server. The first is a program to check goals for common mistakes arising indirectly from type inference. We also give tactics, or proof advancing routines, to simplify goals and handle assumptions. Finally we give tactics which prove goals by selecting assumptions to establish the goal or find a contradiction. These are another step to making theorem proving easier, increasing productive, and reducing unnecessary complication.

Get the paper in DVI (41k), Postscript (96k), or PDF (161k).

This page's URL is /~black/Papers/tphol98a.html

Updated Wed Jul 10 10:27:35 2002

Go to Black's papers or NIST home page.