<?xml version="1.0" encoding="UTF-8"?>
<TEI xml:space="preserve" xmlns="http://www.tei-c.org/ns/1.0" 
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" 
xsi:schemaLocation="http://www.tei-c.org/ns/1.0 https://raw.githubusercontent.com/kermitt2/grobid/master/grobid-home/schemas/xsd/Grobid.xsd"
 xmlns:xlink="http://www.w3.org/1999/xlink">
	<teiHeader xml:lang="en">
		<fileDesc>
			<titleStmt>
				<title level="a" type="main">Unknot Recognition Through Quantifier Elimination</title>
			</titleStmt>
			<publicationStmt>
				<publisher/>
				<availability status="unknown"><licence/></availability>
			</publicationStmt>
			<sourceDesc>
				<biblStruct>
					<analytic>
						<author>
							<persName><forename type="first">Syed</forename><forename type="middle">M</forename><surname>Meesum</surname></persName>
							<email>meesum.syed@gmail</email>
							<affiliation key="aff0">
								<orgName type="department">Institute of Computer Science</orgName>
								<orgName type="institution">University of Wroc law</orgName>
								<address>
									<country key="PL">Poland</country>
								</address>
							</affiliation>
						</author>
						<author>
							<persName><forename type="first">T</forename><forename type="middle">V H</forename><surname>Prathamesh</surname></persName>
							<email>prathamesh.t@gmail.com</email>
							<affiliation key="aff1">
								<orgName type="department">Department of Computer Science</orgName>
								<orgName type="institution">University of Innsbruck</orgName>
								<address>
									<country key="AT">Austria</country>
								</address>
							</affiliation>
						</author>
						<title level="a" type="main">Unknot Recognition Through Quantifier Elimination</title>
					</analytic>
					<monogr>
						<imprint>
							<date/>
						</imprint>
					</monogr>
					<idno type="MD5">0FE96C6927A32C5F515F619F1465B028</idno>
				</biblStruct>
			</sourceDesc>
		</fileDesc>
		<encodingDesc>
			<appInfo>
				<application version="0.7.2" ident="GROBID" when="2023-03-24T21:58+0000">
					<desc>GROBID - A machine learning software for extracting information from scholarly documents</desc>
					<ref target="https://github.com/kermitt2/grobid"/>
				</application>
			</appInfo>
		</encodingDesc>
		<profileDesc>
			<textClass>
				<keywords>
					<term>real algebraic geometry</term>
					<term>knot theory</term>
					<term>algorithms</term>
					<term>symbolic computation</term>
					<term>SMT solving</term>
				</keywords>
			</textClass>
			<abstract>
<div xmlns="http://www.tei-c.org/ns/1.0"><p>Unknot recognition is one of the fundamental questions in low dimensional topology. In this work, we show that this problem can be encoded as a validity problem in the existential fragment of the first-order theory of real closed fields. This encoding is derived using a well-known result on SU(2) representations of knot groups by Kronheimer-Mrowka. We further show that applying existential quantifier elimination to the encoding enables an UnKnot Recognition algorithm with a complexity of the order 2 O(n) , where n is the number of crossings in the given knot diagram. Our algorithm is simple to describe and has the same runtime as the currently best known unknot recognition algorithms. This leads to an interesting class of problems, of interest to both SMT solving and knot theory.</p></div>
			</abstract>
		</profileDesc>
	</teiHeader>
	<text xml:lang="en">
		<body>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="1">Introduction</head><p>In mathematics, a knot refers to an entangled loop. The fundamental problem in the study of knots is the question of knot recognition: can two given knots be transformed to each other without involving any cutting and pasting? This problem was shown to be decidable by Haken in 1962 <ref type="bibr" target="#b6">[7]</ref> using the theory of normal surfaces. We study the special case in which we ask if it is possible to untangle a given knot to an unknot. The UnKnot Recognition recognition algorithm takes a knot presentation as an input and answers Yes if and only if the given knot can be untangled to an unknot. The best known complexity of UnKnot Recognition recognition is 2 O(n) , where n is the number of crossings in a knot diagram <ref type="bibr" target="#b1">[2,</ref><ref type="bibr" target="#b6">7]</ref>.</p><p>More recent developments show that the UnKnot Recognition recognition is in NP ∩ co-NP. Using the theory of normal surfaces, Hass, Lagarias and Pippenger <ref type="bibr" target="#b7">[8]</ref> proved existence of an NP membership certificate for UnKnot Recognition. A notion which is closer to the commonly accepted notion of untangling a knot is that of using Reidemeister moves. The existence of a polynomial length sequence of Reidemeister moves having size O(n 11 ), that untangles an unknot, was proved to exist by Lackenby <ref type="bibr" target="#b11">[12]</ref>. Searching over all possible Reidemeister moves will give a simple to describe algorithm having runtime of 2 O(n 11 ) . According to Lackenby <ref type="bibr" target="#b11">[12]</ref>, a proof sketch for co-NP membership of UnKnot Recognition was first announced by Agol, but not written down in detail. Assuming the Generalized Reimann Hypothesis, a polynomial-time certificate for non-membership of a knot in UnKnot Recognition was proved to exist by Kuperberg <ref type="bibr" target="#b10">[11]</ref>. Finally, an unconditional proof for the membership of UnKnot Recognition in co-NP was given by Lackenby <ref type="bibr" target="#b12">[13]</ref>.</p><p>Several approaches to unknot recognition can be found in literature, such as a complete knot invariant such as Khovanov homology, branching algorithms <ref type="bibr" target="#b1">[2]</ref> involving normal surface theory, manifold hierarchies <ref type="bibr" target="#b12">[13]</ref>, Dynnikov diagrams <ref type="bibr" target="#b3">[4]</ref>, equational reasoning <ref type="bibr" target="#b4">[5]</ref>, and automated reasoning <ref type="bibr" target="#b14">[15]</ref>.</p><p>Most of the known algorithms deciding UnKnot Recognition are complex and have an involved analysis. There are few implementations of this algorithm. One of the implementations is known to show polynomial time behaviour to recognize an unknot, but behaves exponentially to detect that a given diagram represents a knotted knot. <ref type="bibr" target="#b1">[2]</ref> The authors believe that this paper presents a simpler alternate algorithm, which relies on reducing the above problem to a sentence in the existential theory of reals <ref type="bibr" target="#b16">[17]</ref>. This enables application of the decision procedure for existential theory of reals using quantifier elimination, to obtain an algorithm which is exponential in complexity, thus of the same complexity class as the best known approaches. The algorithm presented in this paper has not yet been implemented.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head>Acknowledgments:</head><p>The authors would like to thank the Institute of Mathematical Sciences, HBNI, Chennai, India, where a part of the work was carried out. The first author is supported by the NCN grant number 2015/18/E/ST6/00456. The second author is supported by the FWF project number P30301.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2">Preliminaries</head><p>This section contains some of the basic definitions in knot theory, and a brief note on quantifier elimination and existential theory of reals without explicitly stating the algorithm. For a more detailed introduction to knot theory one may refer to <ref type="bibr" target="#b17">[18,</ref><ref type="bibr" target="#b2">3,</ref><ref type="bibr" target="#b13">14,</ref><ref type="bibr" target="#b8">9]</ref>, and for quantifier elimination in existential theory of reals, one may refer to <ref type="bibr" target="#b5">[6]</ref>  <ref type="bibr" target="#b0">[1]</ref>.</p><p>For a natural number n, we use [n] to denote the set {1, 2, . . . , n}. We use SU(2) to denote the group which contains 2 × 2 complex hermitian matrices with unit determinant, with multiplication as the group operation. For a natural number d, we use S d to denote the subset of R d with euclidean norm equal to one. The symbol i denotes √ −1, the imaginary root of unity. The symbol ∧ is used to denote the operation of logical conjunction. The symbol ∨ is used to denote the operation of logical disjunction.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2.1">Knot Theory</head><p>Basic Definitions Definition 1. A (tame) knot K is the image of a smooth injective map from S 1 to S 3 . Remark 1. S 3 in the above definition can be replaced by R 3 . But we use S 3 , because some of the concepts that we introduce such as knot groups, exist only in the context of the embedding of a circle in S 3 .</p><p>Two knots are considered to be the same, if they are related by an equivalence condition called ambient isotopy. It is defined as follows:</p><p>Definition 2 (Ambient Isotopy). The knots K 1 and K 2 are ambient isotopic if there exists a smooth map F : S 3 × [0, 1] → S 3 such that:</p><formula xml:id="formula_0">-∀x ∈ S 3 . F (x, 0) = x. -F (K 1 , 1) = K 2 . -∀t ∈ [0, 1]. F (S 3 , t) is a homeomorphism of S 3 .</formula><p>Ambient isotopy describes when a knot can be transformed into another by a deformation that does not involve any cutting and pasting. To draw a knot on paper, we use the convention that wherever the string is shown broken it is assumed to be passing under the unbroken string. To illustrate the above condition, consider the following knots:</p><formula xml:id="formula_1">1) Unknot 2) A Twist 3) Trefoil Knot</formula><p>The first two knot diagrams shown above can be deformed into each other by twisting/untwisting, thus they represent the same knot. Deforming either of the first two knots into the third knot, would involve cutting and pasting. Thus it is different from the former knots. Definition 3. An unknot is a knot which is ambient isotopic to the circle S 1 . A knot k is knotted if and only if it is not an unknot.</p><p>Determining when two diagrams represent the same knot, is the key problem of knot theory. The special case of it, determining when a given knot diagram is equivalent to unknot is called the unknot recognition problem. There have been several algorithms and approaches to the knot recognition, listed in the previous section.</p><p>Knot Group One of the known invariants of knots is the fundamental group of the knot complement. Knot complement refers to the compact 3-manifold obtained by considering the complement of a tubular neighbourhood of the knot. This invariant can detect knots up to mirror image. Presentations of this group, called the Wirtinger presentation, can be easily computed from a knot diagram in the following manner:</p><p>-The knot diagram is oriented in one of the two possible directions. The string constituting the knot is given a direction which fixes the direction of all the arcs occurring in the knot diagram. -Every connected arc is associated to a distinct generator.</p><p>-Every crossing gives rise to a relation in the presentation. The relation depends on the orientation of the arcs in the crossing, in the manner as shown in Figure <ref type="figure" target="#fig_0">1</ref>.</p><p>Computing the Wirtinger presentation of a group from the diagram can be achieved using the steps described above in time which is a linear function of the number of crossings in the given knot diagram.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head>SU(2) representations of the knot group</head><p>The following theorem by Kronheimer -Mrowka, translates unknot recoginition to existence of non-commutative SU(2) representations of the knot group.</p><p>Proposition 1 ([10], <ref type="bibr" target="#b10">[11]</ref>). If K is knotted, then it has an non-commutative SU(2) representations of the knot group π 1 (S 3 \ K).</p><p>The following lemma is derived from the theorem above. The reverse direction of the lemma follows from the fact the knot group of the unknot is Z, and all its SU(2) representations are commutative. Lemma 1. A knot K is knotted if and only if there exists a non-commutative SU(2) representation of the knot group π 1 (S 3 \ K).</p><p>We note that every finitely presented group has a trivial homomorphism to the group SU(2) via a mapping of each generator to the identity matrix.</p><p>x k x j x j x k+1</p><p>x j x j</p><p>x k+1 x k</p><p>x j x k x j -1 = x k+1 x j -1 x k x j = x k+1 </p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2.2">Quantifier Elimination in Existential Theory of Reals</head><p>Decidability of the first-order existential theory of reals refers to the existence of a decision procedure for validity of all sentences of the form:</p><formula xml:id="formula_2">∃ X. F ( X),</formula><p>where F is any quantifier free formula of polynomial equalities and inequalities in real variables X. It follows from the Tarski-Seidenberg theorem that the problem above is decidable by a quantifier elimination algorithm. The quantifier elimination in this case, in fact holds true for deciding validity of all first-order sentences. Quantifier elimination algorithm refers to computation of a quantifier free sentence, which is equivalent to the sentence with quantifiers. Validity of the quantifier free sentences can be computed, which makes the algorithm a decision procedure for the first-order theory. Quantifier elimination algorithm in the existential fragment is restricted to finding equivalent quantifier free sentences only for first-order sentences with existential quantifiers, of the form described above.</p><p>The known complexity bounds for the quantifier elimination in the general first-order theory of reals are doubly exponential. The existential fragment has a much lower complexity bound and there are several algorithms for it. Our analysis will be based on the following result: Proposition 2 (see Proposition 4.2 in <ref type="bibr" target="#b16">[17]</ref>). Given a set P of equations, each of which is either a polynomial equalities or inequality of degree d in k variables, and with integer coefficients of bit length L, we can decide the feasibility of P with L log L log log L( • d) O(k) bit operations.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="3">Algorithm</head><p>The algorithm Unknot-QE appears as Algorithm 1 on the next page.</p><p>Remark 2. The algorithm can be simplified leading to improvements in efficiency, within the same complexity class, but our choice of description is motivated by expository concerns.</p><p>The key idea behind the algorithm can be stated in terms of the following theorem which will be proved in the next section.</p><p>Theorem 1. There exists a computable map Φ, which takes a knot diagram K to a sentence in the existential fragment of the first order theory of reals. A knot K is knotted if and only if Φ(K) is valid. Moreover, applying an existential quantifier elimination algorithm to Φ(K) leads to a decision method for UnKnot Recognition.</p><p>Algorithm: Unknot-QE Input: A knot group π1(S 3 \ K) = g1, g2, . . . , gn | R1, R2, . . . , Rn Output: </p><formula xml:id="formula_3">Output Yes if K is an unknot, otherwise output No 1 begin 2 E ←− ∅ 3 P ←− ∅ 4 for k ← 1 to n do 5 M k ←− a k + ib k c k + id k −c k + id k a k − ib k 6 end for 7 for k ← 1 to n do 8 if R k = gjg k g −1 j g −1 k+1 then 9 E k ←− M k+1 Mj − MjM k 10 end if 11 if R k = g −1 j g k gjg −1 k+1 then 12 E k ←− M k Mj − MjM k+1</formula></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4">Proof of the Algorithm</head><p>In the proof, we reduce the Kronheimer-Mrowka property, stated in Section 2.1, to a first-order sentence in the existential theory of quantifier elimination. Observe that every knot group has Wirtinger presentations which correspond to knot diagrams. These presentations are of the following form:</p><formula xml:id="formula_4">g 1 , g 2 , . . . , g n | R 1 , R 2 , . . . , R n .</formula><p>For i ∈ [n], the symbol g i denotes a generator of the group and R i denotes a relation satisfied by the generators. In the Wirtinger presentation, each R k is either g j g k g −1 j g −1 k+1 or g −1 j g k g j g −1 k+1 , where j ∈ [n] and depends on k, we use +(R k ) or −(R k ) to denote them respectively.</p><p>Finding a non-commutative SU(2) representation of π 1 (S 3 \ K), if it exists, can be seen as a conjunction of the following steps:</p><p>1. Mapping generators of the Wirtinger presentation to matrices in SU(2). 2. Checking that the above map extends to a well defined homomorphism, i.e.</p><p>the matrices corresponding to generators satisfy the generating relations of the Wirtinger presentation. 3. Checking that the map is non-commutative.</p><p>In the following paragraphs, we elaborate on and construct equivalent conditions for each of the above steps. Let g k be a generator in the Wirtinger presentation, associated to a knot diagram. Consider a map Φ from the set of generators to M, in which we map g k to M k .</p><formula xml:id="formula_5">M k = a k + ib k c k + id k −c k + id k a k − ib k (1)</formula><p>Here a k , b k , c k , d k are real variables. For M k to be an element of SU(2), it must be unitary (i.e. the inverse of M k is equal to transpose of its complex-conjugate) and it must have unit determinant, which gives us the following extra condition on the variables used to define it.</p><formula xml:id="formula_6">Observation 2 (folklore) M k ∈ SU(2) if and only if (a 2 k + b 2 k + c 2 k + d 2 k = 1</formula><p>). In addition, the mapped elements M k 's have to satisfy the knot group relations obtained from the Wirtinger presentation i.e.</p><formula xml:id="formula_7">(+(R k ) → M j M k M −1 j M −1 k+1 = I) ∧ (−(R k ) → M −1 j M k M j M −1 k+1 = I) (<label>2</label></formula><formula xml:id="formula_8">)</formula><p>where I is the 2 × 2 identity matrix. For k ∈ [n], we define E k as follows:</p><formula xml:id="formula_9">E k = M k+1 M j − M j M k +(R k ) M k M j − M j M k+1 −(R k )</formula><p>The condition on matrices in Equation ( <ref type="formula" target="#formula_7">2</ref>) can be restated in terms ot E k as follows:</p><formula xml:id="formula_10">Observation 3 For M k ∈ SU(2), for i ∈ [n], a knot group embedding must satisfy E k = 0 0 0 0 .</formula><p>The above observation meets the goal of step <ref type="bibr" target="#b1">(2)</ref>. The above matrix equality can be rewritten as a system of four quadratic equations in real variables in the following fashion:</p><p>-Decompose the matrix E k into real and imaginary parts -Re(E k ) and</p><p>Im(E k ): then E k = 0 if and only if Re(E k ) = 0 and Im(E k ) = 0. -Define Re U (E k ) and Im U (E k ) to be the sets of polynomial equalities:</p><formula xml:id="formula_11">p(x) = 0,</formula><p>where p(x) is an entry in the top row of the Re(E k ) and Im(E k ) respectively. We similarly define Re D (E k ) and Im D (E k ) for the bottom row. Either by simplifying E k or by noticing the fact that the matrices M k form a group and their product matrix must also be of the same form as Equation ( <ref type="formula">1</ref>), one can observe that:</p><formula xml:id="formula_12">Re U (E k ) ∪ Im U (E k ) = Re D (E k ) ∪ Im U (E k ).</formula></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head>Consider the set P, consisting of all the polynomials Re</head><formula xml:id="formula_13">U (E k ), Im U (E k ) and a 2 k + b 2 k + c 2 k + d 2 k − 1 = 0, where k ∈ [n].</formula><p>The following lemma allows us to decrease the number of equalities we have in the system of equations.</p><p>Lemma 2 (Reverse Rabinoswitch Encoding <ref type="bibr" target="#b15">[16]</ref>). Let P = {p 1 = 0, . . . , p m = 0} be the system of m equality constraints, as defined above. Then</p><formula xml:id="formula_14">p 1 = 0 ∧ p 2 = 0 • • • ∧ p m = 0 is satisfiable if and only if i∈[m] p 2 i = 0 is satisfiable.</formula><p>The above equation gives an equivalent condition for checking the existence of a SU(2) representation of a knot group. We need to further ensure that the representation is non-commutative. In general, to check that the generators are non-commutative, we would have to check that at least one of the pairs of generators does not commute. However, the special structure of knot group relations allows for a much simpler encoding into polynomial inequalities. In the following lemma we show that finding a non-commutative SU(2) representation is equivalent to finding a representation which maps at least two distinct generators of the Wirtinger presentation to distinct elements of SU(2). Lemma 3. A knot group π 1 (S 3 \ K), with generators g i , has a non-commutative homomorphism ρ to a group if and only if ρ(g i ) = ρ(g j ), for some i = j.</p><p>Proof. In the forward direction, observe that if the generator's images are all equal then ρ is commutative. In the backward direction, assume that the image set of {g i } 1≤i≤n has at least two distinct elements. Therefore, there must exist an index k ∈ [n] such that ρ(g k ) = ρ(g k+1 ). Without loss of generality assume the relation R k = +(R k ), similar steps would be true for the −(R k ) form of the relations. Since ρ(R k ) = I, we have ρ(g j )ρ(g k )ρ(g j ) −1 ρ(g k+1 ) −1 = I.</p><p>As ρ(g k ) = ρ(g k+1 ), it must be the case that</p><formula xml:id="formula_15">ρ(g j )ρ(g k )ρ(g j ) −1 = ρ(g k ) =⇒ ρ(g j )ρ(g k ) = ρ(g k )ρ(g j ).</formula><p>Therefore ρ is non-commutative.</p><p>If ρ is the SU(2) representation, then it suffices to check that there exist at least two distinct matrices in the image to obtain the existence of a noncommutative representation, in addition to the earlier mentioned constraints. The following series of observations further simplify the criterion: Observation 4 Consider the matrices M j and M k , as defined above where j, k ∈</p><formula xml:id="formula_16">[n]. (M j = M k ) ↔ (a j = a k ∨ b j = b k ∨ c j = c k ∨ d j = d k )</formula><p>Observation 5 Let r 1 , . . . , r m be real numbers. There exist indices j, k ∈ [n] such that r j = r k if and only if m =2 (r 1 = r ) is true.</p><p>The following lemma allows us to convert the system of inequalities encoding the constraint of non-commutativity into just one equivalent inequality. Lemma 4. Let N = {p 1 = 0, . . . , p m = 0} be a system of m inequality constraints. Then p</p><formula xml:id="formula_17">1 = 0 ∨ p 2 = 0 ∨ • • • ∨ p m = 0 is satisfiable if and only if i∈[m] p 2 i = 0 is satisfiable.</formula><p>Proof. The lemma follows from the negation of the statement of Lemma 2.</p><p>Combining Lemmas 3, 4 and Observations 4, 5, we get that it suffices to add the the following inequality, to check non-commutativity:</p><formula xml:id="formula_18">n i=1 (a i − a 1 ) 2 + (b i − b 1 ) 2 + (c i − c 1 ) 2 + (d i − d 1 ) 2 = 0</formula><p>Let E be the set consisting of above inequality and the equation in Lemma 2. It is easy to see from Lemma 2, Observations 4 and 5 and Lemma 4, that there exists a non-commutative representation from the knot group to SU(2), if and only if E has a solution. This completes the proof of Theorem 1.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="5">Complexity Analysis</head><p>The algorithm consists of first computing Wirtinger presentation from the input knot diagram, which can be done in linear time. The formula E can be constructed in polynomial time. Next, we analyse the complexity of deciding the feasibility of the constructed existential formula. If the number of crossings in the provided knot diagram is n then the number of real variables in the system of equations is 4n. The system of equations E consists of exactly two statements; one equality and one inequality, with maximum total degree of any monomial of 4. Finally, note that the coefficients of polynomials occurring in our system of equations are from the set {−2 − 1, 1, 2}, as the coefficients of the polynomials before squaring are from the set {−1, 1}. Using Proposition 2, we get the following result. Theorem 6. The procedure Unknot-QE solves the problem UnKnot Recognition in time 2 O(n) , where n is the number of crossings in the given knot diagram.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="6">Conclusion</head><p>In this article, we presented an algorithm for UnKnot Recognition, a proof of correctness, and an analysis of its complexity. The key advantage of this algorithm over the existent algorithms is the simplicity of description while having the same runtime complexity as the other currently best algorithms. The simplicity of this algorithm is largely from an expository perspective, if the existential quantifier elimination is treated as a blackbox. As an open problem, it would be of interest to probe whether one can reduce the runtime complexity further by using a variant of the algorithm presented. It may be possible to do so by decreasing the number of variables in the equation via substitution methods. Practical aspects of this algorithm also need to be explored further, for instancean implementation using existent tools such as SMT solvers and Cylindrical Algebraic Decomposition would be useful. A more 'efficient' or implementable algorithm for quantifier elimination in the existential theory of reals would further aid both the theoretical and practical aspects of unknot recognition.</p></div><figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_0"><head>Fig. 1 .</head><label>1</label><figDesc>Fig. 1. Wirtinger presentation relations for the knot group.</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_1"><head>14 E 15 E 17 Put a 2 k + b 2 k + c 2 k + d 2 k − 1 in P 18 end for 19 Put the equation p∈P p 2 = 0 in E 20 N ←− ∅ 21 for k ← 2 Algorithm 1 :</head><label>141517222218192202121</label><figDesc>real part of the entries of the first row of E k */ Re k ←− Re U (E k ) /* the complex part of the entries of the first row of E k */ Im k ←− Im U (E k ) 16 Put all the polynomials in E Re k and E Im k in the set P to n do 22 Put a k − a1, b k − b1, c k − c1 and d k − d1 in N 23 end for 24 Put the inequality p∈N p 2 = 0 in E 25 if E is satisfiable then Description of the algorithm for Unknot detection.</figDesc></figure>
		</body>
		<back>
			<div type="references">

				<listBibl>

<biblStruct xml:id="b0">
	<monogr>
		<author>
			<persName><forename type="first">Saugata</forename><surname>Basu</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Richard</forename><surname>Pollack</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Marie-Françoise</forename><surname>Coste-Roy</surname></persName>
		</author>
		<title level="m">Algorithms in real algebraic geometry</title>
				<imprint>
			<publisher>Springer Science &amp; Business Media</publisher>
			<date type="published" when="2007">2007</date>
			<biblScope unit="volume">10</biblScope>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b1">
	<monogr>
		<title level="m" type="main">A fast branching algorithm for unknot recognition with experimental polynomial-time behaviour</title>
		<author>
			<persName><forename type="first">A</forename><surname>Benjamin</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Melih</forename><surname>Burton</surname></persName>
		</author>
		<author>
			<persName><surname>Ozlen</surname></persName>
		</author>
		<idno type="arXiv">arXiv:1211.1079v3</idno>
		<imprint>
			<date type="published" when="2014">2014</date>
		</imprint>
	</monogr>
	<note type="report_type">arXiv preprint</note>
</biblStruct>

<biblStruct xml:id="b2">
	<monogr>
		<title level="m" type="main">Introduction to knot theory</title>
		<author>
			<persName><forename type="first">H</forename><surname>Richard</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Ralph</forename><surname>Crowell</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Fox</forename><surname>Hartzler</surname></persName>
		</author>
		<imprint>
			<date type="published" when="2012">2012</date>
			<publisher>Springer Science &amp; Business Media</publisher>
			<biblScope unit="volume">57</biblScope>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b3">
	<analytic>
		<title level="a" type="main">Arc-presentations of links: monotonic simplification</title>
		<author>
			<persName><surname>Ia Dynnikov</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Fundamenta Mathematicae</title>
		<imprint>
			<biblScope unit="volume">190</biblScope>
			<biblScope unit="page" from="29" to="76" />
			<date type="published" when="2006">2006</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b4">
	<analytic>
		<title level="a" type="main">Efficient knot discrimination via quandle coloring with sat and#-sat</title>
		<author>
			<persName><forename type="first">Andrew</forename><surname>Fish</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Alexei</forename><surname>Lisitsa</surname></persName>
		</author>
		<author>
			<persName><forename type="first">David</forename><surname>Stanovskỳ</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Sarah</forename><surname>Swartwood</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">International Congress on Mathematical Software</title>
				<imprint>
			<publisher>Springer</publisher>
			<date type="published" when="2016">2016</date>
			<biblScope unit="page" from="51" to="58" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b5">
	<analytic>
		<title level="a" type="main">Complexity of deciding Tarski algebra</title>
		<author>
			<persName><surname>Yu Grigor'ev</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Journal of symbolic Computation</title>
		<imprint>
			<biblScope unit="volume">5</biblScope>
			<biblScope unit="issue">1-2</biblScope>
			<biblScope unit="page" from="65" to="108" />
			<date type="published" when="1988">1988</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b6">
	<analytic>
		<title level="a" type="main">Theorie der normalflächen</title>
		<author>
			<persName><forename type="first">Wolfgang</forename><surname>Haken</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Acta Mathematica</title>
		<imprint>
			<biblScope unit="volume">105</biblScope>
			<biblScope unit="issue">3-4</biblScope>
			<biblScope unit="page" from="245" to="375" />
			<date type="published" when="1961">1961</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b7">
	<analytic>
		<title level="a" type="main">The computational complexity of knot and link problems</title>
		<author>
			<persName><forename type="first">Joel</forename><surname>Hass</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Jeffrey</forename><forename type="middle">C</forename><surname>Lagarias</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Nicholas</forename><surname>Pippenger</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Journal of the ACM (JACM)</title>
		<imprint>
			<biblScope unit="volume">46</biblScope>
			<biblScope unit="issue">2</biblScope>
			<biblScope unit="page" from="185" to="211" />
			<date type="published" when="1999">1999</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b8">
	<monogr>
		<title level="m" type="main">A survey of knot theory</title>
		<author>
			<persName><forename type="first">Akio</forename><surname>Kawauchi</surname></persName>
		</author>
		<imprint>
			<date type="published" when="2012">2012</date>
			<publisher>Birkhäuser</publisher>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b9">
	<analytic>
		<title level="a" type="main">Witten&apos;s conjecture and property P</title>
		<author>
			<persName><surname>Peter B Kronheimer</surname></persName>
		</author>
		<author>
			<persName><surname>Tomasz S Mrowka</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Geometry &amp; Topology</title>
		<imprint>
			<biblScope unit="volume">8</biblScope>
			<biblScope unit="issue">1</biblScope>
			<biblScope unit="page" from="295" to="310" />
			<date type="published" when="2004">2004</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b10">
	<analytic>
		<title level="a" type="main">Knottedness is in NP, modulo GRH</title>
		<author>
			<persName><forename type="first">Greg</forename><surname>Kuperberg</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Advances in Mathematics</title>
		<imprint>
			<biblScope unit="volume">256</biblScope>
			<biblScope unit="page" from="493" to="506" />
			<date type="published" when="2014">2014</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b11">
	<analytic>
		<title level="a" type="main">A polynomial upper bound on Reidemeister moves</title>
		<author>
			<persName><surname>Lackenby</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Annals of Mathematics</title>
		<imprint>
			<biblScope unit="volume">182</biblScope>
			<biblScope unit="issue">2</biblScope>
			<biblScope unit="page" from="491" to="564" />
			<date type="published" when="2015">2015</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b12">
	<monogr>
		<title level="m" type="main">The efficient certification of knottedness and thurston norm</title>
		<author>
			<persName><forename type="first">Marc</forename><surname>Lackenby</surname></persName>
		</author>
		<idno type="arXiv">arXiv:1604.00290</idno>
		<imprint>
			<date type="published" when="2016">2016</date>
		</imprint>
	</monogr>
	<note type="report_type">arXiv preprint</note>
</biblStruct>

<biblStruct xml:id="b13">
	<monogr>
		<title level="m" type="main">An introduction to knot theory</title>
		<author>
			<persName><forename type="first">Raymond</forename><surname>Wb</surname></persName>
		</author>
		<author>
			<persName><surname>Lickorish</surname></persName>
		</author>
		<imprint>
			<date type="published" when="2012">2012</date>
			<publisher>Springer Science &amp; Business Media</publisher>
			<biblScope unit="volume">175</biblScope>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b14">
	<analytic>
		<title level="a" type="main">Automated reasoning for knot semigroups and π -orbifold groups of knots</title>
		<author>
			<persName><forename type="first">Alexei</forename><surname>Lisitsa</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Alexei</forename><surname>Vernitski</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">Mathematical Aspects of Computer and Information Sciences</title>
				<imprint>
			<publisher>Springer International Publishing</publisher>
			<date type="published" when="2017">2017</date>
			<biblScope unit="page" from="3" to="18" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b15">
	<analytic>
		<title level="a" type="main">Combined decision techniques for the existential theory of the reals</title>
		<author>
			<persName><forename type="first">Grant</forename><surname>Olney</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Passmore</forename></persName>
		</author>
		<author>
			<persName><forename type="first">Paul</forename><forename type="middle">B</forename><surname>Jackson</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="m">International Conference on Intelligent Computer Mathematics</title>
				<imprint>
			<publisher>Springer</publisher>
			<date type="published" when="2009">2009</date>
			<biblScope unit="page" from="122" to="137" />
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b16">
	<analytic>
		<title level="a" type="main">On the computational complexity and geometry of the first-order theory of the reals. part I: Introduction. preliminaries. the geometry of semi-algebraic sets. the decision problem for the existential theory of the reals</title>
		<author>
			<persName><forename type="first">James</forename><surname>Renegar</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Journal of symbolic computation</title>
		<imprint>
			<biblScope unit="volume">13</biblScope>
			<biblScope unit="issue">3</biblScope>
			<biblScope unit="page" from="255" to="299" />
			<date type="published" when="1992">1992</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b17">
	<monogr>
		<author>
			<persName><forename type="first">Edward</forename><surname>Witten</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Martin</forename><surname>Bridson</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Helmut</forename><surname>Hofer</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Marc</forename><surname>Lackenby</surname></persName>
		</author>
		<author>
			<persName><forename type="first">Rahul</forename><surname>Pandharipande</surname></persName>
		</author>
		<title level="m">Lectures on Geometry</title>
				<imprint>
			<publisher>Oxford University Press</publisher>
			<date type="published" when="2017">2017</date>
		</imprint>
	</monogr>
</biblStruct>

				</listBibl>
			</div>
		</back>
	</text>
</TEI>
