TY - GEN
T1 - On communicating proofs in interactive mathematical documents
AU - Caprotti, O.
AU - Oostdijk, M.D.
PY - 2001
Y1 - 2001
N2 - There is a wealth of interactive mathematics available on the web. Examples range from animated geometry to computing the nth digit in the expansion of p. However, proofs seem to remain static and at most they provide interaction in the form of links to definitions and other proofs. In this paper, we want to show how interactivity can be included in proofs themselves by making them executable, human-readable, and yet formal. The basic ingredients are formal proof-objects, OpenMathrelated languages, and the latest eXtensible Markup Language (XML) technology. We exhibit, by an example taken from a formal development in number theory, the final product of which we believe to be a truly interactive mathematical document.
AB - There is a wealth of interactive mathematics available on the web. Examples range from animated geometry to computing the nth digit in the expansion of p. However, proofs seem to remain static and at most they provide interaction in the form of links to definitions and other proofs. In this paper, we want to show how interactivity can be included in proofs themselves by making them executable, human-readable, and yet formal. The basic ingredients are formal proof-objects, OpenMathrelated languages, and the latest eXtensible Markup Language (XML) technology. We exhibit, by an example taken from a formal development in number theory, the final product of which we believe to be a truly interactive mathematical document.
U2 - 10.1007/3-540-44990-6_4
DO - 10.1007/3-540-44990-6_4
M3 - Conference contribution
SN - 3-540-42071-1
T3 - Lecture Notes in Computer Science
SP - 53
EP - 64
BT - Artificial Intelligence and Symbolic Computation (AISC 2000, Madrid, Spain, July 17-19, 2000, Revised Papers)
A2 - Campbell, J.A.
A2 - Roanes-Lozano, E.
PB - Springer
CY - Berlin
ER -