Isabelle: A Generic Theorem Prover

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.

Comentarios de la gente -Escribir un comentario

No encontramos ningún comentario en los lugares habituales.

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

Referencias a este libro

 ML for the Working ProgrammerVista previa limitada - 1996
 Isabelle/HOL: A Proof Assistant for Higher-Order LogicSin vista previa disponible - 2002
Todos los resultados de la Búsqueda de libros &raquo;