Mechanising knot Theory
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...
Main Author: | |
---|---|
Other Authors: | |
Language: | en_US |
Published: |
2018
|
Subjects: | |
Online Access: | http://hdl.handle.net/2005/3052 http://etd.ncsi.iisc.ernet.in/abstracts/3916/G26934-Abs.pdf |
id |
ndltd-IISc-oai-etd.ncsi.iisc.ernet.in-2005-3052 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-IISc-oai-etd.ncsi.iisc.ernet.in-2005-30522018-02-01T03:34:53ZMechanising knot TheoryPrathamesh, Turga Venkata HanumanthaKnot TheoryTheorem ProvingFormal Theorem ProvingKauffman BracketLink TheoryFirst Order LogicTanglesMatricesFormalising Knot TheorySymbolic and Mathematical LogicKnotsBraidsMathematicsMechanisation 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.Gadgil, Siddhartha2018-01-31T07:57:26Z2018-01-31T07:57:26Z2018-01-312014Thesishttp://hdl.handle.net/2005/3052http://etd.ncsi.iisc.ernet.in/abstracts/3916/G26934-Abs.pdfen_USG26934 |
collection |
NDLTD |
language |
en_US |
sources |
NDLTD |
topic |
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 |
spellingShingle |
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 Prathamesh, Turga Venkata Hanumantha Mechanising knot Theory |
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. |
author2 |
Gadgil, Siddhartha |
author_facet |
Gadgil, Siddhartha Prathamesh, Turga Venkata Hanumantha |
author |
Prathamesh, Turga Venkata Hanumantha |
author_sort |
Prathamesh, Turga Venkata Hanumantha |
title |
Mechanising knot Theory |
title_short |
Mechanising knot Theory |
title_full |
Mechanising knot Theory |
title_fullStr |
Mechanising knot Theory |
title_full_unstemmed |
Mechanising knot Theory |
title_sort |
mechanising knot theory |
publishDate |
2018 |
url |
http://hdl.handle.net/2005/3052 http://etd.ncsi.iisc.ernet.in/abstracts/3916/G26934-Abs.pdf |
work_keys_str_mv |
AT prathameshturgavenkatahanumantha mechanisingknottheory |
_version_ |
1718612255051874304 |