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

Full description

Bibliographic Details

Main Author:	Paulson, Lawrence C.
Corporate Author:	SpringerLink (Online service)
Other Authors:	Nipkow, Tobias, 1958-
Format:	eBook
Language:	English
Published:	Berlin ; New York : Springer-Verlag, [1994]
Series:	Lecture notes in computer science ; 828.
Subjects:	Isabelle (Computer file) Isabelle (Logiciel) Automatic theorem proving. métalogique. logique. théorie démonstration. déduction. vérification logiciel. langage formel. logique mathématique. Théorèmes > Démonstration automatique. Automatische bewijsvoering. Isabelle <Programm>. Electronic books. Electronic resources (Books)
Online Access:	Connect to the full text of this electronic book