Detecting Unknots via Equational Reasoning, I: Exploration

DOI10.1007/978-3-319-08434-3_7MaRDI QIDQ5495915zbMATH OpenOpenAlexFDO

Authors Andrew Fish, Alexej P. Lisitsa

Publication date 7 August 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1405.4211

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05)

Abstract: We explore the application of automated reasoning techniques to unknot detection, a classical problem of computational topology. We adopt a two-pronged experimental approach, using a theorem prover to try to establish a positive result (i.e. that a knot is the unknot), whilst simultaneously using a model finder to try to establish a negative result (i.e. that the knot is not the unknot). The theorem proving approach utilises equational reasoning, whilst the model finder searches for a minimal size counter-model. We present and compare experimental data using the involutary quandle of the knot, as well as comparing with alternative approaches, highlighting instances of interest. Furthermore, we present theoretical connections of the minimal countermodels obtained with existing knot invariants, for all prime knots of up to 10 crossings: this may be useful for developing advanced search strategies.

Recommendations

• Visual Algebraic Proofs for Unknot Detection
• A new algorithm for recognizing the unknot
• TOWARDS AN IMPLEMENTATION OF THE B–H ALGORITHM FOR RECOGNIZING THE UNKNOT
• Detecting unknotted graphs in 3-space
• Disentangling topological puzzles by using knot theory
• Formalising Knot Theory in Isabelle/HOL
• scientific article; zbMATH DE number 3866609
• UNKNOTTING OPERATIONS BY USING ORIENTED TRIVIAL TANGLE DIAGRAMS
• Reasoning Using Knots
• scientific article; zbMATH DE number 17249

Cites work

• A classifying invariant of knots, the knot quandle
• Automated model building
• scientific article; zbMATH DE number 3530652 (Why is no real title available?)
• scientific article; zbMATH DE number 274896 (Why is no real title available?)
• Knottedness is in NP, modulo GRH
• Proof theory and automated deduction
• RACKS AND LINKS IN CODIMENSION TWO
• Recognition algorithms in knot theory
• Simple quandles
• The computational complexity of knot and link problems
• Theorie der Normalflächen. Ein Isotopiekriterium für den Kreisknoten
• Three dimensional manifolds, Kleinian groups and hyperbolic geometry

Cited in

(9)

• Dihedral semigroups, their defining relations and an application to describing knot semigroups of rational links
• Efficient knot discrimination via quandle coloring with SAT and \#-SAT
• Automated reasoning for knot semigroups and -orbifold groups of knots
• A neural network approach to predicting and computing knot invariants
• Visual Algebraic Proofs for Unknot Detection
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• Semigroups, keis and groups induced by knot diagrams: an experimental investigation with automated reasoning
• Machine learning discovers invariants of braids and flat braids
• Fundamental n-quandles of links are residually finite

Describes a project that uses

Uses Software

• Prover9
• Mace4
• MathOverflow
• KnotInfo

This page was built for publication: Detecting Unknots via Equational Reasoning, I: Exploration

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5495915)