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...
| Main Author: | |
|---|---|
| Format: | Book |
| Language: | English |
| Published: |
Berlin ; New York :
Springer-Verlag,
©1994
|
| Series: | Lecture notes in computer science ;
828 |
| Subjects: |