Detail práce

Automatický theorem prover

Bakalářská práce Student: Mazánek Martin Akademický rok: 2019/2020 Vedoucí: Lengál Ondřej, Ing., Ph.D.
Název anglicky
An Automatic Theorem Prover
Jazyk práce
český
Abstrakt

Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování.

Klíčová slova

Automatické dokazování, rezoluce, výroková logika, predikátová logika prvního řádu, TPTP

Ústav
Ústav inteligentních systémů FIT VUT v Brně
Studijní program
Informační technologie
Soubory
Stav
obhájeno, hodnocení C
Obhajoba
10. července 2020
Oponent
Havlena Vojtěch, Ing., Ph.D.
Průběh obhajoby

Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm C.

Otázky u obhajoby
  1. Máte představu, kolik času je třeba pro rozhodnutí formulí v experimentální části, kdy došlo k timeoutu (60s)?
Komise
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT), předseda
Kekely Lukáš, Ing., Ph.D. (UPSY FIT VUT), člen
Křivka Zbyněk, Ing., Ph.D. (UIFS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Španěl Michal, Ing., Ph.D. (UPGM FIT VUT), člen
Citace
MAZÁNEK, Martin. Automatický theorem prover. Brno, 2020. Bakalářská práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2020-07-10. Vedoucí práce Lengál Ondřej. Dostupné z: https://www.fit.vut.cz/study/thesis/22800/
BibTeX 
@bachelorsthesis{FITBT22800,
    author = "Martin Maz\'{a}nek",
    type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
    title = "Automatick\'{y} theorem prover",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2020,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/22800/"
}

Závěrečné práce

Nahoru