PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2010 | 22(35) | 95-112
Tytuł artykułu

THE ALGORITHMS FOR IMPROVING AND REORGANIZING NATURAL DEDUCTION PROOFS

Autorzy
Wybrane pełne teksty z tego czasopisma
Warianty tytułu
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
Rocznik
Numer
Strony
95-112
Opis fizyczny
Rodzaj publikacji
ARTICLE
Twórcy
autor
  • Karol Pak, University of Bialystok, Institute of Computer Science, Bialystok, Poland
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
CEJSH db identifier
11PLAAAA101626
Identyfikator YADDA
bwmeta1.element.12b70df8-d149-38de-8ac1-286794222cbe
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.