Algorytmy poprawy czytelności formalnych rozumowań zapisanych w systemie naturalnej dedukcji

Przedmiotem badań opisanych w rozprawie doktorskiej są metody poprawy czytelności formalnych rozumowań zapisanych w systemie naturalnej dedukcji. Wykorzystanie komputerowej weryfikacji jest znanym narzędziem ułatwiającym sprawdzanie poprawności formułowanych rozumowań, aczkolwiek jakiekolwiek próby analizowania tak uszczegółowionych rozumowań są wyjątkowo trudne, a zdaniem niektórych niemożliwe. Czytelność takich wywodów jest pojęciem subiektywnym, różnie rozumianym przez poszczególnych autorów rozumowań. Analiza ich potrzeb przyczyniła się jednak do wyodrębnienia grupy kryteriów umożliwiających uczytelnienie formalnych rozumowań, poprzez upodabnienie ich postaci do takiej, która występuje w nieformalnych dowodach matematycznych. W pierwszej części rozprawy został przedstawiony model abstrakcyjnego dowodu matematycznego odzwierciedlający rzeczywistą strukturę dowodów zapisanych w języku Mizar. Model ten umożliwia interpretowanie przepływu informacji w rozumowaniu jako szczególnego rodzaju skierowanych grafów acyklicznych. W oparciu o ten model w drugiej części rozprawy zostały formalnie opracowane pojęcia oraz wyznaczniki poprawy czytelności. Uczytelnianie formalnych rozumowań zostało zbadane pod kątem zastosowania dwóch rodzajów środków stosowanych w praktyce matematycznej. Jako pierwszy z nich, zostały zbadane metody odnajdywania lokalnych podrozumowań, a następnie ich wyizolowywania (wyodrębniania) w postaci lematów lub kapsułkowaniu na głębszych poziomach zagnieżdżenia. Drugim zaś analizowanym środkiem była reorganizacja niezależnych od siebie kroków rozumowań w sposobie ich uporządkowania w dowodzie, mająca na celu poprawę wybranych własności linearyzacji dowodu. W wyniku przeprowadzonych badań w zakresie pierwszego środka została skonstruowana metoda wyizolowywania i kapsułkowania fragmentów rozumowania przy zachowaniu poprawności modyfikowanego skryptu dowodowego oraz zostały zbadane własności fragmentów dowodu, które determinują budowę stwierdzenia opisującego rozumowanie zawarte w tych fragmentach. W zakresie zaś drugiego środka zostało opracowane pięć, najczęściej wskazywanych przez użytkowników bazy Mizar Mathematical Library wskaźników czytelności. Przeprowadzone badania nad złożonością problemu optymalizacji wartości przyjętych wskaźników wykazały, że optymalizacja czterech z nich wiąże się z rozwiązywaniem problemów NP--trudnych. Dodatkowo, zostały stworzone programy umożliwiające automatyczną poprawę czytelności skryptów dowodowych zapisanych w języku Mizar, których działanie opiera się na optymalizacji wartości opracowanych wskaźników przy zadanej przez użytkownika hierarchii ich ważności.

In this dissertation the methods to improve legibility of existing formal reasonings written in natural deduction are presented. Computer assisted proof development frameworks can check the correctness of such reasonings, but any attempt to analyze details of the proofs scripts created in this way, according to opinion of some proof writers, is extremely difficult or even impossible. The readability of such arguments is a~subjective quality which is understood by different proof writers in different ways. Still the analysis of their needs led to a~distinguished set of criteria that facilitate making the formal deductions closer to the informal mathematical proofs. First part of the dissertation describes an abstract model of mathematical proofs written in the Mizar language. This model expresses the intuitions connected with the reasonings, where the information flow in proof is regarded as a special kind of digraph. Based on this model notion and parameters associated with legibility criteria are formally defined in the second part of the dissertation. Improvement of readability has been realised by two separate approaches that are used in informal mathematical practice. The first approach is based on the finding fragments of reasoning and consists in isolation (extraction) of these fragments in the form of\break lemmas or encapsulation at the deeper levels of nested proof. The second approach to improvement of the readability consists in the modification of the order of independent steps written in the proof script. The methods that reorganize the order of steps focus mainly on the location of information used to justify a step. As a result of research based on the first approach, methods to extract or encapsulate reasoning fragments from existing deductions were elaborated. Also properties of reasoning fragments that determine the structure of statements which describing the information about reasoning contained in these fragments were described. In the second approach five parameters of legibility that are indicated as most important by the users users of Mizar database has been formally defined. Analysis of the proposed parameters related to improvement of proof readability revealed that four of the considered problems are NP-complete. Additionally, an auxiliary application to improve the readability of articles distributed in MML based on the most popular hierarchy of the considered parameters were created.