Detecting Unknots via Equational Reasoning, I: Exploration

Andrew Fish, Alexei Lisitsa

Research output: Chapter in Book/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBN

Abstract

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.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics International Conference, CICM 2014
Place of PublicationPortugal
PublisherSpringer International Publishing
Pages76-91
Number of pages16
Volume8543
ISBN (Print)9783319084336
DOIs
Publication statusPublished - 1 Jan 2014
EventIntelligent Computer Mathematics International Conference, CICM 2014 - Coimbra, Portugal, July 7-11, 2014
Duration: 1 Jan 2014 → …

Publication series

NameLecture Notes in Computer Science

Conference

ConferenceIntelligent Computer Mathematics International Conference, CICM 2014
Period1/01/14 → …

Fingerprint Dive into the research topics of 'Detecting Unknots via Equational Reasoning, I: Exploration'. Together they form a unique fingerprint.

Cite this