Designing a Theorem Prover - Lowrence C. Paulson (1992, in Handbook of Logic puter Science vol.2).pdf

文档介绍：Designing a Theorem Prover
Lawrence C Paulson
Computer Laboratory
University of Cambridge
May 1990
CONTENTS 2
Contents
1 Folderol: a simple theorem prover 3
Representation of rules .......................... 4
Propositional logic ............................ 5
Quanti
ers and uni
cation ........................ 7
Parameters in quanti
er rules ...................... 7
2 Basic data structures and operations 10
Terms ................................... 10
Formulae .................................. 11
Abstraction and substitution ....................... 11
Parsing and printing ........................... 13
3 Uni
cation 14
Examples ................................. 15
Parameter dependencies in uni
cation .................. 16
The environment ............................. 17
The ML code for uni
cation ....................... 17
Extensions and omissions ......................... 18
Instantiation by the environment .................... 19
4 Inference in Folderol 20
Solving a goal ............................... 21
Selecting a rule .............................. 22
Constructing the subgoals ........................ 23
Goal selection ............................... 25
5 Folderol in action 27
Propositional examples .......................... 27
Quanti
er examples ............................ 30
Beyond Folderol: advanced automatic methods ............. 37
6 Interactive theorem proving 39
The Boyer/Moore theorem prover .................... 40
The Automath languages ......................... 41
LCF, a programmable theorem prover .................. 42
Validation-based tactics ......................... 43
State-based tactics ............................ 45
Technical aspects of Isabelle ....................... 46
7 Conclusion 47
8 Program listing 48
1 FOLDEROL: A SIMPLE THEOREM PROVER 3
1 Folderol: a si