
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 / higherorder 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 (higherorder logic and set theory). Isabelle's representation of logic is inAEuenced by logic programming: its ?logical variables? can be used to implement stepwise 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), SpringerVerlag.