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

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.