Set theory for verification. II: Induction and recursion
From MaRDI portal
Publication:1904402
DOI10.1007/BF00881916zbMath0840.68104arXivcs/9511102WikidataQ57382717 ScholiaQ57382717MaRDI QIDQ1904402
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
recursive functionsSchröder-Bernstein theoremrecursive data structuresKnaster-Tarski theoreminductively defined sets
Applications of set theory (03E75) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Related Items
Automatic Proof and Disproof in Isabelle/HOL, ProofScript: Proof Scripting for the Masses, Ordinal arithmetic: Algorithms and mechanization, The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf, A concrete final coalgebra theorem for ZF set theory, The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF, The formal verification of the ctm approach to forcing, The Isabelle Framework, Fixpoints and Search in PVS, Goals and benchmarks for automated map reasoning, Layered map reasoning, Formalization of the fundamental group in untyped set theory using auto2, A fixedpoint approach to implementing (Co)inductive definitions, NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF, First steps towards a formalization of forcing, Structuring metatheory on inductive definitions
Uses Software
Cites Work
- Constructing recursion operators in intuitionistic type theory
- Terminating general recursion
- Deductive synthesis of the unification algorithm
- Non-resolution theorem proving
- Fundamentals of contemporary set theory
- Experimenting with Isabelle in ZF set theory
- Set theory for verification. I: From foundations to functions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
