TY - GEN

T1 - Detecting Unknots via Equational Reasoning, I: Exploration

AU - Fish, Andrew

AU - Lisitsa, Alexei

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

U2 - 10.1007%2F978-3-319-08434-3_7

DO - 10.1007%2F978-3-319-08434-3_7

M3 - Conference contribution with ISSN or ISBN

SN - 9783319084336

VL - 8543

T3 - Lecture Notes in Computer Science

SP - 76

EP - 91

BT - Intelligent Computer Mathematics International Conference, CICM 2014

PB - Springer International Publishing

CY - Portugal

T2 - Intelligent Computer Mathematics International Conference, CICM 2014

Y2 - 1 January 2014

ER -