Isabelle/HOL : a proof assistant for higher-order logic

>> Google Books

所蔵情報QRコード

Isabelle/HOL : a proof assistant for higher-order logic / Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel

資料種別:

図書

出版情報:

Berlin : Springer, c2002

形態:

xiii, 218 p. ; 24 cm

シリーズ名:

Lecture notes in computer science ; 2283 <BA00009279>

著者名:

ISBN:

9783540433767 [3540433767]

書誌ID:

BA56377991

子書誌情報

フルテキスト

所蔵情報

他の版・巻

書誌詳細

注記:

Includes bibliographies (p. [209]-211) and index
"Tutorial"--cover

主題:

器械計算．計算器

言語:

英語

目次情報:

Elementary Techniques / Part I：

The Basics / 1：

Introduction / 1.1：

Theories / 1.2：

Types, Terms, and Formulae / 1.3：

Variables / 1.4：

Interaction and Interfaces / 1.5：

Getting Started / 1.6：

Functional Programming in HOL / 2：

An Introductory Theory / 2.1：

An Introductory Proof / 2.2：

Some Helpful Commands / 2.3：

Datatypes / 2.4：

Lists / 2.4.1：

The General Format / 2.4.2：

Primitive Recursion / 2.4.3：

Case Expressions / 2.4.4：

Structural Induction and Case Distinction / 2.4.5：

Case Study: Boolean Expressions / 2.4.6：

Some Basic Types / 2.5：

Natural Numbers / 2.5.1：

Pairs / 2.5.2：

Datatype option / 2.5.3：

Definitions / 2.6：

Type Synonyms / 2.6.1：

Constant Definitions / 2.6.2：

The Definitional Approach / 2.7：

More Functional Programming / 3：

Simplification / 3.1：

What Is Simplification? / 3.1.1：

Simplification Rules / 3.1.2：

The simp Method / 3.1.3：

Adding and Deleting Simplification Rules / 3.1.4：

Assumptions / 3.1.5：

Rewriting with Definitions / 3.1.6：

Simplifying let-Expressions / 3.1.7：

Conditional Simplification Rules / 3.1.8：

Automatic Case Splits / 3.1.9：

Tracing / 3.1.10：

Induction Heuristics / 3.2：

Case Study: Compiling Expressions / 3.3：

Advanced Datatypes / 3.4：

Mutual Recursion / 3.4.1：

Nested Recursion / 3.4.2：

The Limits of Nested Recursion / 3.4.3：

Case Study: Tries / 3.4.4：

Total Recursive Functions / 3.5：

Defining Recursive Functions / 3.5.1：

Proving Termination / 3.5.2：

Simplification and Recursive Functions / 3.5.3：

Induction and Recursive Functions / 3.5.4：

Presenting Theories / 4：

Concrete Syntax / 4.1：

Infix Annotations / 4.1.1：

Mathematical Symbols / 4.1.2：

Prefix Annotations / 4.1.3：

Syntax Translations / 4.1.4：

Document Preparation / 4.2：

Isabelle Sessions / 4.2.1：

Structure Markup / 4.2.2：

Formal Comments and Antiquotations / 4.2.3：

Interpretation of Symbols / 4.2.4：

Suppressing Output / 4.2.5：

Logic and Sets / Part II：

The Rules of the Game / 5：

Natural Deduction / 5.1：

Introduction Rules / 5.2：

Elimination Rules / 5.3：

Destruction Rules: Some Examples / 5.4：

Implication / 5.5：

Negation / 5.6：

Interlude: The Basic Methods for Rules / 5.7：

Unification and Substitution / 5.8：

Substitution and the subst Method / 5.8.1：

Unification and Its Pitfalls / 5.8.2：

Quantifiers / 5.9：

The Universal Introduction Rule / 5.9.1：

The Universal Elimination Rule / 5.9.2：

The Existential Quantifier / 5.9.3：

Renaming an Assumption: rename_tac / 5.9.4：

Reusing an Assumption: frule / 5.9.5：

Instantiating a Quantifier Explicitly / 5.9.6：

Description Operators / 5.10：

Definite Descriptions / 5.10.1：

Indefinite Descriptions / 5.10.2：

Some Proofs That Fail / 5.11：

Proving Theorems Using the blast Method / 5.12：

Other Classical Reasoning Methods / 5.13：

Forward Proof: Transforming Theorems / 5.14：

Modifying a Theorem Using of and THEN / 5.14.1：

Modifying a Theorem Using OF / 5.14.2：

Forward Reasoning in a Backward Proof / 5.15：

The Method insert / 5.15.1：

The Method subgoal_tac / 5.15.2：

Managing Large Proofs / 5.16：

Tacticals, or Control Structures / 5.16.1：

Subgoal Numbering / 5.16.2：

Proving the Correctness of Euclid's Algorithm / 5.17：

Sets, Functions, and Relations / 6：

Sets / 6.1：

Finite Set Notation / 6.1.1：

Set Comprehension / 6.1.2：

Binding Operators / 6.1.3：

Finiteness and Cardinality / 6.1.4：

Functions / 6.2：

Function Basics / 6.2.1：

Injections, Surjections, Bijections / 6.2.2：

Function Image / 6.2.3：

Relations / 6.3：

Relation Basics / 6.3.1：

The Reflexive and Transitive Closure / 6.3.2：

A Sample Proof / 6.3.3：

Well-Founded Relations and Induction / 6.4：

Fixed Point Operators / 6.5：

Case Study: Verified Model Checking / 6.6：

Propositional Dynamic Logic - PDL / 6.6.1：

Computation Tree Logic - CTL / 6.6.2：

Inductively Defined Sets / 7：

The Set of Even Numbers / 7.1：

Making an Inductive Definition / 7.1.1：

Using Introduction Rules / 7.1.2：

Rule Induction / 7.1.3：

Generalization and Rule Induction / 7.1.4：

Rule Inversion / 7.1.5：

Mutually Inductive Definitions / 7.1.6：

The Reflexive Transitive Closure / 7.2：

Advanced Inductive Definitions / 7.3：

Universal Quantifiers in Introduction Rules / 7.3.1：

Alternative Definition Using a Monotone Function / 7.3.2：

A Proof of Equivalence / 7.3.3：

Another Example of Rule Inversion / 7.3.4：

Case Study: A Context Free Grammar / 7.4：

Advanced Material / Part III：

More about Types / 8：

Numbers / 8.1：

Numeric Literals / 8.1.1：

The Type of Natural Numbers, nat / 8.1.2：

The Type of Integers, int / 8.1.3：

The Type of Real Numbers, real / 8.1.4：

Pairs and Tuples / 8.2：

Pattern Matching with Tuples / 8.2.1：

Theorem Proving / 8.2.2：

Records / 8.3：

Record Basics / 8.3.1：

Extensible Records and Generic Operations / 8.3.2：

Record Equality / 8.3.3：

Extending and Truncating Records / 8.3.4：

Axiomatic Type Classes / 8.4：

Overloading / 8.4.1：

Axioms / 8.4.2：

Introducing New Types / 8.5：

Declaring New Types / 8.5.1：

Defining New Types / 8.5.2：

Advanced Simplification, Recursion, and Induction / 9：

Advanced Features / 9.1：

How the Simplifier Works / 9.1.2：

Advanced Forms of Recursion / 9.2：

Beyond Measure / 9.2.1：

Recursion over Nested Datatypes / 9.2.2：

Partial Functions / 9.2.3：

Advanced Induction Techniques / 9.3：

Massaging the Proposition / 9.3.1：

Beyond Structural and Recursion Induction / 9.3.2：

Derivation of New Induction Schemas / 9.3.3：

CTL Revisited / 9.3.4：

Case Study: Verifying a Security Protocol / 10：

The Needham-Schroeder Public-Key Protocol / 10.1：

Agents and Messages / 10.2：

Modelling the Adversary / 10.3：

Event Traces / 10.4：

Modelling the Protocol / 10.5：

Proving Elementary Properties / 10.6：

Proving Secrecy Theorems / 10.7：

Appendix / A：

Bibliography

Index

Elementary Techniques / Part I：

The Basics / 1：

Introduction / 1.1：

Theories / 1.2：

Types, Terms, and Formulae / 1.3：

Variables / 1.4：

続きを見る

東工大ブックレビュー

類似資料:

1 電子ブック Isabelle/HOL Nipkow, Tobias, Paulson, Lawrence C., Wenzel, Markus SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg	7 図書 Higher order logic theorem proving and its applications : proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and … IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications, Claesen, Luc J. M., … North-Holland
2 電子ブック Theorem Proving in Higher Order Logics Berghofer, Stefan, Kanade, Takeo, Nipkow, Tobias, Urban, Christian, Wenzel, Makarius Springer eBooks Computer Science, Springer Berlin Heidelberg	8 図書 Theorem proving in higher order logics : 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005 : proceedings International Conference on Theorem Proving in Higher Order Logics, Hurd, Joe, Melham, T. F. (Tom F.) Springer
3 電子ブック Theorem Proving in Higher Order Logics Berghofer, Stefan, Kanade, Takeo, Nipkow, Tobias, Urban, Christian, Wenzel, Makarius SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg	9 電子ブック Types for Proofs and Programs Barendregt, Barendregt, Hendrik Pieter, Nipkow, Tobias SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg
4 図書 Isabelle : a generic theorem prover (: gw ; : us) Paulson, Lawrence C., Nipkow, Tobias, 1958- Springer-Verlag	10 電子ブック Theorem Proving in Higher Order Logics Mohamed, Otmane Ait, Ait Mohamed, Otmane, Kanade, Takeo, Mu?oz, C?sar, Mu?oz, C?sar A., Tahar, Sofi?ne Springer eBooks Computer Science, Springer Berlin Heidelberg
5 図書 Logic and computation : interactive proof with Cambridge LCF Paulson, Lawrence C. Cambridge University Press	11 図書 ML for the working programmer Paulson, Lawrence C. Cambridge University Press
6 電子ブック Higher-Order Algebra, Logic, and Term Rewriting Heering, Heering, J., Meinke, Karl, Möller, Bernhard, Nipkow, Tobias SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg	12 電子ブック Isabelle Paulson, Lawrence C. SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg