Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

2006-01-01

Filename

wucse-2006-24.pdf

DOI:

10.7936/K79Z9344

Technical Report Number

WUCSE-2006-24

Abstract

The notion of a proof is central to all of mathematics. In the language of formal logic, a proof is a finite sequence of inferences from a set of axioms, and any statement one yields from such a finitistic procedure is called a theorem. For better or for worse, this is far from the form a traditional mathematical proof takes. Mathematicians write proofs that omit routine logical steps, and details deemed tangential to the central result are often elided. These proofs are fuzzy and human-centric, and a great amount of context is assumed on the part of the reader. While traditional proofs are not overly symbolic or syntactic, and hence are easily understood, such informal proofs are susceptible to logical errors -- Fermat's Last Theorem and the Four Color Theorem being prime examples. In light of this, there has been significant interest in producing formal proofs of mathematical theorems: proofs in which every intermediate logical step is supplied. Drawing on ideas from Computational Logic, Type Theory and the theory of Automated Deduction, we are able to guaranteed the correctness of these proofs. The formalization of mathematics is an endeavor that has enjoyed very encouraging progress in recent years. Major achievements include the complete formalization of the Four Color Theorem, the Prime Number Theorem, Goedel's Incompleteness Theorem, the Jordan Curve Theorem (all within the past five years!). This thesis presents our work in formalizing the meta-theory of Peter Andrews' classical higher-order logic in a higher-order typed lambda calculus. Our development is a completely formal one -- in addition to formalizing logical meta-theory, we have also developed and formalized the syntactic meta-theory. Our syntactic meta-theory allows for the reasoning of notions such as variable occurrences, scope and variable binding, linear replacement, etc. Our formalization is carried out in the interactive proof assistant Coq, developed as part of the LogiCal Project in INRIA. Coq is built upon the Calculus of Inductive Constructions, an extension of Coquand and Huet's seminal Calculus of Construction with support for inductive data types. As far as we know, this thesis presents the first effort to formalize Andrews' logical system.

Comments

Permanent URL: http://dx.doi.org/10.7936/K79Z9344

Download

Share

COinS