Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
From MaRDI portal
Publication:5875415
DOI10.4230/LIPICS.ITP.2019.9OpenAlexW2978296386MaRDI QIDQ5875415FDOQ5875415
Authors: Cezary Kaliszyk, Karol Pąk, Chad E. Brown 
Publication date: 3 February 2023
Full work available at URL: http://drops.dagstuhl.de/opus/volltexte/2019/11064/pdf/LIPIcs-ITP-2019-9.pdf/
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
- The Isabelle Framework
- An introduction to mathematical logic and type theory: To truth through proof.
- Analytic tableaux for higher-order logic with choice
- General bindings and alpha-equivalence in Nominal Isabelle
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Mining the Archive of Formal Proofs
- 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
- Isabelle/HOL. A proof assistant for higher-order logic
- How to identify, translate and combine logics?
- A formulation of the simple theory of types
- Set theory for verification. I: From foundations to functions
- A compendium of continuous lattices in MIZAR
- Four decades of \textsc{Mizar}. Foreword
- Partizan Games in Isabelle/HOLZF
- Higher-order semantics and extensionality
- A mechanized translation from higher-order logic to set theory
- Completeness in the theory of types
- Title not available (Why is that?)
- Analytic Tableaux for Simple Type Theory and its First-Order Fragment
- General models and extensionality
- Brouwer invariance of domain theorem
- Topological manifolds
- Isabelle formalization of set theoretic structures and set comprehensions
- Theorem Proving in Higher Order Logics
- Aligning concepts across proof assistant libraries
- Classification of alignments between concepts of formal mathematical systems
- Sharing HOL4 and HOL Light proof knowledge
- A formal proof of the Kepler conjecture
- Über unerreichbare Kardinalzahlen
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Isabelle import infrastructure for the Mizar Mathematical Library
- Semantics of Mizar as an Isabelle object logic
- Brouwer fixed point theorem in the general case
Cited In (5)
- An intuitionistic formula hierarchy based on high‐school identities
- Combining higher-order logic with set theory formalizations
- A case study of transporting Urysohn's lemma from topology via open sets into topology via neighborhoods
- Title not available (Why is that?)
- Isabelle/HOL/GST: a formal proof environment for generalized set theories
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)
