# Set theory for verification: I. From foundations to functions

Set theory for verification: I. From foundations to functions 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. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Automated Reasoning Springer Journals

# Set theory for verification: I. From foundations to functions

, Volume 11 (3) – Dec 10, 2004
37 pages

/lp/springer-journals/set-theory-for-verification-i-from-foundations-to-functions-n7QjU7RAQN

# References (63)

Publisher
Springer Journals
Subject
Computer Science; Mathematical Logic and Formal Languages; Artificial Intelligence; Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation
ISSN
0168-7433
eISSN
1573-0670
DOI
10.1007/BF00881873
Publisher site
See Article on Publisher Site

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

### Journal

Journal of Automated ReasoningSpringer Journals

Published: Dec 10, 2004