The following pages link to (Q5302559):
Displaying 50 items.
- Improving legibility of formal proofs based on the close reference principle is NP-hard (Q286805) (← links)
- Formal specification and proofs for the topology and classification of combinatorial surfaces (Q396466) (← links)
- A certified proof of the Cartan fixed point theorems (Q438546) (← links)
- Designing and proving correct a convex hull algorithm with hypermaps in Coq (Q448980) (← links)
- Certifying algorithms (Q465678) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Impossibility of gathering, a certification (Q483063) (← links)
- Formal study of functional orbits in finite domains (Q483296) (← links)
- Can strategizing in round-robin subtournaments be avoided? (Q483532) (← links)
- Book review of: Alexander Soifer, The mathematical coloring book. Mathematics of coloring and the colorful life of its creators (Q485101) (← links)
- An introduction to mechanized reasoning (Q504394) (← links)
- Binary pattern tile set synthesis is NP-hard (Q527409) (← links)
- Effective homology of bicomplexes, formalized in Coq (Q631755) (← links)
- Automated theorem provers: a practical tool for the working mathematician? (Q657585) (← links)
- Linear quantifier elimination (Q707743) (← links)
- Contractibility and the Hadwiger conjecture (Q710728) (← links)
- Floating-point arithmetic in the Coq system (Q714617) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps (Q839032) (← links)
- Computer-aided proof of Erdős discrepancy properties (Q892235) (← links)
- A revision of the proof of the Kepler conjecture (Q977177) (← links)
- Formalization of the Lindemann-Weierstrass theorem (Q1687717) (← links)
- A formal proof in Coq of Lasalle's invariance principle (Q1687728) (← links)
- Formally proving size optimality of sorting networks (Q1694569) (← links)
- Retrieving geometric information from images: the case of hand-drawn diagrams (Q1741163) (← links)
- A formal semantics of nested atomic sections with thread escape (Q1749114) (← links)
- Herbrand's fundamental theorem in the eyes of Jean van Heijenoort (Q1942097) (← links)
- Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
- The simplicial model of univalent foundations (after Voevodsky) (Q2031691) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- Predicativity and constructive mathematics (Q2080590) (← links)
- Formal verification of cP systems using Coq (Q2152300) (← links)
- Vertex coloring of a graph for memory constrained scenarios (Q2183733) (← links)
- Graph theory in Coq: minors, treewidth, and isomorphisms (Q2209536) (← links)
- Multi-scale process modelling and distributed computation for spatial data (Q2209724) (← links)
- First steps towards a formalization of forcing (Q2333671) (← links)
- Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets (Q2352482) (← links)
- Flyspeck II: The basic linear programs (Q2379683) (← links)
- Experimental mathematics, computers and the a priori (Q2441736) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started (Q2657827) (← links)
- Vertex-Coloring with Star-Defects (Q2803807) (← links)
- Tool Support for Proof Engineering (Q2867938) (← links)
- Formalizing Frankl’s Conjecture: FC-Families (Q2907327) (← links)
- Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker (Q2945629) (← links)
- A Certified Reduction Strategy for Homological Image Processing (Q2946732) (← links)
- Computational Complexity Via Finite Types (Q2946764) (← links)
- Checking Proofs (Q2950035) (← links)
- An unavoidable set of $D$-reducible configurations (Q3065754) (← links)
- Beyond Provable Security Verifiable IND-CCA Security of OAEP (Q3073706) (← links)
