Published in

Springer, Journal of Automated Reasoning, 3(11), p. 353-389, 1993

DOI: 10.1007/bf00881873

Links

Tools

Export citation

Search in Google Scholar

Set Theory for Verification: I. From Foundations to Functions

Journal article published in 1993 by Lawrence C. Paulson
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Upload
Orange circle
Postprint: archiving restricted
Upload
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

Abstract

A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting several different logics. Isabelle has the flexibility to adapt to variants of set theory. Its higher-order syntax supports the definition of new binding operators. Unknowns in subgoals can be instantiated incrementally. The paper describes the derivation of rules for descriptions, relations and functions, and discusses interactive proofs of Cantor 's Theorem, the Composition of Homomorphisms challenge [9], and Ramsey 's Theorem [5]. A generic proof assistant can stand up against provers dedicated to particular logics. Key words. Isabelle, set theory, generic theorem proving, Ramsey's Theorem, higher-order syntax Copyright c fl 1998 by Lawrence C. Paulson Research funded by the SERC (grants GR/G53279, GR/H40570) and by the ESPRIT Basic Research Actions 3245 `Logical Frameworks' and ...