Set theory for verification. I: From foundations to functions

DOI10.1007/BF00881873zbMath0802.68128DBLPjournals/jar/Paulson93WikidataQ57382712 ScholiaQ57382712MaRDI QIDQ1319386

Lawrence Charles Paulson

Publication date: 11 December 1994

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

zbMATH Keywords

interactive proofsRamsey's theoremZermelo-Fraenkel set theoryIsabelleCantor's theoremgeneric theorem provinghigher-order syntax

Mathematics Subject Classification ID

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

Related Items (30)

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

• Coq
• Isabelle
• Isabelle/ZF
• HOL
• Nuprl
• NQTHM
• sprfn

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Set theory for verification. I: From foundations to functions