##### Document Text Contents

Page 1

HOL Light Tutorial (for version 2.10)

John Harrison

Intel JF1-13

[email protected]

December 14, 2005

Abstract

The HOL Light theorem prover can be difficult to get started with. While

the manual is fairly detailed and comprehensive, the large amount of background

information that has to be absorbed before the user can do anything interesting is

intimidating. Here we give an alternative ‘quick start’ guide, aimed at teaching

basic use of the system quickly by means of a graded set of examples. Some

readers may find it easier to absorb; those who do not are referred after all to the

standard manual.

“Shouldn’t we read the instructions?”

“Do I look like a sissy?”

Calvin & Hobbes, 19th April 1988

1

Page 2

Contents

1 Installation 5

1.1 Cygwin . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.2 OCaml . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.3 HOL Light . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.4 Checkpointing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

1.5 Other versions of HOL . . . . . . . . . . . . . . . . . . . . . . . . . 9

2 OCaml toplevel basics 10

3 HOL basics 12

3.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

3.2 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

3.3 Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14

3.4 Derived rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16

4 Propositional logic 17

4.1 Proving tautologies . . . . . . . . . . . . . . . . . . . . . . . . . . .19

4.2 Low-level logical rules . . . . . . . . . . . . . . . . . . . . . . . . . 21

4.3 Logic design and veri�cation . . . . . . . . . . . . . . . . . . . . . . 22

5 Equations and functions 24

5.1 Curried functions . . . . . . . . . . . . . . . . . . . . . . . . . . . .26

5.2 Pairing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

5.3 Equational reasoning . . . . . . . . . . . . . . . . . . . . . . . . . .28

5.4 De�nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

6 Abstractions and quanti�ers 31

6.1 Quanti�ers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

6.2 First-order reasoning . . . . . . . . . . . . . . . . . . . . . . . . . .35

7 Conversions and rewriting 37

7.1 Conversionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .38

7.2 Depth conversions . . . . . . . . . . . . . . . . . . . . . . . . . . . .39

7.3 Matching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

7.4 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

8 Tactics and tacticals 44

8.1 The goalstack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .45

8.2 Inductive proofs about summations . . . . . . . . . . . . . . . . . . .52

9 HOL’s number systems 54

9.1 Arithmetical decision procedures . . . . . . . . . . . . . . . . . . . .56

9.2 Nonlinear reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . .58

9.3 Quanti�er elimination . . . . . . . . . . . . . . . . . . . . . . . . . . 61

2

Page 115

In addition,wp must distribute over conjunction and disjunction. The former must

hold even for a nondeterministic programming language, but for the latter determinism

is essential:

let WP_DISJUNCTIVE = prove

(‘(wp c p) UNION (wp c q) = wp c (p UNION q)‘,

REWRITE_TAC[FUN_EQ_THM; IN; wp; wlp; IN_ELIM_THM; UNION; terminates] THEN

MESON_TAC[DETERMINISM]);;

One can obtain explicit expressions for the weakest preconditions of commands.

For example, attractively, the weakest precondition of a sequence of commands is just

the composition of the two weakest preconditions of the components:

let WP_SEQ = prove

(‘!c1 c2 q. wp (c1 ;; c2) = wp c1 o wp c2‘,

REWRITE_TAC[wp; wlp; terminates; FUN_EQ_THM; o_THM] THEN REPEAT GEN_TAC THEN

GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [sem_CASES] THEN

REWRITE_TAC[injectivity "command"; distinctness "command"] THEN

MESON_TAC[DETERMINISM]);;

16.4 Axiomatic semantics

We can now return to the prototypical programming problem. We are supposed to

produce a programc guaranteeing some predicateq on the output state given an as-

sumptionp on the input state. We can say that a command is a valid solution to this

problem precisely if the input predicatep is contained in the weakest precondition for

q:

let correct = new_definition

‘correct p c q <=> p SUBSET (wp c q)‘;;

This leads us to yet another approach to the semantics of programming languages,

developed by Hoare (1969) from related work by Floyd (1967). Rather than aim at

explicit statements about the state transition relations resulting from commands, we

simply state rules that allow us to deduce valid ‘Hoare triples’correct p c q ,

more usually written informally asp {c} q or {p} c {q}. We can derive a suitable set

of rules directly from our existing semantic definitions, rather than postulate them from

scratch. Two of the simplest rules areprecondition strengthening(we can assume a

stronger precondition than necessary) andpostcondition weakening(we will guarantee

a weaker postconditon than any that we can deduce):

let CORRECT_PRESTRENGTH = prove

(‘!p p’ c q. p SUBSET p’ /\ correct p’ c q ==> correct p c q‘,

REWRITE_TAC[correct; SUBSET_TRANS]);;

let CORRECT_POSTWEAK = prove

(‘!p c q q’. correct p c q’ /\ q’ SUBSET q ==> correct p c q‘,

REWRITE_TAC[correct] THEN MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;

Similarly, we can quite easily derive the usual Hoare rule for sequences:

let CORRECT_SEQ = prove

(‘!p q r c1 c2.

correct p c1 r /\ correct r c2 q ==> correct p (c1 ;; c2) q‘,

REWRITE_TAC[correct; WP_SEQ; o_THM] THEN

MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;

115

Page 116

We will develop these ideas more in the next section in a slightly different context.

17 Shallow embedding

In the previous section we explicitly de�ned the syntax of a programming language

and its semantic map within HOL. The syntactic constructs and their meanings were

quite different things, with the semantic map mediating between them. A contrasting

approach is to regard a programming language as merely a notation for describing that

semantics directly. For example, an assignment statement x := e does not denote

a syntactic object, but rather is a shorthand for, say, a state mapping, state transition

relation or weakest precondition that we associate with it.

This approach, and indeed the embedding of programming language semantics in

theorem provers generally, was pioneered by Gordon (1989), the inventor of the orig-

inal HOL. For some time it was known as semantic embedding, and the fullblown

formalization of the semantic map as syntactic embedding. However, since Boulton,

Gordon, Gordon, Harrison, Herbert, and Van Tassel (1993) the customary terminology

has been to describe the formalization of the syntax and the semantic map (as in the

previous section) as deep embeddingand the direct semantic embedding as shallow

embedding.

It is worth noting that shallow embedding provides a natural formalization of the at-

titudes expressed by Dijkstra (1976), where a �programming language� (he deprecates

the very term) is viewed as an algorithmically-oriented system of mathematical nota-

tion �rst and foremost. Such a notation is meaningful in isolation from any particular

implementation, and indeed the role of a real programming language compiler on a real

machine is to provide a suf�ciently close approximation to the abstract mathematical

counterpart. (Perhaps, for example, imposing some limitations on sizes of integers.)

17.1 State and expressions

Crudely speaking, to move from a deep to a shallow embedding we want to keep the

same basic theorems as in the deep embedding but with the semantic maps value and

sem erased. Expressions are now simply mappings from states to values. Commands

are just their weakest preconditions. (We could use various other direct semantic no-

tions, but this one �ts best with our future plans � see Dijkstra and Scholten (1990)

for some discussion of this point.)

The syntax of expressions in our deep-embedded language was somewhat restricted:

we only had one type, that of natural numbers, and we had to consider it as a Boolean

using C-style hacking. These restrictions were mainly for technical simplicity: we

could have considered a much wider variety of types and operators. But then the

statements and proofs, while still straightforward conceptually, begin to suffer from

a proliferation of cases. In a shallow embedding, there’s nothing to stop us using quite

arbitrary HOL expressions, even noncomputable ones, and we never need to settle on a

�xed repertoire of types and operators at the outset. Of course, this has the apparently

undesirable feature that one can write ‘programs’ that do not correspond to executable

116

Page 230

Parrilo, P. (2001) Semide�nite programming relaxations for semialgebraic

problems. Available from the Web at citeseer.nj.nec.com/

parrilo01semidefinite.html .

Paulson, L. C. (1983) A higher-order implementation of rewriting. Science of Com-

puter Programming, 3, 119�149.

Paulson, L. C. (1987) Logic and computation: interactive proof with Cambridge LCF,

Volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge Uni-

versity Press.

Peres, A. (1991) Two simple proofs of the Kochen-Specker theorem. Journal of

Physics, A24, 175�178.

Ridge, T. (2005) A mechanically veri�ed, ef�cient, sound and complete theorem

prover for �rst order logic. Available via http://homepages.inf.ed.ac.

uk/s0128214/ .

Rivest, R. L., Shamir, A., and Adelman, L. M. (1978) A method for obtaining digital

signatures and public-key cryptosystems. Journal of the ACM, 21, 120�126.

Rudnicki, P. (1987) Obvious inferences. Journal of Automated Reasoning, 3, 383�393.

Rudnicki, P. (1992) An overview of the MIZAR project. Available on the Web as

http://web.cs.ualberta.ca/˜piotr/Mizar/MizarOverview.ps .

Russell, B. (1919) Introduction to mathematical philosophy. Allen & Unwin.

Scott, D. (1993) A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical

Computer Science, 121, 411�440. Annotated version of a 1969 manuscript.

Scott, D. and Strachey, C. (1971) Toward a mathematical semantics for computer lan-

guages. Programming Research Group Technical Monograph PRG-6, Oxford Univ.

Computing Lab.

Slind, K. (1991) An implementation of higher order logic. Technical Report 91-419-

03, University of Calgary Computer Science Department, 2500 University Drive N.

W., Calgary, Alberta, Canada, TN2 1N4. Author’s Masters thesis.

Slind, K. (1997) Derivation and use of induction schemes in higher-order logic. In

Gunter, E. L. and Felty, A. (eds.), Theorem Proving in Higher Order Logics: 10th

International Conference, TPHOLs'97, Volume 1275 of Lecture Notes in Computer

Science, Murray Hill, NJ, pp. ?�? Springer-Verlag.

Smullyan, R. M. (1992) Gödel's Incompleteness Theorems, Volume 19 of Oxford Logic

Guides. Oxford University Press.

Soko�owski, S. (1983) A note on tactics in LCF. Technical Report CSR-140-83, Uni-

versity of Edinburgh, Department of Computer Science.

230

Page 231

Solovay, R. M. (1976) Provability interpretations of modal logic. Israel Journal of

Mathematics, 25, 287�304.

Stickel, M. E. (1988) A Prolog Technology Theorem Prover: Implementation by an

extended Prolog compiler. Journal of Automated Reasoning, 4, 353�380.

Tarski, A. (1936) Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philo-

sophica, 1, 261�405. English translation, ‘The Concept of Truth in Formalized

Languages’, in Tarski (1956), pp. 152�278.

Tarski, A. (1955) A lattice-theoretical �xpoint theorem and its applications. Paci�c

Journal of Mathematics, 5, 285�309.

Tarski, A. (ed.) (1956) Logic, Semantics and Metamathematics. Clarendon Press.

Trybulec, A. and Blair, H. A. (1985) Computer aided reasoning. In Parikh, R. (ed.),

Logics of Programs, Volume 193 of Lecture Notes in Computer Science, Brooklyn,

pp. 406�412. Springer-Verlag.

Wiedijk, F. (2001) Mizar light for HOL Light. In Boulton, R. J. and

Jackson, P. B. (eds.), 14th International Conference on Theorem Prov-

ing in Higher Order Logics: TPHOLs 2001, Volume 2152 of Lecture

Notes in Computer Science, pp. 378�394. Springer-Verlag. Online at

http://link.springer.de/link/service/series/0558/tocs/t2152.htm .

Winskel, G. (1993) The formal semantics of programming languages: an introduction.

Foundations of computing. MIT Press.

Wos, L. (1998) Programs that offer fast, �awless, logical reasoning. Communications

of the ACM, 41(6), 87�102.

Wos, L. and Pieper, G. W. (1999) A Fascinating Country in the World of Computing:

Your Guide to Automated Reasoning. World Scienti�c.

Wright, J. v., Grundy, J., and Harrison, J. (eds.) (1996) Theorem Proving in Higher

Order Logics: 9th International Conference, TPHOLs'96, Volume 1125 of Lecture

Notes in Computer Science, Turku, Finland. Springer-Verlag.

Wright, J. v., Hekanaho, J., Luostarinen, P., and Langbacka, T. (1993) Mechanizing

some advanced re�nement concepts. Formal Methods in System Design, 3, 49�82.

231

HOL Light Tutorial (for version 2.10)

John Harrison

Intel JF1-13

[email protected]

December 14, 2005

Abstract

The HOL Light theorem prover can be difficult to get started with. While

the manual is fairly detailed and comprehensive, the large amount of background

information that has to be absorbed before the user can do anything interesting is

intimidating. Here we give an alternative ‘quick start’ guide, aimed at teaching

basic use of the system quickly by means of a graded set of examples. Some

readers may find it easier to absorb; those who do not are referred after all to the

standard manual.

“Shouldn’t we read the instructions?”

“Do I look like a sissy?”

Calvin & Hobbes, 19th April 1988

1

Page 2

Contents

1 Installation 5

1.1 Cygwin . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.2 OCaml . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.3 HOL Light . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.4 Checkpointing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

1.5 Other versions of HOL . . . . . . . . . . . . . . . . . . . . . . . . . 9

2 OCaml toplevel basics 10

3 HOL basics 12

3.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

3.2 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

3.3 Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14

3.4 Derived rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16

4 Propositional logic 17

4.1 Proving tautologies . . . . . . . . . . . . . . . . . . . . . . . . . . .19

4.2 Low-level logical rules . . . . . . . . . . . . . . . . . . . . . . . . . 21

4.3 Logic design and veri�cation . . . . . . . . . . . . . . . . . . . . . . 22

5 Equations and functions 24

5.1 Curried functions . . . . . . . . . . . . . . . . . . . . . . . . . . . .26

5.2 Pairing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

5.3 Equational reasoning . . . . . . . . . . . . . . . . . . . . . . . . . .28

5.4 De�nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

6 Abstractions and quanti�ers 31

6.1 Quanti�ers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

6.2 First-order reasoning . . . . . . . . . . . . . . . . . . . . . . . . . .35

7 Conversions and rewriting 37

7.1 Conversionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .38

7.2 Depth conversions . . . . . . . . . . . . . . . . . . . . . . . . . . . .39

7.3 Matching . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

7.4 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

8 Tactics and tacticals 44

8.1 The goalstack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .45

8.2 Inductive proofs about summations . . . . . . . . . . . . . . . . . . .52

9 HOL’s number systems 54

9.1 Arithmetical decision procedures . . . . . . . . . . . . . . . . . . . .56

9.2 Nonlinear reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . .58

9.3 Quanti�er elimination . . . . . . . . . . . . . . . . . . . . . . . . . . 61

2

Page 115

In addition,wp must distribute over conjunction and disjunction. The former must

hold even for a nondeterministic programming language, but for the latter determinism

is essential:

let WP_DISJUNCTIVE = prove

(‘(wp c p) UNION (wp c q) = wp c (p UNION q)‘,

REWRITE_TAC[FUN_EQ_THM; IN; wp; wlp; IN_ELIM_THM; UNION; terminates] THEN

MESON_TAC[DETERMINISM]);;

One can obtain explicit expressions for the weakest preconditions of commands.

For example, attractively, the weakest precondition of a sequence of commands is just

the composition of the two weakest preconditions of the components:

let WP_SEQ = prove

(‘!c1 c2 q. wp (c1 ;; c2) = wp c1 o wp c2‘,

REWRITE_TAC[wp; wlp; terminates; FUN_EQ_THM; o_THM] THEN REPEAT GEN_TAC THEN

GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [sem_CASES] THEN

REWRITE_TAC[injectivity "command"; distinctness "command"] THEN

MESON_TAC[DETERMINISM]);;

16.4 Axiomatic semantics

We can now return to the prototypical programming problem. We are supposed to

produce a programc guaranteeing some predicateq on the output state given an as-

sumptionp on the input state. We can say that a command is a valid solution to this

problem precisely if the input predicatep is contained in the weakest precondition for

q:

let correct = new_definition

‘correct p c q <=> p SUBSET (wp c q)‘;;

This leads us to yet another approach to the semantics of programming languages,

developed by Hoare (1969) from related work by Floyd (1967). Rather than aim at

explicit statements about the state transition relations resulting from commands, we

simply state rules that allow us to deduce valid ‘Hoare triples’correct p c q ,

more usually written informally asp {c} q or {p} c {q}. We can derive a suitable set

of rules directly from our existing semantic definitions, rather than postulate them from

scratch. Two of the simplest rules areprecondition strengthening(we can assume a

stronger precondition than necessary) andpostcondition weakening(we will guarantee

a weaker postconditon than any that we can deduce):

let CORRECT_PRESTRENGTH = prove

(‘!p p’ c q. p SUBSET p’ /\ correct p’ c q ==> correct p c q‘,

REWRITE_TAC[correct; SUBSET_TRANS]);;

let CORRECT_POSTWEAK = prove

(‘!p c q q’. correct p c q’ /\ q’ SUBSET q ==> correct p c q‘,

REWRITE_TAC[correct] THEN MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;

Similarly, we can quite easily derive the usual Hoare rule for sequences:

let CORRECT_SEQ = prove

(‘!p q r c1 c2.

correct p c1 r /\ correct r c2 q ==> correct p (c1 ;; c2) q‘,

REWRITE_TAC[correct; WP_SEQ; o_THM] THEN

MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;

115

Page 116

We will develop these ideas more in the next section in a slightly different context.

17 Shallow embedding

In the previous section we explicitly de�ned the syntax of a programming language

and its semantic map within HOL. The syntactic constructs and their meanings were

quite different things, with the semantic map mediating between them. A contrasting

approach is to regard a programming language as merely a notation for describing that

semantics directly. For example, an assignment statement x := e does not denote

a syntactic object, but rather is a shorthand for, say, a state mapping, state transition

relation or weakest precondition that we associate with it.

This approach, and indeed the embedding of programming language semantics in

theorem provers generally, was pioneered by Gordon (1989), the inventor of the orig-

inal HOL. For some time it was known as semantic embedding, and the fullblown

formalization of the semantic map as syntactic embedding. However, since Boulton,

Gordon, Gordon, Harrison, Herbert, and Van Tassel (1993) the customary terminology

has been to describe the formalization of the syntax and the semantic map (as in the

previous section) as deep embeddingand the direct semantic embedding as shallow

embedding.

It is worth noting that shallow embedding provides a natural formalization of the at-

titudes expressed by Dijkstra (1976), where a �programming language� (he deprecates

the very term) is viewed as an algorithmically-oriented system of mathematical nota-

tion �rst and foremost. Such a notation is meaningful in isolation from any particular

implementation, and indeed the role of a real programming language compiler on a real

machine is to provide a suf�ciently close approximation to the abstract mathematical

counterpart. (Perhaps, for example, imposing some limitations on sizes of integers.)

17.1 State and expressions

Crudely speaking, to move from a deep to a shallow embedding we want to keep the

same basic theorems as in the deep embedding but with the semantic maps value and

sem erased. Expressions are now simply mappings from states to values. Commands

are just their weakest preconditions. (We could use various other direct semantic no-

tions, but this one �ts best with our future plans � see Dijkstra and Scholten (1990)

for some discussion of this point.)

The syntax of expressions in our deep-embedded language was somewhat restricted:

we only had one type, that of natural numbers, and we had to consider it as a Boolean

using C-style hacking. These restrictions were mainly for technical simplicity: we

could have considered a much wider variety of types and operators. But then the

statements and proofs, while still straightforward conceptually, begin to suffer from

a proliferation of cases. In a shallow embedding, there’s nothing to stop us using quite

arbitrary HOL expressions, even noncomputable ones, and we never need to settle on a

�xed repertoire of types and operators at the outset. Of course, this has the apparently

undesirable feature that one can write ‘programs’ that do not correspond to executable

116

Page 230

Parrilo, P. (2001) Semide�nite programming relaxations for semialgebraic

problems. Available from the Web at citeseer.nj.nec.com/

parrilo01semidefinite.html .

Paulson, L. C. (1983) A higher-order implementation of rewriting. Science of Com-

puter Programming, 3, 119�149.

Paulson, L. C. (1987) Logic and computation: interactive proof with Cambridge LCF,

Volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge Uni-

versity Press.

Peres, A. (1991) Two simple proofs of the Kochen-Specker theorem. Journal of

Physics, A24, 175�178.

Ridge, T. (2005) A mechanically veri�ed, ef�cient, sound and complete theorem

prover for �rst order logic. Available via http://homepages.inf.ed.ac.

uk/s0128214/ .

Rivest, R. L., Shamir, A., and Adelman, L. M. (1978) A method for obtaining digital

signatures and public-key cryptosystems. Journal of the ACM, 21, 120�126.

Rudnicki, P. (1987) Obvious inferences. Journal of Automated Reasoning, 3, 383�393.

Rudnicki, P. (1992) An overview of the MIZAR project. Available on the Web as

http://web.cs.ualberta.ca/˜piotr/Mizar/MizarOverview.ps .

Russell, B. (1919) Introduction to mathematical philosophy. Allen & Unwin.

Scott, D. (1993) A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical

Computer Science, 121, 411�440. Annotated version of a 1969 manuscript.

Scott, D. and Strachey, C. (1971) Toward a mathematical semantics for computer lan-

guages. Programming Research Group Technical Monograph PRG-6, Oxford Univ.

Computing Lab.

Slind, K. (1991) An implementation of higher order logic. Technical Report 91-419-

03, University of Calgary Computer Science Department, 2500 University Drive N.

W., Calgary, Alberta, Canada, TN2 1N4. Author’s Masters thesis.

Slind, K. (1997) Derivation and use of induction schemes in higher-order logic. In

Gunter, E. L. and Felty, A. (eds.), Theorem Proving in Higher Order Logics: 10th

International Conference, TPHOLs'97, Volume 1275 of Lecture Notes in Computer

Science, Murray Hill, NJ, pp. ?�? Springer-Verlag.

Smullyan, R. M. (1992) Gödel's Incompleteness Theorems, Volume 19 of Oxford Logic

Guides. Oxford University Press.

Soko�owski, S. (1983) A note on tactics in LCF. Technical Report CSR-140-83, Uni-

versity of Edinburgh, Department of Computer Science.

230

Page 231

Solovay, R. M. (1976) Provability interpretations of modal logic. Israel Journal of

Mathematics, 25, 287�304.

Stickel, M. E. (1988) A Prolog Technology Theorem Prover: Implementation by an

extended Prolog compiler. Journal of Automated Reasoning, 4, 353�380.

Tarski, A. (1936) Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philo-

sophica, 1, 261�405. English translation, ‘The Concept of Truth in Formalized

Languages’, in Tarski (1956), pp. 152�278.

Tarski, A. (1955) A lattice-theoretical �xpoint theorem and its applications. Paci�c

Journal of Mathematics, 5, 285�309.

Tarski, A. (ed.) (1956) Logic, Semantics and Metamathematics. Clarendon Press.

Trybulec, A. and Blair, H. A. (1985) Computer aided reasoning. In Parikh, R. (ed.),

Logics of Programs, Volume 193 of Lecture Notes in Computer Science, Brooklyn,

pp. 406�412. Springer-Verlag.

Wiedijk, F. (2001) Mizar light for HOL Light. In Boulton, R. J. and

Jackson, P. B. (eds.), 14th International Conference on Theorem Prov-

ing in Higher Order Logics: TPHOLs 2001, Volume 2152 of Lecture

Notes in Computer Science, pp. 378�394. Springer-Verlag. Online at

http://link.springer.de/link/service/series/0558/tocs/t2152.htm .

Winskel, G. (1993) The formal semantics of programming languages: an introduction.

Foundations of computing. MIT Press.

Wos, L. (1998) Programs that offer fast, �awless, logical reasoning. Communications

of the ACM, 41(6), 87�102.

Wos, L. and Pieper, G. W. (1999) A Fascinating Country in the World of Computing:

Your Guide to Automated Reasoning. World Scienti�c.

Wright, J. v., Grundy, J., and Harrison, J. (eds.) (1996) Theorem Proving in Higher

Order Logics: 9th International Conference, TPHOLs'96, Volume 1125 of Lecture

Notes in Computer Science, Turku, Finland. Springer-Verlag.

Wright, J. v., Hekanaho, J., Luostarinen, P., and Langbacka, T. (1993) Mechanizing

some advanced re�nement concepts. Formal Methods in System Design, 3, 49�82.

231