Search Results

Documents authored by Siekmann, Jörg


Document
Proof Presentation

Authors: Jörg Siekmann

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)


Abstract
The talk is based on a book about the human-oriented 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 human-oriented? 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 human-oriented 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 heureka-steps 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

Cite as

Jörg Siekmann. Proof Presentation. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{siekmann:DagSemProc.05431.5,
  author =	{Siekmann, J\"{o}rg},
  title =	{{Proof Presentation}},
  booktitle =	{Deduction and Applications},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.5},
  URN =		{urn:nbn:de:0030-drops-5611},
  doi =		{10.4230/DagSemProc.05431.5},
  annote =	{Keywords: Artificial intelligence, mathematics, proof presentation}
}
Document
6th International Workshop on Unification (Dagstuhl Seminar 9231)

Authors: Franz Baader, Jörg Siekmann, and Wayne Snyder

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Franz Baader, Jörg Siekmann, and Wayne Snyder. 6th International Workshop on Unification (Dagstuhl Seminar 9231). Dagstuhl Seminar Report 42, pp. 1-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)


Copy BibTex To Clipboard

@TechReport{baader_et_al:DagSemRep.42,
  author =	{Baader, Franz and Siekmann, J\"{o}rg and Snyder, Wayne},
  title =	{{6th International Workshop on Unification (Dagstuhl Seminar 9231)}},
  pages =	{1--32},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{42},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.42},
  URN =		{urn:nbn:de:0030-drops-149301},
  doi =		{10.4230/DagSemRep.42},
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail