Název:
Automatický theorem prover
Překlad názvu:
An Automatic Theorem Prover
Autoři:
Mazánek, Martin ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce) Typ dokumentu: Bakalářské práce
Rok:
2020
Jazyk:
cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [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.
Klíčová slova:
Automatické dokazování; predikátová logika prvního řádu; rezoluce; TPTP; výroková logika; Automated Theorem Proving; First-order logic; Propositional logic; Resolution; TPTP
Instituce: Vysoké učení technické v Brně
(web)
Informace o dostupnosti dokumentu:
Plný text je dostupný v Digitální knihovně VUT. Původní záznam: http://hdl.handle.net/11012/191505