Original title:
Automatické dokazování vět s použitím tableaux metod
Translated title:
Automated Theorem Proving using the Tableaux method
Authors:
Jakubův, Jan ; Štěpánek, Petr (advisor) ; Hric, Jan (referee) Document type: Master’s theses
Year:
2006
Language:
eng Abstract:
[eng][cze] In this paper we are studying the Tableaux Calculus a related methods. We adopt basic notions and present the tableaux calculus for the First-Order Logic. Then we present the Beckert and Possega [5] prover. We extend this prover with speed-up technique and compare the results with the original prover. Then we present the tableaux T system of Degtyarev and Voronkov [3] supposed to handle the equality. The main benefit of this paper is the implementation the the T system prover. We also present a library providing tools to work with the objects of the First-Order Logic in the programming language Python.V této práci studujeme tableaux kalkul a podobné metody. Nejprve zavádíme obvyklé pojmy a poté představujeme tableaux kalkul pro logiku prvního řádu. Dále představujeme automatický dokazovač vět autorů Beckert a Possega [5]. Rozšiřujeme tento dokozovač o metodu, která má urychlit jeho práci. Výsledný program porovnáváme s jeho původní verzí. Dále představujeme deduktivní systém T autorů Degtyarev a Voronkov [3]. Hlavním přínosem této práce je implementace tohoto systému. Dále také vyvíjíme knihovnu pro práci s objekty logiky prvního řádu v programovacím jazyce Python.
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/7549