velikost textu

# Verefication of Mathematical Proofs

Upozornění: Informace získané z popisných dat či souborů uložených v Repozitáři závěrečných prací nemohou být použity k výdělečným účelům nebo vydávány za studijní, vědeckou nebo jinou tvůrčí činnost jiné osoby než autora.
Název:
Verefication of Mathematical Proofs
Typ:
Disertační práce
Autor:
RNDr. Petr Pudlák, Ph.D.
Školitel:
prof. RNDr. Petr Štěpánek, DrSc.
Oponenti:
RNDr. Zuzana Haniková, Ph.D.
Martin Plátek, CSc.
Id práce:
39795
Fakulta:
Matematicko-fyzikální fakulta (MFF)
Pracoviště:
Katedra teoretické informatiky a matematické logiky (32-KTIML)
Program studia:
Informatika (P1801)
Obor studia:
Teoretická informatika (I1)
Přidělovaný titul:
Ph.D.
Datum obhajoby:
7. 3. 2007
Výsledek obhajoby:
Prospěl/a
Jazyk práce:
Angličtina
Abstract v angličtině:
In this thesis we deal with the problem of automatic proving (or disproving) mathematical conjectures using computer programs (usually called automated theorem provers). We address several issues that are important for a successful utilization of such programs. In Chapter 3 we examine how to store and reuse important pieces of mathematical knowledge in the form of lemmas. We investigate how this process can be automatized, i.e. how a computer can construct and use lemmas without human guidance. The program we develop tries to shorten or to speed up the proofs of several conjectures from a common theory. It repeatedly extracts lemmas from the proofs it has already completed and uses the lemmas to improve the sets of premisses to produce more efficient proofs of the conjectures. In Chapter 4 we develop a new algorithm that tries to construct the optimal sets of premisses for proving and disproving mathematical conjectures. The algorithm semantically analyzes the conjectures and the set of premisses of the given theory to find the optimal subsets of the premisses. The algorithm uses an automated model finder to construct models that serve as counterexamples that guide the algorithm to find the optimal set of premisses. In Chapter 5 we use the algorithm to decide formulae in a wide range of modal systems. We develop an axiomatization of the modal system S1 that is based on equivalences. Then we use this basis to construct algebras in which we can decide the validity of modal formulae and rules in various extensions of S1. Finally we use the algorithm from Chapter 4 to automatically decide the validity of almost 50 formulae and rules in over 30 modal systems and to decide the relationships between the systems.
Dokumenty
Stáhnout Dokument Autor Typ Velikost
Text práce RNDr. Petr Pudlák, Ph.D. 727 kB
Abstrakt v českém jazyce RNDr. Petr Pudlák, Ph.D. 80 kB
Abstrakt anglicky RNDr. Petr Pudlák, Ph.D. 81 kB
Posudek vedoucího prof. RNDr. Petr Štěpánek, DrSc. 240 kB
Posudek oponenta RNDr. Zuzana Haniková, Ph.D. 233 kB
Posudek oponenta Martin Plátek, CSc. 207 kB
Záznam o průběhu obhajoby 213 kB