scientific article; zbMATH DE number 5486210

Publication date: 7 January 2009

Full work available at URL: http://www.ams.org/notices/200811/tx081101382p.pdf

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).

Related Items (78)

A Formalization of Properties of Continuous Functions on Closed Intervals ⋮ Improving legibility of formal proofs based on the close reference principle is NP-hard ⋮ Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps ⋮ Formalizing Frankl’s Conjecture: FC-Families ⋮ Flyspeck II: The basic linear programs ⋮ From realizability to induction via dependent intersection ⋮ Formal verification of cP systems using Coq ⋮ Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started ⋮ Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL ⋮ Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ Computational Complexity Via Finite Types ⋮ Vertex coloring of a graph for memory constrained scenarios ⋮ Formal specification and proofs for the topology and classification of combinatorial surfaces ⋮ Checking Proofs ⋮ Computer-aided proof of Erdős discrepancy properties ⋮ Formalization of the Lindemann-Weierstrass theorem ⋮ A formal proof in Coq of Lasalle's invariance principle ⋮ Computer Bounds for Kronheimer–Mrowka Foam Evaluation ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ What is the point of computers? A question for pure mathematicians ⋮ Mathematics and the formal turn ⋮ Strange new universes: Proof assistants and synthetic foundations ⋮ Formally proving size optimality of sorting networks ⋮ Multivariate spatio‐temporal modelling for assessing Antarctica's present‐day contribution to sea‐level rise ⋮ The formal verification of the ctm approach to forcing ⋮ Herbrand's fundamental theorem in the eyes of Jean van Heijenoort ⋮ Unnamed Item ⋮ Mathematizing as a virtuous practice: different narratives and their consequences for mathematics education and society ⋮ Effective homology of bicomplexes, formalized in Coq ⋮ A certified proof of the Cartan fixed point theorems ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Graph theory in Coq: minors, treewidth, and isomorphisms ⋮ Multi-scale process modelling and distributed computation for spatial data ⋮ Designing and proving correct a convex hull algorithm with hypermaps in Coq ⋮ Unnamed Item ⋮ Experimental mathematics, computers and the a priori ⋮ Certifying algorithms ⋮ Unnamed Item ⋮ Automated theorem provers: a practical tool for the working mathematician? ⋮ Recycling proof patterns in Coq: case studies ⋮ Impossibility of gathering, a certification ⋮ Formal study of functional orbits in finite domains ⋮ Can strategizing in round-robin subtournaments be avoided? ⋮ Book review of: Alexander Soifer, The mathematical coloring book. Mathematics of coloring and the colorful life of its creators ⋮ Primitive Floats in Coq ⋮ Formalization of the Domination Chain with Weighted Parameters (Short Paper) ⋮ From Mathesis Universalis to Provability, Computability, and Constructivity ⋮ Retrieving geometric information from images: the case of hand-drawn diagrams ⋮ An introduction to mechanized reasoning ⋮ A formal semantics of nested atomic sections with thread escape ⋮ Binary pattern tile set synthesis is NP-hard ⋮ Linear quantifier elimination ⋮ A revision of the proof of the Kepler conjecture ⋮ Contractibility and the Hadwiger conjecture ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ Floating-point arithmetic in the Coq system ⋮ An introduction to univalent foundations for mathematicians ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Incidence Simplicial Matrices Formalized in Coq/SSReflect ⋮ Efficient Formal Verification of Bounds of Linear Programs ⋮ An unavoidable set of $D$-reducible configurations ⋮ Verification of dynamic bisimulation theorems in Coq ⋮ Vertex-Coloring with Star-Defects ⋮ Beyond Provable Security Verifiable IND-CCA Security of OAEP ⋮ Implementing geometric algebra products with binary trees ⋮ Formal Proof: Reconciling Correctness and Understanding ⋮ Finite Groups Representation Theory with Coq ⋮ CATEGORY-BASED CO-GENERATION OF SEMINAL CONCEPTS AND RESULTS IN ALGEBRA AND NUMBER THEORY: CONTAINMENT-DIVISION AND GOLDBACH RINGS ⋮ Mining State-Based Models from Proof Corpora ⋮ Automated Improving of Proof Legibility in the Mizar System ⋮ Predicativity and constructive mathematics ⋮ First steps towards a formalization of forcing ⋮ Some Conjectures and Questions in Chromatic Topological Graph Theory ⋮ COMPUTER TOOLS FOR SOLVING MATHEMATICAL PROBLEMS: A REVIEW ⋮ Tool Support for Proof Engineering ⋮ Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets

Uses Software

Coq

This page was built for publication: