|
|
The notion of interpretation between axiomatic theories
Štefanišin, Jan ; Švejdar, Vítězslav (advisor) ; Haniková, Zuzana (referee)
Thesis: The Notion of Interpretation between Axiomatic Theories Author: Jan Štefanišin Abstract: In this thesis we are researching the concept of intepretability between axiomatic theories and its basic properties and its uses. We define one-dimensional interpretation and show its behaviour on simple school theories. We also prove some important theorems about interpretations. In next two chapters we show interpretations on more complex theories. We use interpretations for transporting property of essential undecidability to theories in which theory R is interpretable. Then we show that theory of bounded arithmetic I∆0 is localy interpretable in Robinson arithmetic Q, which is also an example of cut-interpretation and is related to Edward Nelson's finitist program which we will comment on. Finally we return to school theories and use them to show how to prove that one theory is not interpretable in another. Keywords: interpretation, axiomatic theory, interpretability, definable sets, Ro- binson arithmetic
|
|
|
The notion of interpretation between axiomatic theories
Štefanišin, Jan ; Švejdar, Vítězslav (advisor) ; Haniková, Zuzana (referee)
In this thesis we are researching the concept of intepretability between axiomatic theories and its basic properties, its use and variants. We define one- dimensional interpretation and show its behaviour on simple school theories. Then we define multi-dimensional interpetation and piecewise interpretation and use them to make structure of degree of interpretability, in particular Double Degrees structure. We use one-dimensional interpretations for transporting property of essential undecidability to theories in which theory R is interpretable. Finally we show that theory of bounded arithmetic I∆0 is loccaly interpretable in Robinson arithmetic Q, which is also an example of cut-interpretation and is related to Edward Nelson's finitist program which we will comment on. Keywords: interpretation, axiomatic theory, interpretability, definable sets, Ro- binson arithmetic
|
|
| |
|
|
Verefication of Mathematical Proofs
Pudlák, Petr ; Štěpánek, Petr (advisor) ; Haniková, Zuzana (referee) ; Plátek, Martin (referee)
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...
|
|
|
Cambodia after 1979 and the application of the Reagan Doctrine
Haniková, Zuzana ; Hornát, Jan (advisor) ; Bečka, Jan (referee)
The thesis deals with the developments in Cambodia after 1979 and the Reagan Doctrine which was applied to Cambodia in the 1980s. The Vietnamese invasion ended the cruel government of the Khmer Rouge and also effected the development of the country for more than a decade. Cambodia became an ally of the Soviet Union and the expansionism of the Soviets was unacceptable for the United States. According to the Reagan Doctrine, US decided to support anticommunist movements in third world countries. The thesis analyzes the American support to the anticommunist groups in Cambodia and searches for the reasons of American decisions to support these groups and Washington's impact on the peace treaty and the withdrawal of Vietnamese forces. Based on the analysis of American policy, international negotiations and internal development in Cambodia, the thesis concludes that the main reason for US involvement was the fear of the spread of Soviet influence around the world, but the role of the US was limited and passive. It was caused by almost no interest in the issue of Cambodia and the American society also had a painful experience with the war in Vietnam. There were also reports that the international aid and assistance was used by the Khmer Rouge. The US became more active when new president came to office....
|
|
|
Systémy morfismů nad Gödelovou fuzzy logikou
Luhan, Ondřej ; Běhounek, Libor (advisor) ; Haniková, Zuzana (referee)
This work introduces some very basic concepts of category theory as built up over first-order predicate Gödel fuzzy logic (with crisp identity and the delta operator). A fuzzy variation of a classical concept of a category is considered. Then several systems of morphisms loosely based on the crisp categories Rel and Set are defined and examined. Accordingly, all the systems under consideration consist of fuzzy sets as objects and various kinds of binary fuzzy relations as morphisms. Our approach is a logic-based graded generalization of crisp (clas- sical) category-theoretical approaches to fuzzy sets, which have been initiated by Goguen. 1
|
|
|
Generalized Boolean models and classical predicate logic
Lávička, Tomáš ; Honzík, Radek (advisor) ; Haniková, Zuzana (referee)
This bachelor thesis is dealing with complete Boolean algebras and its use in semantics of first-order predicate logic. This thesis has two main goals, at first it is to show that every Boolean al- gebra can be extended to a complete Boolean algebra such that the former Boolean algebra is its dense subalgebra. This theorem is proved using topological construction. Afterwards, in the sec- ond part, we define semantics for first-order predicate logic with respect to complete Boolean algebras, which includes introduc- tion of the Boolean-valued model. Then we prove completeness theorem with respect to all complete Boolean algebras. The the- orem is proven using ultrafilters on Boolean algebras. Keywords: Boolean algebras, complete Boolean algebras, clas- sical logic.
|
|
|
Verefication of Mathematical Proofs
Pudlák, Petr ; Štěpánek, Petr (advisor) ; Haniková, Zuzana (referee) ; Plátek, Martin (referee)
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...
|
|
| |
|
| |
guest ::
