GUI pro dokazovací systémy

• Thesis title in Czech: GUI pro dokazovací systémy
• Thesis title in English: GUI for automated reasoning systems
• Academic year of topic announcement: 2006/2007
• Thesis type: Bachelor's 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: 02.11.2006
• Date of assignment: 02.11.2006
• Date and time of defence: 25.06.2007 00:00
• Date of electronic submission: 25.06.2007
• Date of proceeded defence: 25.06.2007
• Opponents: RNDr. Kamil Toman

Guidelines

Cílem práce (softwarového projektu) je vytvořit grafické rozhraní pro práci se systémy automatického dokazování matematických vět (Prover9, Mace, Waldmeister, atd.). Základní funkce a vzhled prostředí bude specifikován vedoucím; výsledný systém by se měl připomínat prostředí pro práci s TeXem, měl by umožňovat snadné přidávání nových verzí a dalších systémů, student se také může zabývat problematikou exportu výstupních souborů do "lidské podoby". Součástí práce bude dokumentace včetně základního matematického popisu funkce těchto systémů (nikoliv však nutně používaných algoritmů).

References

Sutcliffe, Suttner, The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning 21 (1998).
http://www.cs.miami.edu/~tptp/
http://www.cs.unm.edu/~mccune/prover9/
http://www.mpi-sb.mpg.de/~hillen/waldmeister/
http://users.rsise.anu.edu.au/~jks/finder.html
http://www4.informatik.tu-muenchen.de/~letz/setheo/