Please use this identifier to cite or link to this item: http://www.repositorio.ufc.br/handle/riufc/36069
Title in Portuguese: Matemática feita no computador: estudos sobre uma coleção de sistemas formais, com uma investigação sobre estruturas indutivas, e a separação entre lógica e automação em assistentes de prova
Title: Mathematics made on computers: Studies on a collection of formal systems, with an investigation on inductive structures and the separation between logic and automation in proof assistants
Author: Paula, Hugo Carvalho de
Advisor(s): Brito, Carlos Eduardo Fisch de
Keywords: Assistentes de prova
Computação
Fundamentos da matemática
Teoria dos tipos
Lógica
Issue Date: 2018
Citation: PAULA, Hugo Carvalho de. Matemática feita no computador: estudos sobre uma coleção de sistemas formais, com uma investigação sobre estruturas indutivas, e a separação entre lógica e automação em assistentes de prova. 2018. 67 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Ceará, Fortaleza, 2018.
Abstract in Portuguese: Este trabalho desenvolve um estudo de uma sequência de sistemas formais, com o propósito de investigar a relação entre computação e matemática, e apresenta uma possível nova direção para o desenvolvimento de assistentes de prova. O ponto de partida é o Cálculo Lambda Simplesmente Tipado, e sucessivas extensões são tratadas, culminando no CoqMT. O trabalho trata apenas de alguns aspectos de cada sistema, como a matemática neles realizável, e como que computação neles se manifesta. Embora existam discussões independentes de cada um desses sistemas, aqui há uma ênfase na visão desses sistemas como uma sequência propriamente dita, o que possibilita uma discussão clara de ideias recorrentes. Com base em tais ideias, a dissertação apresenta o que chamamos de "estruturas indutivas", uma generalização de conceitos encontrados no Cálculo das Construções Indutivas. A dissertação conclui com exemplos que ilustram o uso de computação na presença dessas estruturas, e esboça uma implementação com base em trabalhos pré-existentes da literatura.
Abstract: This work develops a study of a sequence of formal systems, with the objective of investigating the relationship between computation and mathematics, and presents a possible new direction for the development of new proof assistants. The starting point is the Simply Typed Lambda Calculus, and successive extensions are presented, culminating with CoqMT. This work deals only with some aspects of each system, such as the mathematics they capture, and how computation manifests in those systems. Although there are independent discussions of each of those systems elsewhere, here there is an emphasis in the view of the systems as a proper sequence, which enables a clear discussion of recurring ideas. Based on those ideas, this dissertation presents what we called "inductive structures", a generalization of concepts found in the Calculus of Inductive Constructions. This dissertation concludes with examples that illustrate the usage of computation in the presence of such structures, and outlines an implementation based on pre-existing works in the literature.
URI: http://www.repositorio.ufc.br/handle/riufc/36069
metadata.dc.type: Dissertação
Appears in Collections:DCOMP - Dissertações defendidas na UFC

Files in This Item:
File Description SizeFormat 
2018_dis_hcpaula.pdf570,47 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.