První se zaměřuje na oblast logické analýzy přirozeného jazyka. Motivací je zde automatické zpracování textů v přirozené řeči do formální podoby, která umožňuje lepší zachycení přesného významu daných tvrzení. Ty pak následně umožní lepší možnosti dotazování nad textovými bázemi a automatické odvozování důsledků vyplývající z uvedených tvrzení. Jako formální prostředek vhodný pro tento typ zpracování přirozené řeči se využívá zejména Transparentní intenzionální logika (TIL).
Druhá podskupina se zaměřuje na oblast verifikace, zejména na verifikaci programů, speciálně na verifikaci paralelních programů, ale obecně i na verifikaci dalších typů systémů. Část výzkumu se věnuje zkoumání algoritmické rozhodnutelnosti a výpočetní složitosti problémů, které vyvstávají v této oblasti. Další část výzkumu se zaměřuje na vývoj nástrojů pro verifikaci. Jednou z oblastí je také využití nástrojů pro interaktivní a automatizované dokazování, jako je například nástroj Coq, pro verifikaci programů a dalších systémů.
Galerie laboratoří
Spolupráce
Spolupráce s firmou Merica, s.r.o. na vývoji softwarové komponenty pro verifikaci BPMN procesů - komponenta bude součástí software dodávaného firmou Merica, která vyvíjí nástroje zaměřené na rozvrhování a optimalizaci výrobních procesů. V minulosti jsme spolupracovali s touto firmou na vývoji některých dalších softwarových komponent využívaných v jejich software.
V oblasti logické analýzy jazyka spolupráce s Univerzitou Komenského Bratislava, Katedrou logiky a metodologie vied
V oblasti verifikace transformací SQL dotazů a formalizace jazyka SQL v Coqu spolupráce s týmem z ENS Paris-Saclay, Université Paris-Saclay, Francie
Loga
Projekty
Sawa Zdeněk doc. Ing., Ph.D.: APS pro výrobu s flexibilními zdroji a procesy, Technologická agentura (2024 - 2026)
Duží Marie prof. RNDr., CSc.: Hyperintensionální usuzování nad texty přirozeného jazyka, Grantová agentura ČR (2018 - 2020)
Duží Marie prof. RNDr., CSc.: Hyperintensionální logika pro analýzu přirozeného jazyka, Grantová agentura ČR (2015 - 2017)
Běhálek Marek Ing., Ph.D.: Rozšiřování nástroje Kaira, Ministerstvo školství, mládeže a tělovýchovy (2015 - 2015)
Běhálek Marek Ing., Ph.D.: Implementace predikce výkonu a verifikací do nástroje Kaira, Ministerstvo školství, mládeže a tělovýchovy (2014 - 2014)
Jančar Petr prof. RNDr., CSc.: Modelování a verifikace paralelních systémů, Grantová agentura ČR (2011 - 2014)
Publikace
Rapant, P., Menšík, M., Albert, A. (2024). Automatic sketch map creation from labeled planar graph, International Journal of Geographical Information Science, 38, 981-1006 [detail...]
Číhalová, M., Duží, M. (2023). Modelling dynamic behaviour of agents in a multi-agent system; Logical analysis of Wh-questions and answers., Logic journal of IGPL, 31, 140-171 [detail...]
Jančar, P., Osička, P., Sawa, Z. (2023). Countdown games, and simulation on (succinct) one-counter nets, Logical Methods in Computer Science, 19, 11:1-11:44 [detail...]
Duží, M. (2023). Specification of Agents’ Activities in Past, Present and Future., Organon F, 30, 66-101 [detail...]
Jespersen, BTF., Duží, M. (2022). Transparent quantification into hyperpropositional attitudes de dicto, Linguistics and Philosophy, 45, 1119–1164 [detail...]
Duží, M. (2019). If structured propositions are logical procedures then how are procedures individuated?, Synthese, 196, 1249-1283 [detail...]
Jespersen, B., Carrara, M., Duží, M. (2017). Iterated privation and positive predication, Journal of Applied Logic, 25, 48-71 [detail...]
Jespersen, B., Duží, M. (2015). Introduction, Synthese, 192, 525-534 [detail...]
Böhm, S., Běhálek, M., Meca, O., Šurkovský, M. (2014). Visual Programming of MPI Applications: Debugging, Performance Analysis, and Performance Prediction, COMPUTER SCIENCE AND INFORMATION SYSTEMS, 11, 1315-1336 [detail...]
Duží, M., Jespersen, B. (2014). Transparent Quantification into Hyperintensional objectual attitudes, Synthese, 192, 635-677 [detail...]
Aplikační výsledky
Böhm, S., Běhálek, M., Meca, O., Šurkovský, M. (2014). Kaira, Vysoká škola báňská - Technická univerzita Ostrava SOFTWARE [detail...]