Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
type: Item
instance of: scholarly article
author: Cezary Kaliszyk
author: Karol Pąk
author: Chad E. Brown
publication date: 2023-02-03T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 7649958
zbMATH Keywords: model
zbMATH Keywords: higher-order
zbMATH Keywords: Tarski Grothendieck
zbMATH Keywords: proof foundation
describes a project that uses: Isabelle
describes a project that uses: kepler98
describes a project that uses: Archive Formal Proofs
describes a project that uses: Satallax
describes a project that uses: Isabelle/HOL
describes a project that uses: Transfer
describes a project that uses: Lifting
describes a project that uses: Mizar
describes a project that uses: ETPS
describes a project that uses: Oz
describes a project that uses: Isabelle/ZF
MaRDI profile type: MaRDI publication profile
full work available at URL: LIPIcs-ITP-2019-9.pdf
OpenAlex ID: W2978296386
title: Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
cites work: An introduction to mathematical logic and type theory: To truth through proof.
cites work: General models and extensionality
cites work: Analytic tableaux for higher-order logic with choice
cites work: The role of the Mizar mathematical library for interactive proof development in Mizar
cites work: A compendium of continuous lattices in MIZAR
cites work: Higher-order semantics and extensionality
cites work: Mining the Archive of Formal Proofs
cites work: Analytic Tableaux for Simple Type Theory and its First-Order Fragment
cites work: A formulation of the simple theory of types
cites work: Sharing HOL4 and HOL Light Proof Knowledge
cites work: Aligning concepts across proof assistant libraries
cites work: Four decades of {\textsc{Mizar}}. Foreword
cites work: 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
cites work: A FORMAL PROOF OF THE KEPLER CONJECTURE
cites work: Completeness in the theory of types
cites work: Theorem Proving in Higher Order Logics
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
cites work: Isabelle import infrastructure for the Mizar Mathematical Library
cites work: Semantics of Mizar as an Isabelle object logic
cites work: General Bindings and Alpha-Equivalence in Nominal Isabelle
cites work: Q4805123
cites work: A Mechanized Translation from Higher-Order Logic to Set Theory
cites work: Classification of alignments between concepts of formal mathematical systems
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Partizan Games in Isabelle/HOLZF
cites work: Set theory for verification. I: From foundations to functions
cites work: Brouwer fixed point theorem in the general case
cites work: Brouwer invariance of domain theorem
cites work: Topological manifolds
cites work: How to identify, translate and combine logics?
cites work: Über unerreichbare Kardinalzahlen
cites work: The Isabelle Framework
DOI: 10.4230/LIPICS.ITP.2019.9
Recommended article: Q4531863
Recommended article: Theorem proving for and with Gröbner bases theory
Recommended article: Q4944848
Recommended article: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
Recommended article: Free ordered algebraic structures towards proof theory
Recommended article: Tychonoff's theorem in the framework of formal topologies
Recommended article: THE LARGE STRUCTURES OF GROTHENDIECK FOUNDED ON FINITE-ORDER ARITHMETIC
Recommended article: Foundations for analysis and proof theory
Recommended article: Formalization of geometric algebra theories in higher-order logic
Recommended article: Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
description: scientific article; zbMATH DE number 7649958