PL EN


2010 | 22(35) | 95-112
Article title

THE ALGORITHMS FOR IMPROVING AND REORGANIZING NATURAL DEDUCTION PROOFS

Authors
Selected contents from this journal
Title variants
Languages of publication
EN
Abstracts
EN
It can be observed in the course of analyzing nontrivial examples of natural deduction proofs, either declarative or procedural, that the proofs are often formulated in a chaotic way. Authors tend to create deductions which are correct for computers, but hardly readable for humans, as they believe that finding and removing inessential reasoning fragments, or shortening the proofs is not so important as long as the computer accepts the proof script. This article consists of two parts. In the first part, we present some types of unnecessary deductions and methods of reorganizing proof graphs in order to make them closer to good quality informal mathematical reasoning. In the second part, we describe tools implemented to solve the above-mentioned problems. Next, we demonstrate their usability by analysing statistical data drawn from the Mizar Mathematical Library.
Keywords
Year
Issue
Pages
95-112
Physical description
Document type
ARTICLE
Contributors
author
  • Karol Pak, University of Bialystok, Institute of Computer Science, Bialystok, Poland
References
Document Type
Publication order reference
Identifiers
CEJSH db identifier
11PLAAAA101626
YADDA identifier
bwmeta1.element.12b70df8-d149-38de-8ac1-286794222cbe
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.