Isabelle/ZF

swMATH4973MaRDI QIDQ17120FDOQ17120

Author name not available (Why is that?)

Official website: http://isabelle.in.tum.de/website-Isabelle2012/dist/library/ZF/README.html

Cited In (86)

• Categoricity results and large model constructions for second-order ZF in dependent type theory
• Structuring metatheory on inductive definitions
• Presentation and manipulation of Mizar properties in an Isabelle object logic
• A fixedpoint approach to implementing (co)inductive definitions
• Mechanizing coinduction and corecursion in higher-order logic
• Title not available (Why is that?)
• Final coalgebras as greatest fixed points in ZF set theory
• Title not available (Why is that?)
• Layered map reasoning: an experimental approach put to trial on sets
• First steps towards a formalization of forcing
• Title not available (Why is that?)
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Relating two standard notions of secrecy
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Isabelle Framework
• Reconsidering pairs and functions as sets
• Generating custom set theories with non-set structured objects
• NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
• MBase: Representing knowledge and context for the integration of mathematical software systems
• Title not available (Why is that?)
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Partial Recursive Functions in Higher-Order Logic
• A first-order syntax for the \(\pi\)-calculus in Isabelle/HOL using permutations
• Combining Type Theory and Untyped Set Theory
• An approach to literate and structured formal developments
• Set theory for verification. II: Induction and recursion
• Set theory for verification. I: From foundations to functions
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Type inference for ZFH
• HERMES
• simpleAPL
• ForMaRE
• VSDITLU
• Monotonox
• Metamath
• A mechanized translation from higher-order logic to set theory
• Lifting
• IsarMathLib
• mini-ML
• ProofScript
• sprfn
• HOLCF
• Depth First Search
• FinFuns
• Logic2CNF
• Presburger Automata
• PROVERB
• ProofPeer
• A set theory with support for partial functions
• A general mathematics of names
• An embedding of Ruby in Isabelle
• Mechanised computability theory
• Coinductive Formal Reasoning in Exact Real Arithmetic
• Ordinal arithmetic: Algorithms and mechanization
• Smooth_Manifolds
• Logic and theory of algorithms. 4th conference on computability in Europe, CiE 2008, Athens, Greece, June 15--20, 2008. Proceedings
• Title not available (Why is that?)
• Semantics of Mizar as an Isabelle object logic
• Partial and nested recursive function definitions in higher-order logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• A higher-order interpretation of deductive tableau
• Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
• Automatic proof and disproof in Isabelle/HOL
• An algebraic treatment of procedure refinement to support mechanical verification
• Goals and benchmarks for automated map reasoning
• Using a generalisation critic to find bisimulations for coinductive proofs
• ProofScript: proof scripting for the masses
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Logic for Programming, Artificial Intelligence, and Reasoning
• Program development schemata as derived rules
• The practice of logical frameworks
• Ordinal Partitions
• ZFC_in_HOL
• Wetzels_Problem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Interfaces for refining recursion and procedures
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• STMM: A set theory for mechanized mathematics
• Set theory or higher order logic to represent auction concepts in Isabelle?

This page was built for software: Isabelle/ZF