Original title:
Automatický theorem prover
Translated title:
An Automatic Theorem Prover
Authors:
Mazánek, Martin ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor) Document type: Bachelor's theses
Year:
2020
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[cze][eng]
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í.
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; First-order logic; Propositional logic; Resolution; TPTP; Automatické dokazování; predikátová logika prvního řádu; rezoluce; TPTP; výroková logika
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: http://hdl.handle.net/11012/191505