Logic and Computation: Interactive Proof with Cambridge LCFThis book is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about computation. It combines the methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of program statements. Cambridge LCF is based on an earlier theorem-proving system, Edinburgh LCF, which introduced a design that gives the user flexibility to use and extend the system. A goal of this book is to explain the design, which has been adopted in several other systems. The book consists of two parts. Part I outlines the mathematical preliminaries, elementary logic and domain theory, and explains them at an intuitive level, giving reference to more advanced reading; Part II provides sufficient detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach. |
Contents
Survey and History of LCF | 3 |
11 The structure of LCF | 4 |
12 A brief history | 7 |
13 Further reading | 10 |
Formal Proof in First Order Logic | 13 |
22 Introduction to first order logic | 14 |
23 Conjunction | 17 |
24 Disjunction | 19 |
Cambridge LCF | 137 |
Syntactic Operations for PPA | 139 |
52 Quotations | 145 |
53 Primitive constructors and destructors | 150 |
54 Compound constructors and destructors | 154 |
55 Functions required for substitution | 156 |
56 Pattern matching primitives | 159 |
57 Terminal interaction and system functions | 160 |
25 Implication | 20 |
26 Negation | 22 |
27 Understanding quantifiers | 25 |
28 The universal quantifier | 29 |
29 The existential quantifier | 30 |
210 Mathematical induction | 33 |
211 Equality | 34 |
212 A sequent calculus for natural deduction | 38 |
213 A sequent calculus for backwards proof | 42 |
214 Classical deduction in a sequent calculus | 46 |
215 How to find formal proofs | 50 |
216 Further reading | 52 |
A Logic of Computable Functions | 53 |
32 Semantic questions | 57 |
33 Computable functions | 59 |
34 Axioms and rules of the logic | 68 |
35 Fixed point induction | 69 |
36 Admissibility of fixed point induction | 74 |
37 Further reading | 75 |
Structural Induction | 77 |
41 The Cartesian product of two types | 78 |
42 The strict product of two types | 83 |
43 The strict sum of two types | 86 |
44 Lifted types | 90 |
45 Atomic types | 93 |
46 Recursive type definitions | 94 |
47 The inverse limit construction for recursive domains | 98 |
48 The type of lazy lists | 110 |
49 The type of strict lists | 114 |
410 Formal reasoning about types | 118 |
411 Structural induction over lazy lists | 125 |
412 Structural induction over strict lists | 129 |
413 Automating the derivation of induction | 134 |
414 Further reading | 135 |
Theory Structure | 163 |
61 Drafting a new theory | 164 |
62 Using a theory | 174 |
63 Inspecting a theory | 177 |
64 Limitations of theories | 179 |
Axioms and Inference Rules | 181 |
72 First order logic | 183 |
73 Domain theory | 194 |
74 Forwards proof and derived rules | 200 |
75 Discussion and further reading | 207 |
Tactics and Tacticals | 209 |
82 Tactics for first order logic | 213 |
83 Domain theory | 219 |
84 Simple backwards proof | 220 |
85 Complex tactics | 224 |
86 The subgoal package | 228 |
87 Tacticals | 234 |
88 Discussion and further reading | 244 |
Rewriting and Simplification | 245 |
91 The extraction of rewrite rules | 246 |
92 The standard rewriting strategy | 248 |
93 Toplevel rewriting tools | 249 |
94 Conversions | 257 |
95 Implementing new rewriting strategies | 262 |
96 Further reading | 263 |
Sample Proofs | 265 |
102 Commutativity of addition | 271 |
103 Equality on the natural numbers | 273 |
104 A simple fixed point induction | 278 |
105 A mapping functional for infinite sequences | 281 |
106 Project suggestions | 287 |
| 289 | |
| 296 | |
Other editions - View all
Logic and Computation: Interactive Proof with Cambridge LCF Lawrence C. Paulson Limited preview - 1987 |
Logic and Computation: Interactive Proof with Cambridge LCF Lawrence C. Paulson No preview available - 1987 |
Common terms and phrases
A-calculus A₁ ACCEPT_ASM_TAC applied argument ASM_REWRITE_TAC axioms bi-implication bool bound variable Cambridge LCF Cartesian product chain-complete conjunction constant construction conv defined denotational semantics derived rules destructors disjunction domain theory Edinburgh LCF element elimination rule embedding equations equivalent Example Exercise exhaustion axiom expression fconv fixed point induction free variables goal proved implication inference rules infix introduction rule isomorphism functions LAPP lazy lists LCONS least upper bound list of theorems llist LNIL meta monotonic n-place natural deduction natural numbers new_closed_axiom operator order logic ORELSE pair partial ordering predicate premise programming proof tree rewrite rules semantics SEQ_OF_FUN sequent calculus simplifies SND TT Standard ML strict lists string structural induction subgoal substitution SUCC symbol t₁ term list theorem thm list type constructors type variables universal quantifier UP(x valid void Vx.A