Cover Image
Read Now

Isabelle A Generic Theorem Prover

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 o...

Full description

Bibliographic Details
Main Author: Paulson, Lawrence C.
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 1994, 1994
Edition:1st ed. 1994
Series:Lecture Notes in Computer Science
Subjects:
Computer Science Logic And Foundations Of Programming
Software Engineering
Computer Science
Mathematical Logic
Artificial Intelligence
Formal Languages And Automata Theory
Machine Theory
Mathematical Logic And Foundations
Online Access:
Collection: Springer Book Archives -2004 - Collection details see MPG.ReNa
Table of Contents:
  • Foundations
  • Getting started with Isabelle
  • Advanced methods
  • Basic use of Isabelle
  • Proof management: The subgoal module
  • Tactics
  • Tacticals
  • Theorems and forward proof
  • Theories, terms and types
  • Defining logics
  • Syntax transformations
  • Substitution tactics
  • Simplification
  • The classical reasoner
  • Basic concepts
  • First-order logic
  • Zermelo-Fraenkel set theory
  • Higher-order logic
  • First-order sequent calculus
  • Constructive Type Theory
  • Syntax of Isabelle Theories

Similar Items