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

Bibliographic Information

Book Title: Isabelle
Book Subtitle: A Generic Theorem Prover
Editors: Lawrence C. Paulson
Series Title: Lecture Notes in Computer Science
DOI: https://doi.org/10.1007/BFb0030541
Publisher: Springer Berlin, Heidelberg
eBook Packages: Springer Book Archive
Copyright Information: Springer-Verlag Berlin Heidelberg 1994
Softcover ISBN: 978-3-540-58244-1Published: 28 July 1994
eBook ISBN: 978-3-540-48586-5Published: 01 December 2005
Series ISSN: 0302-9743
Series E-ISSN: 1611-3349
Edition Number: 1
Number of Pages: XIX, 329
Topics: Mathematical Logic and Formal Languages, Logics and Meanings of Programs, Software Engineering, Artificial Intelligence, Mathematical Logic and Foundations

Publish with us

Policies and ethics

Editors:

Sections

Buy it now

Buying options

Other ways to access

Table of contents (21 chapters)

Front Matter

About this book