Tool Support for Logics of Programs

Lawrence C. Paulson

Computer Laboratory, University of Cambridge

November 1996

Key words: proof tools / generic reasoning / logic programming / logical variables / uniocation / Isabelle / higher-order logic / set theory / inductive deonitions / cryptographic protocols

Summary. Proof tools must be well designed if they are to be more eoeective than pen and paper. Isabelle supports a range of formalisms, two of which are described (higher-order logic and set theory). Isabelle's representation of logic is inAEuenced by logic programming: its ?logical variables? can be used to implement step-wise reonement. Its automatic proof procedures are based on search primitives that are directly available to users. While emphasizing basic concepts, the article also discusses applications such as an approach to the analysis of security protocols.

To appear in the proceedings Mathematical Methods in Program Development (Summer School Marktoberdorf 1996), Springer-Verlag.