Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
From MaRDI portal
Publication:5875415
Recommendations
- scientific article; zbMATH DE number 1745043
- Theorem proving for and with Gröbner bases theory
- scientific article; zbMATH DE number 1420784
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Free ordered algebraic structures towards proof theory
- Tychonoff's theorem in the framework of formal topologies
- THE LARGE STRUCTURES OF GROTHENDIECK FOUNDED ON FINITE-ORDER ARITHMETIC
- Foundations for analysis and proof theory
- Formalization of geometric algebra theories in higher-order logic
- Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
Cites work
- scientific article; zbMATH DE number 1908324 (Why is no real title available?)
- A compendium of continuous lattices in MIZAR
- A formal proof of the Kepler conjecture
- A formulation of the simple theory of types
- A mechanized translation from higher-order logic to set theory
- Aligning concepts across proof assistant libraries
- An introduction to mathematical logic and type theory: To truth through proof.
- Analytic Tableaux for Simple Type Theory and its First-Order Fragment
- Analytic tableaux for higher-order logic with choice
- Brouwer fixed point theorem in the general case
- Brouwer invariance of domain theorem
- Classification of alignments between concepts of formal mathematical systems
- Completeness in the theory of types
- Four decades of \textsc{Mizar}. Foreword
- General bindings and alpha-equivalence in Nominal Isabelle
- General models and extensionality
- Higher-order semantics and extensionality
- How to identify, translate and combine logics?
- Isabelle formalization of set theoretic structures and set comprehensions
- Isabelle import infrastructure for the Mizar Mathematical Library
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Mining the Archive of Formal Proofs
- Partizan Games in Isabelle/HOLZF
- Semantics of Mizar as an Isabelle object logic
- Seminar of algebraic geometry du Bois-Marie 1963--1964. Topos theory and étale cohomology of schemes (SGA 4). Vol. 1: Topos theory. Exp. I--IV
- Set theory for verification. I: From foundations to functions
- Sharing HOL4 and HOL Light proof knowledge
- The Isabelle Framework
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Theorem Proving in Higher Order Logics
- Topological manifolds
- Über unerreichbare Kardinalzahlen
Cited in
(5)- A case study of transporting Urysohn's lemma from topology via open sets into topology via neighborhoods
- Isabelle/HOL/GST: a formal proof environment for generalized set theories
- scientific article; zbMATH DE number 3924746 (Why is no real title available?)
- An intuitionistic formula hierarchy based on high‐school identities
- Combining higher-order logic with set theory formalizations
Describes a project that uses
Uses Software
This page was built for publication: Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875415)
