Open AccessFaithfully Reflecting the Structure of Informal Mathematical Proofs into Formal Type Theories
Author(s) -
Gueorgui Jojgov,
Rob Nederpelt,
M. Scheffer
Publication year - 2004
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2003.12.030
Subject(s) - mathematical proof , proof assistant , type theory , structural proof theory , computer science , notation , type (biology) , mathematical notation , proof theory , calculus (dental) , formal proof , natural deduction , mathematics , algebra over a field , programming language , theoretical computer science , pure mathematics , arithmetic , medicine , ecology , geometry , dentistry , biology
Mathematical proofs, as written in every-day Common Mathematical Language (CML), are informal and many details are left implicit. To check such proofs with a proof assistant they need to be formalized and elaborated to full detail. In order to reduce the possibility of formalization errors and therefore increase the reliability of the translation of CML texts into type theories, we use a version of Nederpelt's formal language WTT extended with logical notation that encodes the natural deduction proof steps. By using this intermediate version, the subsequent translation into a full-fledged type theory can be made such that the proof clearly reflects the structure of the original CML proof. This makes it easier to ensure that the formalization of the CML text is done correctly, and offers additional advantages over usual representations of proof terms in type theory
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom