Isabelle/HOL : A Proof Assistant for Higher-Order Logic - Tobias Nipkow

Instant online reading.
Don't wait for delivery!

Isabelle/HOL

A Proof Assistant for Higher-Order Logic

By: Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel

Write A Review

Paperback | 3 April 2002

At a Glance

Paperback
240 Pages

Dimensions(cm)
22.86 x 15.24 x 1.27

Paperback

$89.99

or 4 interest-free payments of $22.50 with

Ships in 5 to 7 business days

This volume is a self-contained introduction to interactive proof in high- order logic (HOL), using the proof assistant Isabelle 2002. Compared with existing Isabelle documentation, it provides a direct route into higher-order logic, which most people prefer these days. It bypasses ?rst-order logic and minimizes discussion of meta-theory. It is written for potential users rather than for our colleagues in the research world. Another departure from previous documentation is that we describe Markus Wenzel's proof script notation instead of ML tactic scripts. The l- ter make it easier to introduce new tactics on the ?y, but hardly anybody does that. Wenzel's dedicated syntax is elegant, replacing for example eight simpli?cation tactics with a single method, namely simp, with associated - tions. The book has three parts. - The ?rst part, Elementary Techniques, shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion. - The second part, Logic and Sets, presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes I- belle/HOL's treatment of sets, functions, and relations and explains how to de?ne sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages.

Shipping

	Standard Shipping	Express Shipping
Metro postcodes:	$9.99	$14.95
Regional postcodes:	$9.99	$14.95
Rural postcodes:	$9.99	$14.95

Orders over $79.00 qualify for free shipping.

How to return your order

At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.

Additional postage charges may be applicable.

Defective items

If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.

For more info please visit our Help Centre.

You Can Find This Book In

Non-Fiction Computing & I.T.Computer Science Artificial Intelligence Medicine Medicine in General Philosophy Philosophy & Logic Mathematical Theory of Computation Mathematics Mathematical Foundation Mathematical Logic

Computer Programming & Software Development Programming & Scripting Languages Computer Architecture & Logic Design Software Engineering

Elementary Techniques
The Basics	p. 3
Introduction	p. 3
Theories	p. 4
Types, Terms, and Formulae	p. 4
Variables	p. 7
Interaction and Interfaces	p. 7
Getting Started	p. 8
Functional Programming in HOL	p. 9
An Introductory Theory	p. 9
An Introductory Proof	p. 11
Some Helpful Commands	p. 15
Datatypes	p. 17
Lists	p. 17
The General Format	p. 17
Primitive Recursion	p. 18
Case Expressions	p. 18
Structural Induction and Case Distinction	p. 19
Case Study: Boolean Expressions	p. 19
Some Basic Types	p. 22
Natural Numbers	p. 22
Pairs	p. 24
Datatype option	p. 24
Definitions	p. 24
Type Synonyms	p. 25
Constant Definitions	p. 25
The Definitional Approach	p. 26
More Functional Programming	p. 27
Simplification	p. 27
What Is Simplification?	p. 27
Simplification Rules	p. 28
The simp Method	p. 28
Adding and Deleting Simplification Rules	p. 29
Assumptions	p. 29
Rewriting with Definitions	p. 30
Simplifying let-Expressions	p. 31
Conditional Simplification Rules	p. 31
Automatic Case Splits	p. 31
Tracing	p. 33
Induction Heuristics	p. 33
Case Study: Compiling Expressions	p. 36
Advanced Datatypes	p. 38
Mutual Recursion	p. 38
Nested Recursion	p. 40
The Limits of Nested Recursion	p. 42
Case Study: Tries	p. 43
Total Recursive Functions	p. 46
Defining Recursive Functions	p. 46
Proving Termination	p. 48
Simplification and Recursive Functions	p. 49
Induction and Recursive Functions	p. 50
Presenting Theories	p. 53
Concrete Syntax	p. 53
Infix Annotations	p. 53
Mathematical Symbols	p. 54
Prefix Annotations	p. 55
Syntax Translations	p. 56
Document Preparation	p. 57
Isabelle Sessions	p. 58
Structure Markup	p. 59
Formal Comments and Antiquotations	p. 60
Interpretation of Symbols	p. 63
Suppressing Output	p. 63
Logic and Sets
The Rules of the Game	p. 67
Natural Deduction	p. 67
Introduction Rules	p. 68
Elimination Rules	p. 69
Destruction Rules: Some Examples	p. 71
Implication	p. 72
Negation	p. 73
Interlude: The Basic Methods for Rules	p. 75
Unification and Substitution	p. 76
Substitution and the subst Method	p. 77
Unification and Its Pitfalls	p. 78
Quantifiers	p. 79
The Universal Introduction Rule	p. 80
The Universal Elimination Rule	p. 80
The Existential Quantifier	p. 82
Renaming an Assumption: rename_tac	p. 82
Reusing an Assumption: frule	p. 83
Instantiating a Quantifier Explicitly	p. 84
Description Operators	p. 85
Definite Descriptions	p. 85
Indefinite Descriptions	p. 86
Some Proofs That Fail	p. 87
Proving Theorems Using the blast Method	p. 89
Other Classical Reasoning Methods	p. 90
Forward Proof: Transforming Theorems	p. 92
Modifying a Theorem Using of and THEN	p. 93
Modifying a Theorem Using OF	p. 95
Forward Reasoning in a Backward Proof	p. 96
The Method insert	p. 97
The Method subgoal_tac	p. 98
Managing Large Proofs	p. 99
Tacticals, or Control Structures	p. 99
Subgoal Numbering	p. 100
Proving the Correctness of Euclid's Algorithm	p. 101
Sets, Functions, and Relations	p. 105
Sets	p. 105
Finite Set Notation	p. 107
Set Comprehension	p. 107
Binding Operators	p. 108
Finiteness and Cardinality	p. 109
Functions	p. 109
Function Basics	p. 109
Injections, Surjections, Bijections	p. 110
Function Image	p. 111
Relations	p. 111
Relation Basics	p. 112
The Reflexive and Transitive Closure	p. 112
A Sample Proof	p. 113
Well-Founded Relations and Induction	p. 114
Fixed Point Operators	p. 116
Case Study: Verified Model Checking	p. 116
Propositional Dynamic Logic - PDL	p. 118
Computation Tree Logic - CTL	p. 121
Inductively Defined Sets	p. 127
The Set of Even Numbers	p. 127
Making an Inductive Definition	p. 127
Using Introduction Rules	p. 128
Rule Induction	p. 128
Generalization and Rule Induction	p. 129
Rule Inversion	p. 130
Mutually Inductive Definitions	p. 131
The Reflexive Transitive Closure	p. 132
Advanced Inductive Definitions	p. 135
Universal Quantifiers in Introduction Rules	p. 135
Alternative Definition Using a Monotone Function	p. 137
A Proof of Equivalence	p. 138
Another Example of Rule Inversion	p. 139
Case Study: A Context Free Grammar	p. 140
Advanced Material
More about Types	p. 149
Numbers	p. 149
Numeric Literals	p. 150
The Type of Natural Numbers, nat	p. 151
The Type of Integers, int	p. 153
The Type of Real Numbers, real	p. 154
Pairs and Tuples	p. 155
Pattern Matching with Tuples	p. 155
Theorem Proving	p. 156
Records	p. 158
Record Basics	p. 158
Extensible Records and Generic Operations	p. 159
Record Equality	p. 161
Extending and Truncating Records	p. 163
Axiomatic Type Classes	p. 164
Overloading	p. 164
Axioms	p. 167
Introducing New Types	p. 170
Declaring New Types	p. 171
Defining New Types	p. 171
Advanced Simplification, Recursion, and Induction	p. 175
Simplification	p. 175
Advanced Features	p. 175
How the Simplifier Works	p. 177
Advanced Forms of Recursion	p. 178
Beyond Measure	p. 178
Recursion over Nested Datatypes	p. 180
Partial Functions	p. 182
Advanced Induction Techniques	p. 186
Massaging the Proposition	p. 186
Beyond Structural and Recursion Induction	p. 188
Derivation of New Induction Schemas	p. 190
CTL Revisited	p. 191
Case Study: Verifying a Security Protocol	p. 195
The Needham-Schroeder Public-Key Protocol	p. 195
Agents and Messages	p. 197
Modelling the Adversary	p. 198
Event Traces	p. 199
Modelling the Protocol	p. 200
Proving Elementary Properties	p. 201
Proving Secrecy Theorems	p. 203
Appendix	p. 207
Bibliography	p. 209
Index	p. 213
Table of Contents provided by Publisher. All Rights Reserved.

Isabelle/HOL

A Proof Assistant for Higher-Order Logic

At a Glance

Paperback

Shipping

How to return your order

Defective items

You Can Find This Book In

More in Computer Science

Python Crash Course

3rd Edition - A Hands-On, Project-Based Introduction to Programming

Microsoft 365 Excel For Dummies

For Dummies (Computer/Tech)

The Tech Coup

How to Save Democracy from Silicon Valley

The AI Con

How To Fight Big Tech's Hype and Create the Future We Want

Nexus

A Brief History of Information Networks from the Stone Age to AI

Creative Machines

AI, Art & Us

Python All-in-One For Dummies

3rd Edition

The AI-Driven Leader

Harnessing AI to Make Faster, Smarter Decisions

Empire of AI

Inside the reckless race for total domination

Microsoft 365 Excel All-in-One For Dummies

Excel for Dummies

Building Machine Learning Systems with a Feature Store

Batch, Real-Time, and LLM Systems

The Shortest History of AI

Artificial Intelligence and Human Existence

Insights on Education, Technology, and Society

Metaheuristics in Engineering Applications

Advances in Metaheuristics

Scary Smart

The Future of Artificial Intelligence and How You Can Save Our World

It's Not in the Manual

Real-World Leadership for Security and Risk Professionals

Deep Learning Applications in Operations Research

Thermal and Flow Measurements

Causal Inference and Machine Learning

In Economics, Social, and Health Sciences

Hands-On Machine Learning with Scikit-Learn and PyTorch

Concepts, Tools, and Techniques to Build Intelligent Systems

AI Systems Performance Engineering

Optimizing Model Training and Inference Workloads with Gpus, Cuda, and Pytorch

Artificial Intelligence in Biomaterials Design and Development

Woodhead Publishing Series in Biomaterials

Intelligent Networked Things

8th China Intelligent Networked Things Conference, CINT 2025, Zhuhai, China, June 13-15, 2025, Proceedings, Part I

Digital Hermeneutics II

Sources, Analysis, Interpretation, Annotation, and Curation : Third International Workshop, Frankfurt am Main, Germany, November 23-24, 2023, Revised Selected Papers

This product is categorised by