The Jordan Curve Theorem, Formally and Informally
From MaRDI portal
Publication:5448058
DOI10.1080/00029890.2007.11920481zbMath1137.03305OpenAlexW2405679748WikidataQ58280796 ScholiaQ58280796MaRDI QIDQ5448058
Publication date: 20 March 2008
Published in: The American Mathematical Monthly (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1080/00029890.2007.11920481
Mechanization of proofs and logical operations (03B35) Relations of low-dimensional topology with graph theory (57M15)
Related Items
An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps, Mathematics by machine, Fuzzy simplification of non-numeric expressions containing some intervals and/or floating point numbers, Sparse interpolation over finite fields via low-order roots of unity, Multivariate sparse interpolation using randomized Kronecker substitutions, Computing the differential Galois group of a parameterized second-order linear differential equation, A new deterministic algorithm for sparse multivariate polynomial interpolation, A fast algorithm for computing the characteristic polynomial of the p-curvature, Computing necessary integrability conditions for planar parametrized homogeneous potentials, Improved algorithm for computing separating linear forms for bivariate systems, Solving higher order linear differential equations having elliptic function coefficients, Parallel telescoping and parameterized Picard-Vessiot theory, A generalized Apagodu-Zeilberger algorithm, The asymptotic analysis of some interpolated nonlinear recurrence relations, Fast arithmetic for the algebraic closure of finite fields, On the computation of the topology of plane curves, Essentially optimal interactive certificates in linear algebra, Root counts of semi-mixed systems, and an application to counting nash equilibria, Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation), Sub-cubic change of ordering for Gröbner basis, Sparse Gröbner bases, The MMO problem, Factoring linear differential operators in n variables, Online order basis algorithm and its impact on the block Wiedemann algorithm, On isomorphisms of modules over non-commutative PID, Radical solutions of first order autonomous algebraic ordinary differential equations, Computing low-degree factors of lacunary polynomials, Maximum likelihood geometry in the presence of data zeros, Constructing fewer open cells by GCD computation in CAD projection, An a posteriori certification algorithm for Newton homotopies, Evaluating parametric holonomic sequences using rectangular splitting, Equivariant lattice generators and Markov bases, Sparse polynomial interpolation codes and their decoding beyond half the minimum distance, Sparse multivariate function recovery with a high error rate in the evaluations, Bounds for D-finite closure properties, Powers of tensors and fast matrix multiplication, Reduction among bracket polynomials, Formal solutions of a class of Pfaffian systems in two variables, On the reduction of singularly-perturbed linear differential systems, High performance implementation of the TFT, Randomized detection of extraneous factors, Toric border basis, On efficient algorithms for computing parametric local cohomology classes associated with semi-quasihomogeneous singularities and standard bases, A near-optimal algorithm for computing real roots of sparse polynomials, LLL reducing with the most significant bits, Covering of surfaces parametrized without projective base points, Linear independence oracles and applications to rectangular and low rank linear systems, Faster relaxed multiplication, Unimodular completion of polynomial matrices, Without Loss of Generality, HOL Light: An Overview, Computational logic: its origins and applications, Formalizing Ordinal Partition Relations Using Isabelle/HOL, Fibbinary zippers in a monoid of toroidal hamiltonian cycles that generate Hilbert-style square-filling curves, The HOL Light theory of Euclidean space, Reliability of mathematical inference, Matrix-F5 algorithms over finite-precision complete discrete valuation fields, Optimal positioning of anodes and virtual sources in the design of cathodic protection systems using the method of fundamental solutions, Planar nearrings on the Euclidean plane., A revision of the proof of the Kepler conjecture, Quantifier elimination by cylindrical algebraic decomposition based on regular chains, Logspace computations in graph products, Tame decompositions and collisions, Formalization of Bing’s Shrinking Method in Geometric Topology, The Zambelli Attractors of Coupled, Nonlinear Macrodynamics and Knot Theory
Uses Software
