{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article1302","name":"Proof Presentation","abstract":"The talk is based on a book about the human-oriented presentation of a mathematical proof in natural\r\nlanguage, in a style as we may find it in a typical mathematical text book.\r\nHow can a proof be other than human-oriented?\r\nWhat we have in mind is a deduction systems, which is implemented on a computer,\r\nthat proves \u2013 with some human interaction \u2013 a mathematical textbook as may be used\r\nin an undergraduate course. The proofs generated by these systems today are far from\r\nbeing human-oriented and can in general only be read by an expert in the respective\r\nfield: proofs between several hundred (for a common mathematical theorem), for more\r\nthan a thousand steps (for an unusually difficult theorem) and more than ten thousand\r\ndeduction steps (in a program verification task) are not uncommon.\r\nAlthough these proofs are provably correct, they are typically marred by many problems:\r\nto start with, that are usually written in a highly specialised logic such as the\r\nresolution calculus, in a matrix format, or even worse, they may be generated by a\r\nmodel checker. Moreover they record every logical step that may be necessary for the\r\nminute detail of some term transformation (such as, for example, the rearrangement of\r\nbrackets) along side those arguments, a mathematician would call important steps or\r\nheureka-steps that capture the main idea of the proof. Only these would he be willing\r\nto communicate to his fellow mathematicians \u2013 provided they have a similar academic\r\nbackground and work in the same mathematical discipline. If not, i.e. if the proof was\r\nwritten say for an undergraduate textbook, the option of an important step may be\r\nviewed differently depending on the intended reader.\r\nNow, even if we were able to isolate the ten important steps \u2013 out of those hundreds\r\nof machine generated proof steps \u2013 there would still be the startling problem\r\nthat they are usually written in the \"wrong\" order. A human reader might say: \"they do\r\nnot have a logical structure\"; which is to say that of course they follow a logical pattern\r\n(as they are correctly generated by a machine), but, given the convention of the respective\r\nfield and the way the trained mathematician in this field is used to communicate,\r\nthey are somewhat strange and ill structured.\r\nAnd finally, there is the problem that proofs are purely formal and recorded in a\r\npredicate logic that is very far from the usual presentation that relies on a mixture\r\nof natural language arguments interspersed with some formalism.\r\nThe book (about 800 page) which gives an answer to some of these problems is to appear with Elsevier","keywords":["Artificial intelligence","mathematics","proof presentation"],"author":{"@type":"Person","name":"Siekmann, J\u00f6rg","givenName":"J\u00f6rg","familyName":"Siekmann"},"position":5,"pageStart":1,"pageEnd":7,"dateCreated":"2006-05-08","datePublished":"2006-05-08","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":{"@type":"Person","name":"Siekmann, J\u00f6rg","givenName":"J\u00f6rg","familyName":"Siekmann"},"copyrightYear":"2006","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.05431.5","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume587","volumeNumber":5431,"name":"Dagstuhl Seminar Proceedings, Volume 5431","dateCreated":"2006-04-25","datePublished":"2006-04-25","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article1302","isPartOf":{"@type":"Periodical","@id":"#series119","name":"Dagstuhl Seminar Proceedings","issn":"1862-4405","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume587"}}}