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.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!