Isabelle/ZF

swMATH4973MaRDI QIDQ17120FDOQ17120

Author name not available (Why is that?)

Cited In (65)

• Title not available (Why is that?)
• Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?
• Categoricity results and large model constructions for second-order ZF in dependent type theory
• Structuring metatheory on inductive definitions
• Mechanised Computability Theory
• Presentation and manipulation of Mizar properties in an Isabelle object logic
• Mechanizing coinduction and corecursion in higher-order logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Final coalgebras as greatest fixed points in ZF set theory
• Title not available (Why is that?)
• First steps towards a formalization of forcing
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Automatic Proof and Disproof in Isabelle/HOL
• Friends with Benefits
• Relating two standard notions of secrecy
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• ProofScript: Proof Scripting for the Masses
• The Isabelle Framework
• Reconsidering pairs and functions as sets
• Interfaces for refining recursion and procedures
• 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
• A Mechanized Translation from Higher-Order Logic to Set Theory
• Partial Recursive Functions in Higher-Order Logic
• A first-order syntax for the \(\pi\)-calculus in Isabelle/HOL using permutations
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
• 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
• Title not available (Why is that?)
• A set theory with support for partial functions
• Formalization of the fundamental group in untyped set theory using auto2
• A general mathematics of names
• An embedding of Ruby in Isabelle
• A fixedpoint approach to implementing (Co)inductive definitions
• Layered map reasoning
• Coinductive Formal Reasoning in Exact Real Arithmetic
• Ordinal arithmetic: Algorithms and mechanization
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• 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?)
• STMM: A set theory for mechanized mathematics
• Type Inference for ZFH
• A higher-order interpretation of deductive tableau
• 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
• Logic for Programming, Artificial Intelligence, and Reasoning
• Program development schemata as derived rules
• The practice of logical frameworks

This page was built for software: Isabelle/ZF