II.g AIF: Automatické uvažování a formální metody

Vedoucí skupiny
Jméno: Jiří Vyskočil
Telefon: +()
Email: jiri.vyskocil(at)ciirc.cvut.cz

Skupina AIF se zaměřuje na výzkum v různých oblastech umělé inteligence a výpočetní logiky (computational logic), mezi které zejména patří automatické uvažování (automated reasoning), interaktivní dokazování vět (interactive theorem proving) a práce s rozsáhlými formálními (zejména matematickými) znalostními bázemi (knowledge bases). Tyto oblasti dále zahrnují automatické deduktivní odvozování (automathed theorem proving), induktivní uvažování (včetně strojového učení a hledání nových znalostí) a jejich vzájemné kombinace a interakce. Dále se také věnujeme formalizaci, počítačové verifikaci, typům, ověřování modelů (model checking) a deklarativnímu a funkcionálnímu programování.

V poslední době také vyvíjíme nové metody pro automatické zpracování přirozeného jazyka v dobře formalizovatelných doménách, jakými jsou například matematika a informatika.


Zodpovídá: Jiří Vyskočil