Generation and presentation of formal mathematical documents
The aim of this Ph.D. thesis is to explore the role that could play the computer mathematics field in the development of mathematics. Chapter 2 of the book presents a gentle introduction to type theoretical theorem proving, and argues that type theory could be a good candidate for the language devoted to encode the formal mathematical discourse. This chapter exposes, as concrete type theory, the calculus of inductive constructions, the system standing behind the Coq theorem prover. Chapter 3 investigates computations in theorem provers, with an application to automated theorem proving for certain classes of problems, on the basis of reflection method. Chapter 4 describes an implementation of a tool which presents formalized mathematical theories as interactive natural language mathematical documents. Chapter 5 demonstrates that theroem proving and computer algebra systems can be combined to get efficient albeit formal proofs. This demonstration is supported by a generator which automatically produces proofs of primality that are formally verifiable. The Pocklington's criterion for testing primality of numbers is used to produce the primality proofs. The final Chapter 6 presents the conclusions of this thesis, emphasizing the new proposed approach and the obtained results.
This page was built for publication: Generation and presentation of formal mathematical documents
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2760868)
