Add to Watchlist

Writing and checking complete proofs in LaTeX


Citation of segment
Embed Code
Purchasing a DVD Cite video

For this video, there are no automatic analysis results.

Analysis results are only provided—where legally permissible—for videos from the realms of technology/engineering, architecture, chemistry, information technology, mathematics, and physics.


Formal Metadata

Title Writing and checking complete proofs in LaTeX
Title of Series The 30th Annual Meeting of the TeX Users Group (TUG 2009)
Part Number 18
Number of Parts 28
Author Neveln, Bob
Alps, Bob
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.
DOI 10.5446/30837
Publisher River Valley TV
Release Date 2012
Language English
Production Place Indiana, USA

Content Metadata

Subject Area Information technology
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.


AV-Portal 3.5.0 (cb7a58240982536f976b3fae0db2d7d34ae7e46b)


  305 ms - page object