- Detecting unknots via equational reasoning, I: Exploration , by Andrew Fish and Alexei Lisitsa, (accepted for Calculemus 2014 , part of CICM 2014)

Unknot detection (or unknot recognizion) problem has attracted a lot of attention, but some of the fundamental questions about it remain open. In particular, it is unknown whether it is possible to recognize unknots in PTIME. It is known though that the problem lies in the intersection of NP and coNP [8,11]. There has been a slow but steady development of the algorithms for unknot detection and their experimental evaluation. Early algorithm presented by W. Haken in his proof of the decidability of UKD [7] served mainly to theoretical purposes and deemed to be too complex to attempt to implement it. Since then various algorithms for unknot detection have been proposed with the various degree of implementability and efficiency [5]. The algorithms based on monotone simplifications [5] provide with the practically fast recoginition of unknots but not necessarily with a decision procedure. The algorithms based on normal surface theory implemented in Regina system [2] provide with an efficient recognition of non-trivial knots. In particular it is reported that every non-trivial knot with the crossing number less or equal to 12 is recognized as such by the procedure from [2] in under 5 min. There still efficiency problems with the existing algorithms, in the worst case they are exponential, and it appears that establishing that a particular diagram with a few hundreds (or even dozens) crossings represents a non-trvial knot may well be out of reach of the available procedures.

That makes an exploration of alternative procedures for unknot detection an intersting and well-justifed task.

Here we propose to explore the following route to the efficient practical algorithms for unknot detection. Unknotedness property can be faithfully characterized by the properties of algebraic invariants associated with knot projections. One can try to prove the properties of concrete invariants by using the methods and procedures develeoped in automated reasoning area.

- x * x = x for all x in Q.
- (x * y) * y = x for all x,y in Q.
- (x * z) * (y * z) = (x * y) * z for all x,y,z in Q.

For a diagram D denote the set of all such relations by R_{D}.

Then the presentation (G_{D} | R_{D}) defines the invoilutory quandle IQ(D), that is a quotient of the free involutory quandle modulo equational theory defined by R_{D}. The importance of involutary quandles in the context of unknot detection relies on the following properties [9,10,13]:

- Involutory quandle is a knot invariant, i.e. it does not depend on a projection of a knot;
- Involutory quandle IQ(D)$ of a knot diagram D is trivial, that is contains a single element e with e *e = e, iff D is a diagram of unknot.

- given a knot digaram convert it to its involutary quandle presentation; then
- convert the task of involutary quandle triviality detection into the task of (dis)proving a first-order equational formuala; and finally
- apply generic automated reasoning tools for first-order equational logic to tackle (dis)proving task

Now we notice that if E_{iq}(D) |-- /\_i=1... n-1 (a_{i} = a_{i+1}) holds true this fact can be established by a proof of the formula E_{iq}(D) --> /\_{i=1... n-1} (a_{i} = a_{i+1}) by a complete automated theorem prover for first-order logic with equality, of which there are many around, see e.g. [1]. For an introducton to the automated theorem proving see e.g. [6].

In order to show that E_{iq}(D) |-- /\_i=1... n-1 (a_{i} = a_{i+1}) does not hold it does suffice to disprove the above implication. We propose to do that by application of a generic finite model finding procedures [4,12] to find a finite countermodel to the formula, or equivalently a finite model for E_{iq}(D) /\ not (/\_{i=1...n-1} (a_{i} = a_{i+1}).

- automated proving E_{iq}(D) --> /\_{i=1... n-1} (a_{i} = a_{i+1}) by a complete first-order theorem prover; and
- automated disproving E_{iq}(D) --> /\_{i=1...n-1} (a_{i} = a_{i+1}) by a complete finite model finding procedure.

- such a countermodel is a homomorphic image of the involutory quandle IQ(D) of D (by satisfaction of E_{iq}(D)); and
- it is non-trivial involutory quandle (by satisfaction of not(/\_{i=1 ... n-1} (a_{i} = a_{i+1})).

Two remarks on the conjecture:

- the knot groups, the invaraints closely related to the involutory quandles are residually finite;
- the only reference dealing with residual finitness of knot quandles known to the author is a question posed on MathOverflow

Here is the formula of the form E_{iq}(D) --> /\_{i=1 .. n-1} (a_{i} = a_{i+1}) for this diagram in the syntax of Prover9/Mace4:

Assumptions, that is E_{iq}(D):

- x * x = x.
- (x * y) * y = x.
- (x * z) * (y * z) = (x * y) * z.
- a1 = a9 * a7.
- a3 = a1 * a2.
- a2 = a3 * a4.
- a5 = a2 * a10.
- a6 = a5 * a4.
- a7 = a6 * a1.
- a8 = a7 * a4.
- a10 = a8 * a9.
- a4 = a10 * a3.
- a9 = a4 * a8.

- (a1 = a2) & (a2 = a3) & (a3 = a4) & (a4 = a5) & (a5 = a6) & (a6 = a7) & (a7 = a8) & (a8 = a9) & (a9 = a10).

Prover9 produces the proof of the formula of the form E_{iq}(D) --> /\_{i=1 ... n-1} (a_{i} = a_{i+1}) for this diagram in just under 15s, demonstrating that indeed it is unknot. The input and the proof produced by Prover9 can be found here. .

Here is the formula of the form E_{iq}(D) --> /\_{i=1 .. n-1} (a_{i} = a_{i+1}) for this diagram: Assumptions, that is E_{iq}(D):

- x * x = x.
- (x * y) * y = x.
- (x * z) * (y * z) = (x * y) * z.
- a * b = c.
- b * c = a.
- c * a = b.

- (a = b) & (b = c)

interpretation( 3, [number=1, seconds=0], [

function(a1, [ 0 ]),

function(a2, [ 1 ]),

function(a3, [ 2 ]),

function(*(_,_), [

0, 2, 1,

2, 1, 0,

1, 0, 2 ])

]).

The square table above represents an interpretation for * operation of involutory quandle, which by the virtue of the method is

- a finite involutory quandle, a homomorphic image of IQ(D);
- a non-trivial involutory quandle;
- is of minimal size among those satsifying conditions above (by the default model finding strategy applied by Mace4).

Better interface to access this data is under construction.

[2] {BenOZ12} Benjamin A. Burton and Melih Olzen, A fast branching algorithm for unknot recognizion with experimental polynomial-time behaviour arXiv:1211.1079 [math.GT],

[3] {Bir35} G.~Birkhoff. On the structure of abstract algebras, {\em Proc. Cambridge Philos. Soc.,} 31:433--454, 1935

[4] {Model} R.~Caferra, A.~Leitsch, N.~Peltier, {\em Automated Model Building}, Applied Logic Series, 31, Kluwer, 2004.

[5] {Dyn} I. A. Dynnikov, Recognition algorithms in knot theory, Uspekhi Mat. Nauk 58 (2003), no. 6(354), 45–92.

[6] {GLM} J.~Goubault-Larrecq and Ian Mackie, {\em Proof Theory and Automated Deduction}, Applied Logic Series, 6, Kluwer, 2001

[7] {Hak61} Wolfgang Haken, Theorie der Normalﬂ¨achen, Acta Math. 105 (1961), 245–375.

[8] {coNP} Joel Hass, Jeﬀrey C. Lagarias, and Nicholas Pippenger, The computational complexity of knot and link problems, J. Assoc. Comput. Mach. 46 (1999), no. 2, 185–211.

[9] {Joyce1982a} Joyce, D., A Classifying Invariant of Knots, the Knot Quandle, Journal of Pure and Applied Algebra 23 (1982) 37-65.

[10] {Joyce1982b} Joyce, D., Simple Quandles, Journal of Algebra 79 (1982) pp. 307-318.

[11]{NP} Greg Kuperberg, Knottedness is in NP, modulo GRH, Preprint, arXiv:1112.0845, November 2011

[12] {McCune} W.~McCune, Prover9 and Mace4, http://www.cs.unm.edu/~mccune/mace4/

[13] {Winker} Steven N. Winker, Quandles, Knot Invariants and the N-fold Branching Cover