THE ALGORITHMS FOR IMPROVING AND REORGANIZING NATURAL DEDUCTION PROOFS

• Autorzy: Pak Karol
• Języki publikacji: EN

Abstrakty

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.

Słowa kluczowe

EN

NATURAL DEDUCTION; PROOF

• Wydawca: Bialystok University Press
• Czasopismo: Studies in Logic, Grammar and Rhetoric
• Rocznik: 2010
• Numer: 22(35)
• Strony: 95-112
• Rodzaj publikacji: ARTICLE

Twórcy

autor

Pak Karol

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

Identyfikatory

CEJSH db identifier

11PLAAAA101626