A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem
No abstract available.
DOI 10.1007/978-3-319-03545-1_11
Related papers
- Towards Fully Abstract Semantics for Local Variables POPL 1988
- Formally proving a compiler transformation safe Haskell 2015
- A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL OOPSLA 2026
- Verified Characteristic Formulae for CakeML ESOP 2017
- Rely-Guarantee Is Coinductive - - A Proof-Centered Investigation of Inductively Approximated Coinduction - ESOP 2026
- A Formally Verified Foundation for Compositional Heterogeneous Coherence PLDI 2026
- A Certifying Proof Assistant for Synthetic Mathematics in Lean CPP 2026
- Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem CPP 2019