Visual algebraic proofs for unknot detection

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.