Set theory for verification. II: Induction and recursion

DOI10.1007/BF00881916MaRDI QIDQ1904402zbMATH OpenWikidataFDO

Publication date 20 December 1995

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/cs/9511102

inductively defined sets Knaster-Tarski theorem recursive data structures recursive functions Schröder-Bernstein theorem

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04) Applications of set theory (03E75)

Abstract: 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.

Recommendations

Cites work

Cited in

(23)

Describes a project that uses

Uses Software

This page was built for publication: Set theory for verification. II: Induction and recursion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1904402)