Alexei Lisitsa's talk at MACSMIN 2026, https://kurlin.org/macsmin/2026.php

Speaker. Alexei Lisitsa (Computer Science, University of Liverpool, UK). Title. Automated reasoning for knots and knotted structures with possible applications to proteins. Abstract. In this talk, I will present applications of automated reasoning to problems in knot theory and related knotted structures. Fundamental algorithmic tasks—such as unknot detection (i.e., deciding whether a given knot is trivial) and knot equivalence - can be approached by translating these problems into algebraic invariants, including variants of quandles.These translations enable the use of automated reasoning techniques, such as first-order theorem proving, countermodel finding, and constraint-based methods including SAT solving. I will outline how these approaches provide effective tools for analysing knot properties and, in some cases, for certifying non-equivalence. Potential applications include knot detection and analysis in biological and chemical contexts, such as proteins and polymers, where knotted structures naturally arise.