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 way 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 Infinite Braid Group. 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 Isabelle Proof Assistant. We formulate equivalence of Links in Higher Order Logic. We obtain a construction of Kauffman Bracket in the Isabelle Proof Assistant. We further obtain a machine checked proof of invariance of Kauffman Bracket.

- All seminars.
- Seminars for 2014

Last updated: 06 Mar 2020