Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 368)
Detail práce
   Přihlásit přes CAS
Automatická konstrukce modelů
Název práce v češtině: Automatická konstrukce modelů
Název v anglickém jazyce: Automated model building
Akademický rok vypsání: 2010/2011
Typ práce: diplomová práce
Jazyk práce: čeština
Ústav: Katedra algebry (32-KA)
Vedoucí / školitel: doc. RNDr. David Stanovský, Ph.D.
Řešitel: skrytý - zadáno a potvrzeno stud. odd.
Datum přihlášení: 18.10.2010
Datum zadání: 18.10.2010
Datum a čas obhajoby: 08.09.2015 09:00
Datum odevzdání elektronické podoby:29.07.2015
Datum odevzdání tištěné podoby:30.07.2015
Datum proběhlé obhajoby: 08.09.2015
Oponenti: doc. RNDr. Pavel Surynek, Ph.D.
 
 
 
Zásady pro vypracování
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ů.
Seznam odborné literatury
dokumentace systémů Paradox, SEM, Equinox, Geo, ...
http://www.tptp.org
John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge Uni. Press, 2009.
 
Univerzita Karlova | Informační systém UK