Automatizace metody hintů
| Thesis title in Czech: | Automatizace metody hintů |
|---|---|
| Thesis title in English: | Automatizing the hints strategy |
| Academic year of topic announcement: | 2009/2010 |
| Thesis type: | diploma thesis |
| Thesis language: | |
| 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: | 15.10.2009 |
| Date of assignment: | 15.10.2009 |
| Guidelines |
| V automatickém dokazovači vět Prover9 je implementována tzv. metoda hintů, která umožňuje řídit hledání důkazu pomocí nápověd. Bob Veroff a Michael Kinyon tuto metodu mnohokrát využili k získání důkazů v algebře, které konvenčním způsobem nalézt nešly. Cílem je pokusit se zautomatizovat jejich metodu, která zatím vyžaduje expertní vstup ze strany znalce problému. Expert by mohl být nahrazen programem HR Simona Coltona, případně vlastním programem pracujícím na Coltonových či jiných principech. Cílem práce je 1) implementovat tuto strategii (ať už s použitím HR, nebo s použitím vlastního expertního systému), 2) otestovat (a odladit parametry) na databázi úloh TPTP a/nebo QPTP. V případě výrazného úspěchu by systém mohl být přihlášen do soutěže dokazovačů CASC v roce 2010.
|
| References |
| Voronkov, Handbook of automated reasoning, North Holland, 2001
W. McCune, Prover9, http://www.prover9.org G. Sutcliffe, http://www.tptp.org S. Colton, A. Bundy and T. Walsh: "Automatic Identification of Mathematical Concepts", Proceedings of ICML-2000, Stanford, CA, 2000 |