Automated Theorem Proving using the Tableaux method

• Název práce v češtině: Automatické dokazování vět s použitím tableaux metod
• Název v anglickém jazyce: Automated Theorem Proving using the Tableaux method
• Akademický rok vypsání: 2005/2006
• Typ práce: diplomová práce
• Jazyk práce: angličtina
• Ústav: Katedra teoretické informatiky a matematické logiky (32-KTIML)
• Vedoucí / školitel: prof. RNDr. Petr Štěpánek, DrSc.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 21.11.2005
• Datum zadání: 21.11.2005
• Datum a čas obhajoby: 11.09.2006 00:00
• Datum odevzdání elektronické podoby: 11.09.2006
• Datum proběhlé obhajoby: 11.09.2006
• Oponenti: RNDr. Jan Hric

Zásady pro vypracování

Start with the relevant parts of the book [1] in particular Chapters 3, 10 and 18. Read the paper [2] as a reference implementation of a Theorem Prover of the type. Explore the possibilities of extending the reference implementation towards more expressive logics or extensions using some features of other Tableaux Provers e.g. SETHEO, PTTP, DCTP, HOL - Meson tactics.

Seznam odborné literatury

1] Handbook of Automated Reasoning, A. Robinson and A. Voronkov (editors), The MIT Press, Cambridge, Massachusetts (2001)

[2] B. Beckert, J. Posegga, LeanTaP:Lean Tableaux-based Deduction (to appear in the Journal of Automated Reasoning)

Předběžná náplň práce

Master Thesis is devoted to Automated Theorem Proving of a particular type, namely, to Provers using Tableaux. Its goal is to find appropriate extensions of so called reference implementation towards more expressive logics or to extensions using some features of Tableaux Provers e.g. SETHEO, DCTP, PTTP, HOL - Meson tactics.