Systémy automatického dokazování

• Thesis title in Czech: Systémy automatického dokazování
• Thesis title in English: Systems for automated theorem proving
• Academic year of topic announcement: 2007/2008
• Thesis type: Bachelor's thesis
• Department: Department of Algebra (32-KA)
• Supervisor: doc. RNDr. David Stanovský, Ph.D.
• Author: hidden - assigned and confirmed by the Study Dept.
• Date of registration: 14.11.2007
• Date of assignment: 14.11.2007

Guidelines

Existuje řada počítačových systémů pro automatické dokazování matematických vět. V některých oblastech vykazují zajímavé výsledky (např. některé algebraické obory), v jiných je zatím jejich chování neuspokojivé (např. teorie množin). Cílem práce je seznámit se s úspěšnými systémy a s principem jejich činnosti, porovnat je na úlohách předložených vedoucím práce a pokusit se vyvodit závěry, který typ úloh kterému systému lépe svědčí.

References

Nerode, Anil; Shore, Richard A., Logic for applications. Graduate Texts in Computer Science. New York, NY: Springer
http://www.cs.miami.edu/~tptp - software a články uvedené na této adrese