Isabelle: A Generic Theorem Prover

Portada
Springer Science & Business Media, 1994 M07 28 - 321 páginas
As a generic theorem prover, Isabelle supports a variety of logics. Distinctive features include Isabelle's representation of logics within a meta-logic and the use of higher-order unification to combine inference rules. Isabelle can be applied to reasoning in pure mathematics or verification of computer systems. This volume constitutes the Isabelle documentation. It begins by outlining theoretical aspects and then demonstrates the use in practice. Virtually all Isabelle functions are described, with advice on correct usage and numerous examples. Isabelle's built-in logics are also described in detail. There is a comprehensive bebliography and index. The book addresses prospective users of Isabelle as well as researchers in logic and automated reasoning.
 

Contenido

1 Foundations
3
12 Formalizing logical rules in Isabelle
7
13 Proof construction in Isabelle
11
14 Lifting a rule into a context
15
15 Backward proof by resolution
17
16 Variations on resolution
21
2 Getting Started with Isabelle
25
22 Backward proof
30
14 The Classical Reasoner
171
142 Simulating sequents by natural deduction
172
143 Extra rules for the sequent calculus
173
144 Classical rule sets
174
145 The classical tactics
176
146 Setting up the classical reasoner
178
Isabelles ObjectLogics
179
15 Basic Concepts
181

23 Quantifier reasoning
34
3 Advanced Methods
41
32 Defining theories
46
the natural numbers
52
35 A Prolog interpreter
58
The Isabelle Reference Manual
63
4 Basic Use of Isabelle
65
42 Ending a session
66
45 Displaying exceptions as error messages
68
The Subgoal Module
71
52 Shortcuts for applying tactics
74
53 Executing batch proofs
76
54 Managing multiple proofs
77
55 Debugging and inspecting
78
6 Tactics
81
62 Other basic tactics
83
63 Obscure tactics
85
64 Managing lots of rules
87
65 Programming tools for proof strategies
89
66 Sequences
90
7 Tacticals
93
72 Control and search tacticals
95
73 Tacticals for subgoal numbering
98
8 Theorems and Forward Proof
101
82 Primitive metalevel inference rules
105
83 Derived rules for goaldirected proof
109
9 Theories Terms and Types
113
92 Loading a new theory
115
93 Reloading modified theories
116
94 Basic operations on theories
118
95 Terms
119
96 Variable binding
120
97 Certified terms
121
98 Types
122
10 Defining Logics
125
103 Mixfix declarations
131
some minimal logics
136
11 Syntax Transformations
139
112 Transforming parse trees to ASTs
140
113 Transforming ASTs to terms
142
Syntactic rewriting
144
116 Translation functions
150
12 Substitution Tactics
153
122 Substitution in the hypotheses
154
123 Setting up hyp_subst_tac
155
13 Simplification
157
132 The simplification tactics
160
133 Examples using the simplifier
161
134 Permutative rewrite rules
164
135 Setting up the simplifier
166
151 Syntax definitions
182
152 Proof procedures
183
16 FirstOrder Logic
185
162 Generic packages
186
164 Classical proof procedures
191
165 An intuitionistic example
192
166 An example of intuitionistic negation
193
167 A classical example
195
168 Derived rules and the classical tactics
196
17 ZermeloFraenkel Set Theory
203
172 The syntax of set theory
204
173 Binding operators
206
17A The ZermeloFraenkel axioms
208
175 From basic lemmas to function spaces
211
176 Further developments
219
177 Simplification rules
228
178 The examples directory
229
179 A proof about powersets
230
1710 Monotonicity of the union operator
232
1711 Lowlevel reasoning about functions
233
18 HigherOrder Logic
235
182 Rules of inference
240
183 A formulation of set theory
245
184 Generic packages and classical reasoning
251
185 Types
253
186 The examples directories
259
Cantors Theorem
260
19 FirstOrder Sequent Calculus
263
192 Syntax and rules of inference
265
193 Tactics for the cut rule
267
194 Tactics for sequents
268
195 Packaging sequent rules
269
196 Proof procedures
270
197 A simple example of classical reasoning
271
198 A more complex proof
272
20 Constructive Type Theory
275
201 Syntax
277
203 Rule lists
281
204 Tactics for subgoal reordering
284
206 Tactics for logical reasoning
285
207 A theory of arithmetic
286
type inference
288
2010 An example of logical reasoning
289
deriving a currying functional
292
proving the Axiom of Choice
293
A Syntax of Isabelle Theories
297
References
301
Index
305
Derechos de autor

Otras ediciones - Ver todas

Términos y frases comunes

Información bibliográfica