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

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-416297


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce