Isabelle: A Generic Theorem ProverSpringer 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. |
Dentro del libro
Resultados 1-5 de 36
Página 10
Lo sentimos, el contenido de esta página está restringido..
Lo sentimos, el contenido de esta página está restringido..
Página 12
Lo sentimos, el contenido de esta página está restringido..
Lo sentimos, el contenido de esta página está restringido..
Página 13
Lo sentimos, el contenido de esta página está restringido..
Lo sentimos, el contenido de esta página está restringido..
Página 14
Lo sentimos, el contenido de esta página está restringido..
Lo sentimos, el contenido de esta página está restringido..
Página 15
Lo sentimos, el contenido de esta página está restringido..
Lo sentimos, el contenido de esta página está restringido..
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 |
301 | |
305 | |
Otras ediciones - Ver todas
Términos y frases comunes
abbreviates abstract syntax trees arities assume_tac assumption axioms backward proof bool bound variables bounded quantifiers claset classical reasoner constants Constructive Type Theory consts contains declarations defined definitions depth-first search derived rules elim-resolution elimination rules example False fast_tac first-order logic formula free variables higher-order logic higher-order unification induction infix instantiate introduction rules intuitionistic Isabelle Isabelle's Level macro meta-level meta-logic meta-type mixfix natural deduction natural numbers nonterminal object-level object-logics operator ORELSE P,if P₁ pairs parameters parse tree Pow A Int premises printing priority PROD x:A proof procedures prop prove quantifier recursion replaces res_inst_tac resolution resolve_tac rewrite rules schematic variables Sect sequence sequent calculus set theory simplifier simpset string subgoal subset Suc(x SUM x:A SUM y:B(x symbol syntax tactic term theorem thm list type constructor Type Theory type variables unification Union unknowns