Set theory for verification. I: From foundations to functions
From MaRDI portal
Publication:1319386
DOI10.1007/BF00881873zbMath0802.68128WikidataQ57382712 ScholiaQ57382712MaRDI QIDQ1319386
Publication date: 11 December 1994
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
interactive proofsRamsey's theoremZermelo-Fraenkel set theoryIsabelleCantor's theoremgeneric theorem provinghigher-order syntax
Applications of set theory (03E75) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Related Items
Presentation and manipulation of Mizar properties in an Isabelle object logic, Generating custom set theories with non-set structured objects, A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle, Reconsidering pairs and functions as sets, Automatic Proof and Disproof in Isabelle/HOL, Type Inference for ZFH, ProofScript: Proof Scripting for the Masses, Ordinal arithmetic: Algorithms and mechanization, Set theory for verification. II: Induction and recursion, An approach to literate and structured formal developments, The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf, Categoricity results for second-order ZF in dependent type theory, A concrete final coalgebra theorem for ZF set theory, On extensibility of proof checkers, The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF, Combining higher-order logic with set theory formalizations, Unnamed Item, The Isabelle Framework, Higher-Order Tarski Grothendieck as a Foundation for Formal Proof., An embedding of Ruby in Isabelle, Layered map reasoning, MBase: Representing knowledge and context for the integration of mathematical software systems, Formalization of the fundamental group in untyped set theory using auto2, A fixedpoint approach to implementing (Co)inductive definitions, Categoricity results and large model constructions for second-order ZF in dependent type theory, Semantics of Mizar as an Isabelle object logic, Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?, NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF, Set theory for verification. I: From foundations to functions, The practice of logical frameworks
Uses Software
Cites Work
- An extension of the Boyer-Moore theorem prover to support first-order quantification
- A \(\lambda\)-unifiability test for set theory
- Term rewriting: Some experimental results
- The existence of refinement mappings
- Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operators
- Set theory in first-order logic: Clauses for Gödel's axioms
- Seventy-five problems for testing automatic theorem provers
- Set theory. An introduction to independence proofs
- Automated deduction in von Neumann-Bernays-Gödel set theory
- Unification under a mixed prefix
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Non-resolution theorem proving
- Automatic theorem proving in set theory
- Towards the automation of set theory and its logic
- Fundamentals of contemporary set theory
- Experimenting with Isabelle in ZF set theory
- Set theory for verification. I: From foundations to functions
- \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
- The foundation of a generic theorem prover
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
