Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Isabelle

A Generic Theorem Prover

  • Book
  • © 1994

Overview

Editors:
  1. Lawrence C. Paulson
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 828)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
Softcover Book USD 15.99 USD 54.99
Discount applied Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

About this book

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.

Keywords

Table of contents (21 chapters)

  1. Front Matter

    Download chapter PDF

  2. Foundations

    Pages 1-24

  3. Getting started with Isabelle

    Pages 25-39

  4. Advanced methods

    Pages 41-62

  5. Basic use of Isabelle

    Pages 63-69

  6. Proof management: The subgoal module

    Pages 71-79

  7. Tactics

    Pages 81-91

  8. Tacticals

    Pages 93-100

  9. Theorems and forward proof

    Pages 101-111

  10. Theories, terms and types

    Pages 113-123

  11. Defining logics

    Pages 125-138

  12. Syntax transformations

    Pages 139-152

  13. Substitution tactics

    Pages 153-156

  14. Simplification

    Pages 157-170

  15. The classical reasoner

    Pages 171-178

  16. Basic concepts

    Pages 179-183

  17. First-order logic

    Pages 185-201

  18. Zermelo-Fraenkel set theory

    Pages 203-234

  19. Higher-order logic

    Pages 235-261

  20. First-order sequent calculus

    Pages 263-273
Back to top

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation