Isabelle/ZF
From MaRDI portal
Software:17120
No author found.
Related Items (65)
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 ⋮ A general mathematics of names ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Type Inference for ZFH ⋮ ProofScript: Proof Scripting for the Masses ⋮ Ordinal arithmetic: Algorithms and mechanization ⋮ Logic for Programming, Artificial Intelligence, and Reasoning ⋮ 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 ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Mechanizing coinduction and corecursion in higher-order logic ⋮ Unnamed Item ⋮ Coinductive Formal Reasoning in Exact Real Arithmetic ⋮ Friends with Benefits ⋮ Logic and theory of algorithms. 4th conference on computability in Europe, CiE 2008, Athens, Greece, June 15--20, 2008. Proceedings ⋮ The Isabelle Framework ⋮ Unnamed Item ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An embedding of Ruby in Isabelle ⋮ Goals and benchmarks for automated map reasoning ⋮ STMM: A set theory for mechanized mathematics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Layered map reasoning ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ A higher-order interpretation of deductive tableau ⋮ A Mechanized Translation from Higher-Order Logic to Set Theory ⋮ Interfaces for refining recursion and procedures ⋮ MBase: Representing knowledge and context for the integration of mathematical software systems ⋮ Formalization of the fundamental group in untyped set theory using auto2 ⋮ Combining Type Theory and Untyped Set Theory ⋮ Partial Recursive Functions in Higher-Order Logic ⋮ A fixedpoint approach to implementing (Co)inductive definitions ⋮ Mechanised Computability Theory ⋮ Final coalgebras as greatest fixed points in ZF set theory ⋮ Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings ⋮ Unnamed Item ⋮ Using a generalisation critic to find bisimulations for coinductive proofs ⋮ Categoricity results and large model constructions for second-order ZF in dependent type theory ⋮ Semantics of Mizar as an Isabelle object logic ⋮ A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations ⋮ Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? ⋮ A set theory with support for partial functions ⋮ NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF ⋮ Program development schemata as derived rules ⋮ First steps towards a formalization of forcing ⋮ An algebraic treatment of procedure refinement to support mechanical verification ⋮ Structuring metatheory on inductive definitions ⋮ Unnamed Item ⋮ Set theory for verification. I: From foundations to functions ⋮ The practice of logical frameworks
This page was built for software: Isabelle/ZF
