|
|
Pojem interpretace axiomatických teorií
Štefanišin, Jan ; Švejdar, Vítězslav (vedoucí práce) ; Haniková, Zuzana (oponent)
Práce: Pojem interpretace axiomatických teorií Autor: Jan Štefanišin Abstrakt: V této práci se zabýváme konceptem interpretovatelnosti axiomatic- kých teorií (interpretovaní jedné teorie v druhé) a jeho základními vlastnostmi a využitími. Definujeme interpretaci a ukážeme její chování na jednoduchých školních teoriích a dokážeme o ní několik vět. V dalších dvou kapitolách ukážeme příklady na složitějších teoriích. Použijeme interpretace k dokazování podstatné nerozhodnutelnosti teorií pomocí interpretace teorie R v těchto teoriích. Pak se budeme věnovat možnému využití interpretací ve finitistním programu Edwarda Nelsona a s tím související lokální interpretaci omezené aritmetiky I∆0 v Robin- sonově aritmetice Q, což je také příklad řezové interpretace. Nakonec se vrátíme k jednoduchým školním teoriím a ukážeme na nich, jak dokazovat neinterpreto- vatelnost. Klíčová slova: interpretace, axiomatická teorie, interpretovatelnost, definovatelná množina, Robinsonova aritmetika
|
|
|
Pojem interpretace axiomatických teorií
Štefanišin, Jan ; Švejdar, Vítězslav (vedoucí práce) ; Haniková, Zuzana (oponent)
V této práci se zabýváme konceptem interpretovatelnosti axiomatic- kých teorií (interpretovaní jedné teorie v druhé) a jeho základní vlastnostmi a využitími a jeho různými variantami. Definujeme jedno-dimenzionální interpre- taci a ukážeme její chování na jednoduchých teoriích. Následně definujeme více- dimenzionální interpretaci a interpretaci po částech a využijeme je k sestavení uspořádání teorií podle relace interpretace do takzvaných stupňů - konkrétně do Double Degree struktur. Jedno-dimenzionální interpretace použijeme k dokazo- vání podstatné nerozhodnutelnosti teorií pomocí interpretováním teorie R v těchto teoriích. Nakonec se budeme věnovat možnému využití interpretací ve finitistním programu Edvarda Nelsona a s tím související lokální interpretaci omezené arit- metiky I∆0 v Robinsonově aritmetice Q, což je také příklad řezové interpretace. Klíčová slova: interpretace, axiomatická teorie, interpretovatelnost, definovatelná množina, Robinsonova aritmetika
|
|
| |
|
|
Verefication of Mathematical Proofs
Pudlák, Petr ; Štěpánek, Petr (vedoucí práce) ; Haniková, Zuzana (oponent) ; Plátek, Martin (oponent)
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...
|
|
|
Kambodža po roce 1979 a aplikace Reaganovy doktríny
Haniková, Zuzana ; Hornát, Jan (vedoucí práce) ; Bečka, Jan (oponent)
Bakalářská práce se zabývá vývojem v Kambodži po roce 1979 a Reaganovou doktrínou, která v 80. letech byla aplikována i na Kambodžu. Vietnamská invaze nejenom ukončila krutou vládu Rudých Khmerů, ale také ovlivnila další vývoj na více než desetiletí. Země byla ovládána Vietnamem, který byl významným spojencem Sovětského svazu. Pro Spojené státy bylo nepřijatelné, aby se sovětský vliv dále rozšiřoval a v rámci Reaganovy doktríny se rozhodly podporovat antikomunistické skupiny v zemích třetího světa. Práce analyzuje americkou podporu nekomunistickému hnutí v Kambodži a zabývá se otázkou, jaké důvody vedly USA k jejich podpoře a jaký vliv měly na mírové uspořádání a odchod vietnamských jednotek ze země. Na základě sledování rozhodování USA, mezinárodních jednání a i vnitropolitického vývoje v Kambodži práce dochází k závěru, že motivem pro zapojení byl strach z rostoucího sovětského vliv, ale role Spojených států byla omezená a po dobu vlády prezidenta Reagana velmi pasivní. To bylo způsobeno například malým zájmem o situaci v Kambodži a obavami z výsledku v případě přímého konfliktu po negativní zkušenosti z Vietnamu. Také se šířily zprávy, že z asistence čerpají prostředky i Rudí Khmerové, kteří byli nejsilnější resistenční skupinou, ale jedním z cílů Washingtonu bylo zabránit jejich návratu k moci....
|
|
|
Systémy morfismů nad Gödelovou fuzzy logikou
Luhan, Ondřej ; Běhounek, Libor (vedoucí práce) ; Haniková, Zuzana (oponent)
V práci jsou zavedeny některé velice základní pojmy teorie kategorií budované nad prvořádovou Gödelovou fuzzy logikou (s ostrou rovností a delta operá- torem). Fuzzy varianta klasického pojmu kategorie je uvážena. Následně je defi- nováno a prozkoumáno několik systémů morfismů volně vycházejících z ostrých kategorií Rel a Set. Všechny uvažované systémy tudíž obsahují fuzzy množiny jako objekty a různé druhy binárních fuzzy relací jako morfismy. Náš přístup je logicky-založené stupňované zobecnění ostrých (klasických) kategoriálně-teore- tických přístupů k fuzzy množinám, které byly iniciovány Goguenem. 1
|
|
|
Generalized Boolean models and classical predicate logic
Lávička, Tomáš ; Honzík, Radek (vedoucí práce) ; Haniková, Zuzana (oponent)
Tato bakalářská práce pojednává o úplných Booleových alge- berách a o jejich užití v semantice prvořádové predikátové logiky. Práce má dva hlavní cíle, v první řadě dokázat, že každá Booleova algebra může být rozšířena na úplnou Booleovu algebru tak, že původní algebra je její hustá podalgebra. Toto tvrzení je dokázáno pomocí topologické kontrukce. Následně, ve druhé části, defin- ujeme sémantiku prvořádové predikátové logiky s ohledem na úplné Booleovy algebry, současně také zavedeme pojem Booleovsky- ohodnoceného modelu. Poté dokážeme větu o úplnosti s ohledem na všechny úplné Booleovy algebry. To je dokázáno pomocí ultrafiltrů na Booleových algebrách. Klíčová slova: Booleovy algebry, úplné Booleovy algebry, kla- sická logika.
|
|
|
Verefication of Mathematical Proofs
Pudlák, Petr ; Štěpánek, Petr (vedoucí práce) ; Haniková, Zuzana (oponent) ; Plátek, Martin (oponent)
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...
|
|
| |
|
| |
host ::
RSS.