Set Theory for Verification: II. Induction and Recursion

Details Set Theory for Verification: II. Induction and Recursion Set Theory for Verification: II. Induction and Recursion

2000-11-14

arxiv.org/abs/cs/9511102v1

published in Journal of Journal of Automated Reasoning 15 (1995), 167-215

Computer Science

Logic in Computer Science

Scientific paper

A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs and other computational reasoning. Inductively defined sets are expressed as least fixedpoints, applying the Knaster-Tarski Theorem over a suitable set. Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion. Recursive data structures are expressed by applying the Knaster-Tarski Theorem to a set, such as V[omega], that is closed under Cartesian product and disjoint sum. Worked examples include the transitive closure of a relation, lists, variable-branching trees and mutually recursive trees and forests. The Schr\"oder-Bernstein Theorem and the soundness of propositional logic are proved in Isabelle sessions.

Affiliated with

Also associated with

No associations

Rating

Set Theory for Verification: II. Induction and Recursion does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Set Theory for Verification: II. Induction and Recursion, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Set Theory for Verification: II. Induction and Recursion will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-351058