Since 2014
Experiments with ZF Set Theory in HOL and Isabelle
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Experiments with ZF Set Theory in HOL and Isabelle
|
|
| Creator |
Agerholm, Sten
Gordon, Mike |
|
| Description |
Most general purpose proof assistants support versions oftyped higher order logic. Experience has shown that these logics are capableof representing most of the mathematical models needed in ComputerScience. However, perhaps there exist applications where ZF-styleset theory is more natural, or even necessary. Examples may includeScott's classical inverse-limit construction of a model of the untyped lambda-calculus (D_inf) and the semantics of parts of the Z specification notation.This paper compares the representation and use of ZF set theory withinboth HOL and Isabelle. The main case study is the construction of D_inf.The advantages and disadvantages of higher-order set theory versus first-orderset theory are explored experimentally. This study also provides acomparison of the proof infrastructure of HOL and Isabelle.
|
|
| Publisher |
Aarhus University
|
|
| Contributor |
—
|
|
| Date |
1995-06-07
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion — |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/19940
10.7146/brics.v2i37.19940 |
|
| Source |
BRICS Report Series; No 37 (1995): RS-37 Experiments with ZF Set Theory in HOL and Isabelle
BRICS Report Series; No 37 (1995): RS-37 Experiments with ZF Set Theory in HOL and Isabelle 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/19940/17593
|
|
| Rights |
Copyright (c) 2015 BRICS Report Series
|
|