Thesis Details

Automatický theorem prover

Bachelor's Thesis Student: Mazánek Martin Academic Year: 2019/2020 Supervisor: Lengál Ondřej, Ing., Ph.D.
English title
An Automatic Theorem Prover
Language
Czech
Abstract

This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and first-order logic. The goal of this thesis is to create simple prover and document the development. Making state-of-the-art prover is not the goal of this thesis. We also present some popular automated theorem provers.

Keywords

Automated Theorem Proving, Resolution, Propositional logic, First-order logic, TPTP

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology
Files
Status
defended, grade C
Date
10 July 2020
Reviewer
Havlena Vojtěch, Ing., Ph.D.
Committee
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Kekely Lukáš, Ing., Ph.D. (DCSY FIT BUT), člen
Křivka Zbyněk, Ing., Ph.D. (DIFS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Španěl Michal, Ing., Ph.D. (DCGM FIT BUT), člen
Citation
MAZÁNEK, Martin. Automatický theorem prover. Brno, 2020. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2020-07-10. Supervised by Lengál Ondřej. Available from: https://www.fit.vut.cz/study/thesis/22800/
BibTeX 
@bachelorsthesis{FITBT22800,
    author = "Martin Maz\'{a}nek",
    type = "Bachelor's thesis",
    title = "Automatick\'{y} theorem prover",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2020,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/22800/"
}

Theses

Back to top