TY - GEN

T1 - Visual algebraic proofs for unknot detection

AU - Fish, Andrew

AU - Lisitsa, Alexei

AU - Vernitski, Alexei

N1 - The final authenticated version is available online at https://doi.org/10.1007/978-3-319-91376-6_12

PY - 2018/5/17

Y1 - 2018/5/17

N2 - A knot diagram looks like a two-dimensional drawing of aknotted rubberband. Proving that a given knot diagram can be untangled(that is, is a trivial knot, called an unknot) is one of the most famousproblems of knot theory. For a small knot diagram, one can try to finda sequence of untangling moves explicitly, but for a larger knot diagramproducing such a proof is difficult, and the produced proofs are hardto inspect and understand. Advanced approaches use algebra, with anadvantage that since the proofs are algebraic, a computer can be usedto produce the proofs, and, therefore, a proof can be produced evenfor large knot diagrams. However, such produced proofs are not easy toread and, for larger diagrams, not likely to be human readable at all.We propose a new approach combining advantages of these: the proofsare algebraic and can be produced by a computer, whilst each part ofthe proof can be represented as a reasonably small knot-like diagram(a new representation as a labeled tangle diagram), which can be easilyinspected by a human for the purposes of checking the proof and findingout interesting facts about the knot diagram.

AB - A knot diagram looks like a two-dimensional drawing of aknotted rubberband. Proving that a given knot diagram can be untangled(that is, is a trivial knot, called an unknot) is one of the most famousproblems of knot theory. For a small knot diagram, one can try to finda sequence of untangling moves explicitly, but for a larger knot diagramproducing such a proof is difficult, and the produced proofs are hardto inspect and understand. Advanced approaches use algebra, with anadvantage that since the proofs are algebraic, a computer can be usedto produce the proofs, and, therefore, a proof can be produced evenfor large knot diagrams. However, such produced proofs are not easy toread and, for larger diagrams, not likely to be human readable at all.We propose a new approach combining advantages of these: the proofsare algebraic and can be produced by a computer, whilst each part ofthe proof can be represented as a reasonably small knot-like diagram(a new representation as a labeled tangle diagram), which can be easilyinspected by a human for the purposes of checking the proof and findingout interesting facts about the knot diagram.

U2 - 10.1007/978-3-319-91376-6_12

DO - 10.1007/978-3-319-91376-6_12

M3 - Conference contribution with ISSN or ISBN

SN - 9783319913759

VL - 10871

T3 - Lecture Notes in Computer Science

SP - 89

EP - 104

BT - 10th International Conference on Theory and Applications of Diagrams

A2 - Chapman, P.

A2 - Stapleton, G.

A2 - Moktefi , A.

A2 - Perez-Kriz, S.

A2 - Bellucci , F.

PB - Springer

CY - Edinburgh

T2 - 10th International Conference on Theory and Applications of Diagrams

Y2 - 1 January 2018

ER -