On the public citation graph

Formalization of the Equivalence among Completeness Theorems of Real Number in Coq

https://doi.org/10.3390/math9010038
0 signed · 43 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/3-540-39185-1_7openalex-snapshot
A Constructive Formalization of the Fundamental Theorem of Calculus
inferredcites →https://doi.org/10.1007/3-540-44659-1_10openalex-snapshot
On the Mechanization of Real Analysis in Isabelle/HOL
inferredcites →https://doi.org/10.1007/3-540-45842-5_6openalex-snapshot
Constructive Reals in Coq: Axioms and Categoricity
inferredcites →https://doi.org/10.1007/3-540-45949-9openalex-snapshot
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
inferredcites →https://doi.org/10.1007/3-540-52335-9_47openalex-snapshot
Inductively defined types
inferredcites →https://doi.org/10.1007/978-1-4613-8955-2openalex-snapshot
Introduction to Calculus and Analysis
inferredcites →https://doi.org/10.1007/978-1-4613-8958-3openalex-snapshot
Introduction to Calculus and Analysis
inferredcites →https://doi.org/10.1007/978-3-030-52200-1_27openalex-snapshot
A Formalization of Properties of Continuous Functions on Closed Intervals
inferredcites →https://doi.org/10.1007/978-3-540-27818-4_7openalex-snapshot
C-CoRN, the Constructive Coq Repository at Nijmegen
inferredcites →https://doi.org/10.1007/978-3-642-20920-8_4openalex-snapshot
Univalent Foundations of Mathematics
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_14openalex-snapshot
A Machine-Checked Proof of the Odd Order Theorem
inferredcites →https://doi.org/10.1007/978-3-662-07964-5openalex-snapshot
Interactive Theorem Proving and Program Development
inferredcites →https://doi.org/10.1007/bf01384233openalex-snapshot
Constructing the real numbers in HOL
inferredcites →https://doi.org/10.1007/s00283-012-9324-xopenalex-snapshot
N.G. de Bruijn (1918–2012) and his Road to Automath, the Earliest Proof Checker
inferredcites →https://doi.org/10.1007/s10649-007-9101-5openalex-snapshot
The completeness property of the set of real numbers in the transition from calculus to analysis
inferredcites →https://doi.org/10.1007/s10817-018-9490-4openalex-snapshot
Formally Verifying the Solution to the Boolean Pythagorean Triples Problem
inferredcites →https://doi.org/10.1007/s11786-014-0181-1openalex-snapshot
Coquelicot: A User-Friendly Library of Real Analysis for Coq
inferredcites →https://doi.org/10.1016/0890-5401(88)90005-3openalex-snapshot
The calculus of constructions
inferredcites →https://doi.org/10.1016/c2013-0-02242-6openalex-snapshot
The Fundamentals of Mathematical Analysis
inferredcites →https://doi.org/10.1016/j.hm.2004.11.003openalex-snapshot
Bolzano and uniform continuity
inferredcites →https://doi.org/10.1016/s0049-237x(08)70223-4openalex-snapshot
Checking Landau's “Grundlagen” in the Automath System
inferredcites →https://doi.org/10.1017/fmp.2017.1openalex-snapshot
A FORMAL PROOF OF THE KEPLER CONJECTURE
inferredcites →https://doi.org/10.1080/00029890.1960.11989538openalex-snapshot
The Rôle of Compactness in Analysis
inferredcites →https://doi.org/10.1080/00029890.1983.11971185openalex-snapshot
Who Gave You the Epsilon? Cauchy and the Origins of Rigorous Calculus
inferredcites →https://doi.org/10.1093/oso/9780195105193.001.0001openalex-snapshot
What Is Mathematics?
inferredcites →https://doi.org/10.1109/access.2020.2969486openalex-snapshot
A Formal System of Axiomatic Set Theory in Coq
inferredcites →https://doi.org/10.1109/lics.1989.39193openalex-snapshot
ECC, an extended calculus of constructions
inferredcites →https://doi.org/10.1145/3018610.3018620openalex-snapshot
The next 700 syntactical models of type theory
inferredcites →https://doi.org/10.4169/amer.math.monthly.120.05.392openalex-snapshot
Real Analysis in Reverse
inferredcites →https://doi.org/10.48550/arxiv.0905.3713openalex-snapshot
A formal proof of the four color theorem
inferredcites →https://doi.org/10.6092/issn.1972-5787/4552openalex-snapshot
Mixing Computations and Proofs
inferredcites →https://doi.org/10.6092/issn.1972-5787/4716openalex-snapshot
Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions
inferredcites →https://doi.org/10.7551/mitpress/9153.001.0001openalex-snapshot
Certified Programming with Dependent Types

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1007/978-981-95-1106-8_6openalex-snapshot
A Formalization of Adequately Simplified Axiomatic Set Theory in Coq for Mathematical Analysis
inferred← citeshttps://doi.org/10.1007/978-981-95-1106-8_9openalex-snapshot
Proving the Standard Part Principle in Nonstandard Analysis with Rocq Prover
inferred← citeshttps://doi.org/10.1007/s11424-026-5318-1openalex-snapshot
A Comparative Review of ZFC, NBG, and MK Axiom Systems: Theoretical Foundations and Formalization in Coq
inferred← citeshttps://doi.org/10.1109/access.2025.3552634openalex-snapshot
A Review on Mechanical Proving and Formalization of Mathematical Theorems
inferred← citeshttps://doi.org/10.1109/cac53003.2021.9727335openalex-snapshot
Formalizing equivalence between real number completeness and intermediate value theorem
inferred← citeshttps://doi.org/10.1109/cac59555.2023.10450918openalex-snapshot
Formalizing the Term Substitution Theorem in First-Order Logic within the Coq Proof Assistant
inferred← citeshttps://doi.org/10.1109/iccc59590.2023.10507313openalex-snapshot
Formal Proof of Contract Theorem in First-Order Logic in Coq
inferred← citeshttps://doi.org/10.3390/math11051079openalex-snapshot
Formal Verification of a Topological Spatial Relations Model for Geographic Information Systems in Coq
inferred← citeshttps://doi.org/10.3390/math13172707openalex-snapshot
A Machine Proof of the Filter-Method Construction for Real Numbers
inferred← citeshttps://doi.org/10.3390/math9121377openalex-snapshot
Formalizing Calculus without Limit Theory in Coq
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.