Writing and checking complete proofs in LaTeX

Video in TIB AV-Portal: Writing and checking complete proofs in LaTeX

Formal Metadata

Title
Writing and checking complete proofs in LaTeX
Title of Series
Part Number
18
Number of Parts
28
Author
License
CC Attribution - NoDerivatives 2.0 UK: England & Wales:
You are free to use, copy, distribute and transmit the work or content in unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
2012
Language
English
Production Place
Indiana, USA

Content Metadata

Subject Area
Abstract
ProofCheck is a system for writing and checking mathematical proofs. Theorems and proofs are contained in a plain or document. Parsing and proof checking are accomplished through Python programs which read the source file. A general explanation of the use and structure of the system and programs is provided and a sample proof is shown in detail. The work done by the authors has been based on standard sentence logic, a non-standard predicate logic and set theory with proper classes. Theorems and proofs based on other foundations may be checked if external data files are modified. Four such data files and their possible modifications are described. In addition, the extent to which the formal language can be shaped to accommodate an author's preferences is discussed.
Feedback