1) La descarga del recurso depende de la página de origen
2) Para poder descargar el recurso, es necesario ser usuario registrado en Universia

Opción 1: Descargar recurso

Opción 2: Descargar recurso

Detalles del recurso


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.

Pertenece a

ETD at Indian Institute of Science  


Prathamesh, Turga Venkata Hanumantha - 

Id.: 70950701

Idioma: inglés (Estados Unidos)  - 

Versión: 1.0

Estado: Final

Palabras claveKnot Theory - 

Tipo de recurso: Thesis  - 

Tipo de Interactividad: Expositivo

Nivel de Interactividad: muy bajo

Audiencia: Estudiante  -  Profesor  -  Autor  - 

Estructura: Atomic

Coste: no

Copyright: sí

Requerimientos técnicos:  Browser: Any - 

Relación: [References] G26934

Fecha de contribución: 01-feb-2018



Otros recursos que te pueden interesar

  1. Concordance and mutation We provide a framework for studying the interplay between concordance and positive mutation and iden...
  2. Span of the Jones polynomial of an alternating virtual link For an oriented virtual link, L H Kauffman defined the [math] –polynomial (Jones polynomial). The su...
  3. Relationships between braid length and the number of braid strands For a knot [math] , let [math] be the minimum length of an [math] –stranded braid representative of ...
  4. Klein links and related torus links In this paper, we present our constructions and results leading up to our discovery of a class of Kl...
  5. A simplification of grid equivalence In the work of Cromwell and Dynnikov, grid equivalence is given by the grid moves commutation, (de-)...

Otros recursos de la mismacolección

  1. Compactness Theorems for The Spaces of Distance Measure Spaces and Riemann Surface Laminations Gromov’s compactness theorem for metric spaces, a compactness theorem for the space of compact metri...
  2. A Formal Proof of Feit-Higman Theorem in Agda In this thesis we present a formalization of the combinatorial part of the proof of Feit-Higman theo...
  3. A Posteriori Error Analysis of Discontinuous Galerkin Methods for Elliptic Variational Inequalities The main emphasis of this thesis is to study a posteriori error analysis of discontinuous Galerkin (...
  4. Central and Peripheral Correlates of Motor Planning A hallmark of human behaviour is that we can either couple or decouple our thoughts, decision and mo...
  5. Eigenvalues of Products of Random Matrices In this thesis, we study the exact eigenvalue distribution of product of independent rectangular com...

Aviso de cookies: Usamos cookies propias y de terceros para mejorar nuestros servicios, para análisis estadístico y para mostrarle publicidad. Si continua navegando consideramos que acepta su uso en los términos establecidos en la Política de cookies.