Zpracování strojových důkazů

• Thesis title in Czech: Zpracování strojových důkazů
• Thesis title in English: Processing machine generated proofs
• Academic year of topic announcement: 2011/2012
• Thesis type: diploma thesis
• Thesis language: čeština
• 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: 28.09.2011
• Date of assignment: 20.10.2011
• Confirmed by Study dept. on: 07.12.2011
• Advisors: Mgr. Josef Urban, Ph.D.

Guidelines

Zkoumejte strojově nalezené důkazy nad knihovnou Mizar a porovnejte je jak mezi sebou navzájem, tak i s původními důkazy napsanými matematiky. Kritérii mohou být různými způsoby zadefinovaná délka důkazu, počet premis, "elegance" atd.
Dále se zabývejte se různými způsoby transformace a reprezentace strojově nalezených důkazů, s účelem důkazy zkrátit, zjednodušit, "zpřehlednit". Techniky aplikujte na důkazy nad Mizarem a/nebo na důkazy vět z teorie kvazigrup a lup.

References

www.mizar.org
Josef Urban: MPTP - Motivation, Implementation, First Experiments. J. Autom. Reasoning 33(3-4): 319-339 (2004)
JD Phillips, D.S.: Automated theorem proving in quasigroup and loop theory, Artificial Intelligence Communications 23/2-3 (2010), 267--283.
J. Vyskočil, J. Urban, D.S.: Automated proof compression by invention of new definitions, LPAR-16 (Dakar, 2010), in LNAI 6355.
G. Sutcliffe, ART, http://www.cs.miami.edu/~geoff/ResearchProjects/ART/
J. A. Robinson, A. Voronkov: The Handbook of Automated Reasoning, MIT Press, 2001.