Isabelle-91

Tobias Nipkow; Lawrence C. Paulson

doi:10.1007/3-540-55602-8_201

Isabelle-91

Tobias Nipkow
, Lawrence C. Paulson

Informatics 7 - Chair of Theoretical Computer Science

University of Cambridge

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

16 Scopus citations

Abstract

Isabelle is a generic theorem prover. Object-logics are formalized within higher-order logic, which is Isabelle’s meta-logic. Proofs are performed by a generalization of resolution, using higher-order unification. The latest incarnation of Isabelle, Isabelle-91, features a type system based on order-sorted unification; this supports polymorphism and overloading in logic definitions.

Original language	English
Title of host publication	Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings
Editors	Deepak Kapur
Publisher	Springer Verlag
Pages	673-676
Number of pages	4
ISBN (Print)	9783540556022
DOIs	https://doi.org/10.1007/3-540-55602-8_201
State	Published - 1992
Event	11th International Conference on Automated Deduction, CADE, 1992 - Saratoga Springs, United States Duration: 15 Jun 1992 → 18 Jun 1992

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	607 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Conference on Automated Deduction, CADE, 1992
Country/Territory	United States
City	Saratoga Springs
Period	15/06/92 → 18/06/92

Access to Document

10.1007/3-540-55602-8_201

Cite this

Nipkow, T., & Paulson, L. C. (1992). Isabelle-91. In D. Kapur (Ed.), Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings (pp. 673-676). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 607 LNAI). Springer Verlag. https://doi.org/10.1007/3-540-55602-8_201

@inproceedings{e8ffef313ab34bbfa0f4bf3b790bd0c8,

title = "Isabelle-91",

abstract = "Isabelle is a generic theorem prover. Object-logics are formalized within higher-order logic, which is Isabelle{\textquoteright}s meta-logic. Proofs are performed by a generalization of resolution, using higher-order unification. The latest incarnation of Isabelle, Isabelle-91, features a type system based on order-sorted unification; this supports polymorphism and overloading in logic definitions.",

author = "Tobias Nipkow and Paulson, \{Lawrence C.\}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1994.; 11th International Conference on Automated Deduction, CADE, 1992 ; Conference date: 15-06-1992 Through 18-06-1992",

year = "1992",

doi = "10.1007/3-540-55602-8\_201",

language = "English",

isbn = "9783540556022",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "673--676",

editor = "Deepak Kapur",

booktitle = "Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings",

}

Nipkow, T & Paulson, LC 1992, Isabelle-91. in D Kapur (ed.), Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 607 LNAI, Springer Verlag, pp. 673-676, 11th International Conference on Automated Deduction, CADE, 1992, Saratoga Springs, United States, 15/06/92. https://doi.org/10.1007/3-540-55602-8_201

Isabelle-91. / Nipkow, Tobias; Paulson, Lawrence C.
Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. ed. / Deepak Kapur. Springer Verlag, 1992. p. 673-676 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 607 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Isabelle-91

AU - Nipkow, Tobias

AU - Paulson, Lawrence C.

PY - 1992

Y1 - 1992

N2 - Isabelle is a generic theorem prover. Object-logics are formalized within higher-order logic, which is Isabelle’s meta-logic. Proofs are performed by a generalization of resolution, using higher-order unification. The latest incarnation of Isabelle, Isabelle-91, features a type system based on order-sorted unification; this supports polymorphism and overloading in logic definitions.

AB - Isabelle is a generic theorem prover. Object-logics are formalized within higher-order logic, which is Isabelle’s meta-logic. Proofs are performed by a generalization of resolution, using higher-order unification. The latest incarnation of Isabelle, Isabelle-91, features a type system based on order-sorted unification; this supports polymorphism and overloading in logic definitions.

UR - https://www.scopus.com/pages/publications/85029583595

U2 - 10.1007/3-540-55602-8_201

DO - 10.1007/3-540-55602-8_201

M3 - Conference contribution

AN - SCOPUS:85029583595

SN - 9783540556022

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 673

EP - 676

BT - Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings

A2 - Kapur, Deepak

PB - Springer Verlag

T2 - 11th International Conference on Automated Deduction, CADE, 1992

Y2 - 15 June 1992 through 18 June 1992

ER -

Isabelle-91

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this