Get 20M+ Full-Text Papers For Less Than $1.50/day. Subscribe now for You or Your Team.

Learn More →

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

Journal of Automated Reasoning , Volume 11 (3) – Dec 10, 2004

Loading next page...
 
/lp/springer-journals/set-theory-for-verification-i-from-foundations-to-functions-n7QjU7RAQN

References (63)

Publisher
Springer Journals
Copyright
Copyright
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

There are no references for this article.