The paper proves Tarski's Axiom A inside Egal and constructs a Grothendieck universe operator inside Mizar, establishing a relationship between the two formalizations of Tarski-Grothendieck set theory.
(ed s.) Theorem Proving in Higher Order Logics
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
verdicts
UNVERDICTED 2representative citing papers
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
citing papers explorer
-
A Tale of Two Set Theories
The paper proves Tarski's Axiom A inside Egal and constructs a Grothendieck universe operator inside Mizar, establishing a relationship between the two formalizations of Tarski-Grothendieck set theory.
-
Reformalization of the Jordan Curve Theorem
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.