THE ALGORITHMS FOR IMPROVING AND REORGANIZING NATURAL DEDUCTION PROOFS

• Authors: Pak Karol
• 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

EN

NATURAL DEDUCTION; PROOF

Discipline

• OTHER_SOCIAL_SCIENCES: OTHER SOCIAL SCIENCES

• Publisher: Sciendo
• Journal: Studies in Logic, Grammar and Rhetoric
• Year: 2010
• Issue: 22(35)
• Pages: 95-112
• Document type: ARTICLE

Contributors

author

Pak Karol

• Karol Pak, University of Bialystok, Institute of Computer Science, Bialystok, Poland

Identifiers

CEJSH db identifier

11PLAAAA101626