|
|
DPLL algorithm and propositional proofs
Hrnčiar, Maroš ; Krajíček, Jan (vedoucí práce) ; Koucký, Michal (oponent)
Dôkazová zložitosť je zaujímavá súčasť matematiky nachádzajúca sa na pomedzí obrovskej oblasti logiky a teórie zložitosti. Skúma aké dôkazové systémy sú potrebné na efektívne dokazovanie rôznych matematických tvrdení. Predmetom tejto práce je spojenie medzi dôkazovými systémami a algoritmami na SAT. Uvidíme, že beh algoritmu na nesplniteľnej formule môže byť nahliadnutý ako výrokový dôkaz jej nesplniteľnosti, čím samotný algoritmus prakticky definuje celý dôkazový systém. Práca je určená najmä čitateľom so záujmom o dôkazovú zložitosť, ale dokáže aj samostatne objasniť princíp rezolúcie, či ponúknuť menej obvyklý pohľad na SAT, no zároveň predpokladá čitateľovu znalosť základov výrokovej logiky, teórie grafov a zložitosti.
|
|
|
Solving diophantine equations by factorization in number fields
Hrnčiar, Maroš ; Kala, Vítězslav (vedoucí práce) ; Příhoda, Pavel (oponent)
Název práce: Řešení diofantických rovnic rozkladem v číselných tělesech Autor: Bc. Maroš Hrnčiar Katedra: Katedra algebry Vedoucí diplomové práce: Mgr. Vítězslav Kala, Ph.D., Mathematisches Institut, Georg-August Universität Göttingen Abstrakt: Problém řešitelnosti diofantických rovnic je jedním z nejstarších ma- tematických problémů v historii. Postupně se vyvinuly různé přístupy k řešení určitých typů rovnic, z nichž se v práci zabýváme převážně metodou využívající faktorizaci v algebraickém číselném tělese. Myšlenkou této metody je vyjádřit rovnici ve tvaru L = yn , kde levá strana L je součin typicky lineárních fak- torů s koeficienty v daném číselném tělese. Při splnění několika předpokladů po- tom můžeme každý z faktorů napsat jako n-tou mocninu. Klíčovou roli při apli- kaci metody hraje struktura číselných těles, proto neoddělitelnou součást práce tvoří přehled algebraické teorie čísel. Kromě výkladu obecné teorie jsou zde uve- dené i výpočty v jednotlivých kvadratických a kubických tělesech popisující jejich vlastnosti. Hlavním předmětem práce je však řešení konkrétních úloh. Například v rovnici x2 + y2 = z3 se potýkáme s netriviálními společnými děliteli faktorů v...
|
|
|
Solving diophantine equations by factorization in number fields
Hrnčiar, Maroš ; Kala, Vítězslav (vedoucí práce) ; Příhoda, Pavel (oponent)
Název práce: Řešení diofantických rovnic rozkladem v číselných tělesech Autor: Bc. Maroš Hrnčiar Katedra: Katedra algebry Vedoucí diplomové práce: Mgr. Vítězslav Kala, Ph.D., Mathematisches Institut, Georg-August Universität Göttingen Abstrakt: Problém řešitelnosti diofantických rovnic je jedním z nejstarších ma- tematických problémů v historii. Postupně se vyvinuly různé přístupy k řešení určitých typů rovnic, z nichž se v práci zabýváme převážně metodou využívající faktorizaci v algebraickém číselném tělese. Myšlenkou této metody je vyjádřit rovnici ve tvaru L = yn , kde levá strana L je součin typicky lineárních fak- torů s koeficienty v daném číselném tělese. Při splnění několika předpokladů po- tom můžeme každý z faktorů napsat jako n-tou mocninu. Klíčovou roli při apli- kaci metody hraje struktura číselných těles, proto neoddělitelnou součást práce tvoří přehled algebraické teorie čísel. Kromě výkladu obecné teorie jsou zde uve- dené i výpočty v jednotlivých kvadratických a kubických tělesech popisující jejich vlastnosti. Hlavním předmětem práce je však řešení konkrétních úloh. Například v rovnici x2 + y2 = z3 se potýkáme s netriviálními společnými děliteli faktorů v...
|
|
|
DPLL algorithm and propositional proofs
Hrnčiar, Maroš ; Krajíček, Jan (vedoucí práce) ; Koucký, Michal (oponent)
Dôkazová zložitosť je zaujímavá súčasť matematiky nachádzajúca sa na pomedzí obrovskej oblasti logiky a teórie zložitosti. Skúma aké dôkazové systémy sú potrebné na efektívne dokazovanie rôznych matematických tvrdení. Predmetom tejto práce je spojenie medzi dôkazovými systémami a algoritmami na SAT. Uvidíme, že beh algoritmu na nesplniteľnej formule môže byť nahliadnutý ako výrokový dôkaz jej nesplniteľnosti, čím samotný algoritmus prakticky definuje celý dôkazový systém. Práca je určená najmä čitateľom so záujmom o dôkazovú zložitosť, ale dokáže aj samostatne objasniť princíp rezolúcie, či ponúknuť menej obvyklý pohľad na SAT, no zároveň predpokladá čitateľovu znalosť základov výrokovej logiky, teórie grafov a zložitosti.
|
host ::
RSS.