Record Details

Mechanising knot Theory

Electronic Theses of Indian Institute of Science

View Archive Info
 
 
Field Value
 
Title Mechanising knot Theory
 
Creator Prathamesh, Turga Venkata Hanumantha
 
Subject Knot Theory
Theorem Proving
Formal Theorem Proving
Kauffman Bracket
Link Theory
First Order Logic
Tangles
Matrices
Formalising Knot Theory
Symbolic and Mathematical Logic
Knots
Braids
Mathematics
 
Description Mechanisation of Mathematics refers to use of computers to generate or check proofs in Mathematics. It involves translation of relevant mathematical theories from one system of logic to another, to render these theories implementable in a computer. This process is termed formalisation of mathematics. Two among the many ways of mechanising are:
1 Generating results using automated theorem provers.
2 Interactive theorem proving in a proof assistant which involves a combination of user intervention and automation.
In the first part of this thesis, we reformulate the question of equivalence of two Links in first order logic using braid groups. This is achieved by developing a set of axioms whose canonical model is the braid group on infinite strands B∞. This renders the problem of distinguishing knots and links, amenable to implementation in first order logic based automated theorem provers. We further state and prove results pertaining to models of braid axioms.
The second part of the thesis deals with formalising knot Theory in Higher Order Logic using the interactive proof assistant -Isabelle. We formulate equivalence of links in higher order logic. We obtain a construction of Kauffman bracket in the interactive proof assistant called Isabelle proof assistant. We further obtain a machine checked proof of invariance of Kauffman bracket.
 
Contributor Gadgil, Siddhartha
 
Date 2018-01-31T07:57:26Z
2018-01-31T07:57:26Z
2018-01-31
2014
 
Type Thesis
 
Identifier http://hdl.handle.net/2005/3052
http://etd.ncsi.iisc.ernet.in/abstracts/3916/G26934-Abs.pdf
 
Language en_US
 
Relation G26934