Abstract
The talk is based on a book about the humanoriented presentation of a mathematical proof in natural
language, in a style as we may find it in a typical mathematical text book.
How can a proof be other than humanoriented?
What we have in mind is a deduction systems, which is implemented on a computer,
that provesĂ˘â‚¬â€ťwith some human interactionĂ˘â‚¬â€ťa mathematical textbook as may be used
in an undergraduate course. The proofs generated by these systems today are far from
being humanoriented and can in general only be read by an expert in the respective
field: proofs between several hundred (for a common mathematical theorem), for more
than a thousand steps (for an unusually difficult theorem) and more than ten thousand
deduction steps (in a program verification task) are not uncommon.
Although these proofs are provably correct,they are typically marred by many problems:
to start with, that are usually written in a highly specialised logic such as the
resolution calculus, in a matrix format, or even worse, they may be generated by a
model checker. Moreover they record every logical step that may be necessary for the
minute detail of some term transformation (such as, for example, the rearrangement of
brackets) along side those arguments, a mathematician would call important steps or
heurekasteps that capture the main idea of the proof. Only these would he be willing
to communicate to his fellow mathematiciansĂ˘â‚¬â€ťprovided they have a similar academic
background and work in the same mathematical discipline. If not, i.e. if the proof was
written say for an undergraduate textbook, the option of an important step may be
viewed differently depending on the intended reader.
Now, even if we were able to isolate the ten important steps Ă˘â‚¬â€ť out of those hundreds
of machine generated proof steps Ă˘â‚¬â€ť there would still be the startling problem
that they are usually written in the Ă˘â‚¬ËśwrongĂ˘â‚¬â„˘ order. A human reader might say: Ă˘â‚¬Ëśthey do
not have a logical structureĂ˘â‚¬â„˘; which is to say that of course they follow a logical pattern
(as they are correctly generated by a machine), but, given the convention of the respective
field and the way the trained mathematician in this field is used to communicate,
they are somewhat strange and ill structured.
And finally, there is the problem that proofs are purely formal and recorded in a
predicate logic that is very far from the usual presentation that relies on a mixture
of natural language arguments interspersed with some formalism.
The book ( about 800 page) which gives an answer to some of these problems is to appear with Elsevier
BibTeX  Entry
@InProceedings{siekmann:DSP:2006:561,
author = {J{\"o}rg Siekmann},
title = {Proof Presentation},
booktitle = {Deduction and Applications},
year = {2006},
editor = {Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
number = {05431},
series = {Dagstuhl Seminar Proceedings},
ISSN = {18624405},
publisher = {Internationales Begegnungs und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2006/561},
annote = {Keywords: Artificial intelligence, mathematics, proof presentation}
}
Keywords: 

Artificial intelligence, mathematics, proof presentation 
Seminar: 

05431  Deduction and Applications 
Issue Date: 

2006 
Date of publication: 

08.05.2006 