Automatická konstrukce modelů

• Thesis title in Czech: Automatická konstrukce modelů
• Thesis title in English: Automated model building
• Academic year of topic announcement: 2010/2011
• 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: 18.10.2010
• Date of assignment: 18.10.2010
• Date and time of defence: 08.09.2015 09:00
• Date of electronic submission: 29.07.2015
• Date of submission of printed version: 30.07.2015
• Date of proceeded defence: 08.09.2015
• Opponents: doc. RNDr. Pavel Surynek, Ph.D.

Guidelines

Problém zní, k dané sadě axiomů v predikátové logice najít model.

Student provede analýzu výsledků soutěže CASC a zjistí, na čem jsou založeny úspěšné systémy (Paradox, Equinox, Geo). Cílem práce pak bude návrh a implementace vlastních algoritmů na hledání modelů, založených na různých metodách, a výběr vhodného algoritmu na základě analýzy vstupních dat.

Metody, které student vyzkouší:
* redukce na problém SAT a použití nějakého state-of-the-art SAT-solveru (v zásadě jde o reimplementaci, případně vylepšení, algoritmu, který používá systém Paradox)
* redukce na problém CSP a použití nějakého state-of-the-art CSP-solveru (nový přístup)
* vliv saturace teorie na efektivitu solveru
* případně další nápady, které se objeví v průběhu práce

Systém bude testován na úlohách z knihovny TPTP a porovnán s ostatními systémy na hledání modelů.

References

dokumentace systémů Paradox, SEM, Equinox, Geo, ...
http://www.tptp.org
John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge Uni. Press, 2009.