|
|
DPLL algorithm and propositional proofs
Hrnčiar, Maroš ; Krajíček, Jan (advisor) ; Koucký, Michal (referee)
Proof complexity is an interesting mathematical part connecting logic and complexity theory. It investigates which proof systems are needed for effective theorem proving. The aim of this paper is to present a relation between propositional proof systems and SAT algorithms. We will see that a run of an algorithm on the unrealizable formula can be seen as a propositional proof of its unsatisfiability, so the algorithm practically defines whole proof system. The thesis is mainly recommended for readers interested in proof complexity, but it can also independently illustrate a resolution principle and perhaps show some less common view of SAT assuming reader's basic knowledge of propositional logic, graph theory and complexity.
|
|
|
Solving diophantine equations by factorization in number fields
Hrnčiar, Maroš ; Kala, Vítězslav (advisor) ; Příhoda, Pavel (referee)
Title: Solving diophantine equations by factorization in number fields Author: Bc. Maroš Hrnčiar Department: Department of Algebra Supervisor: Mgr. Vítězslav Kala, Ph.D., Mathematical Institute, University of Göttingen Abstract: The question of solvability of diophantine equations is one of the oldest mathematical problems in the history of mankind. While different approaches have been developed for solving certain types of equations, this thesis predo- minantly deals with the method of factorization over algebraic number fields. The idea behind this method is to express the equation in the form L = yn where L equals a product of typically linear factors with coefficients in a particular number field. Provided that several assumptions are met, it follows that each of the factors must be the n-th power of an element of the field. The structure of number fields plays a key role in the application of this method, hence a crucial part of the thesis presents an overview of algebraic number theory. In addition to the general theoretical part, the thesis contains all the necessary computations in specific quadratic and cubic number fields describing their basic characteristics. However, the main objective of this thesis is solving specific examples of equati- ons. For instance, in the case of equation x2 + y2 = z3 we...
|
|
|
Solving diophantine equations by factorization in number fields
Hrnčiar, Maroš ; Kala, Vítězslav (advisor) ; Příhoda, Pavel (referee)
Title: Solving diophantine equations by factorization in number fields Author: Bc. Maroš Hrnčiar Department: Department of Algebra Supervisor: Mgr. Vítězslav Kala, Ph.D., Mathematical Institute, University of Göttingen Abstract: The question of solvability of diophantine equations is one of the oldest mathematical problems in the history of mankind. While different approaches have been developed for solving certain types of equations, this thesis predo- minantly deals with the method of factorization over algebraic number fields. The idea behind this method is to express the equation in the form L = yn where L equals a product of typically linear factors with coefficients in a particular number field. Provided that several assumptions are met, it follows that each of the factors must be the n-th power of an element of the field. The structure of number fields plays a key role in the application of this method, hence a crucial part of the thesis presents an overview of algebraic number theory. In addition to the general theoretical part, the thesis contains all the necessary computations in specific quadratic and cubic number fields describing their basic characteristics. However, the main objective of this thesis is solving specific examples of equati- ons. For instance, in the case of equation x2 + y2 = z3 we...
|
|
|
DPLL algorithm and propositional proofs
Hrnčiar, Maroš ; Krajíček, Jan (advisor) ; Koucký, Michal (referee)
Proof complexity is an interesting mathematical part connecting logic and complexity theory. It investigates which proof systems are needed for effective theorem proving. The aim of this paper is to present a relation between propositional proof systems and SAT algorithms. We will see that a run of an algorithm on the unrealizable formula can be seen as a propositional proof of its unsatisfiability, so the algorithm practically defines whole proof system. The thesis is mainly recommended for readers interested in proof complexity, but it can also independently illustrate a resolution principle and perhaps show some less common view of SAT assuming reader's basic knowledge of propositional logic, graph theory and complexity.
|
guest ::
