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).
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
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
Postscript (96k), or
This page's URL is /~black/Papers/tphol98a.html
Wed Jul 10 10:27:35 2002
by Paul E. Black
Black's papers or
NIST home page.