Research groups

Laboratories

The research group is organized into two subgroups.

The first subgroup specializes in the logical analysis of natural language. Its aim is to automatically process natural language texts into a formal representation that more accurately captures the precise meaning of statements. Such representations enable more advanced querying of text databases as well as automated derivation of conclusions implied by the statements. A key formal framework applied in this research is Transparent Intensional Logic (TIL).

The second subgroup focuses on verification. Its primary interest lies in program verification—particularly the verification of parallel programs—while also addressing the verification of other types of systems. The research covers several directions: the study of algorithmic decidability and computational complexity of problems in this domain, the development of verification tools, and the application of interactive and automated theorem proving systems, such as Coq, for program and system verification.

Cooperation

Collaboration with Merica, s.r.o. on the development of a software component for BPMN process verification – the component will be part of the software delivered by Merica, a company specializing in the development of tools for scheduling and optimization of manufacturing processes. In the past, we have also cooperated with this company on the development of several other software components used in their products.

• In the field of logical language analysis collaboration with Comenius University in Bratislava, Department of Logic and Methodology of Sciences.
• In the field of SQL query transformation verification and SQL language formalization in Coq – collaboration with a team from ENS Paris-Saclay, Université Paris-Saclay, France.

Projects

• 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)

Publications

• 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...]

Application results

• Böhm, S., Běhálek, M., Meca, O., Šurkovský, M. (2014). Kaira, Vysoká škola báňská - Technická univerzita Ostrava SOFTWARE [detail...]

Team

Group leader

doc. Ing. Zdeněk Sawa, Ph.D.

Contact person

Prof. RNDr. Marie Duží, CSc.

Academic staff:

Ing. Marek Běhálek, Ph.D., Prof. RNDr. Marie Duží, CSc., Ing. Martin Kot, Ph.D., Mgr. Marek Menšík, Ph.D., doc. Ing. Zdeněk Sawa, Ph.D., doc. Mgr. Pavla Dráždilová, Ph.D.

Scientists:

Ing. Adam Albert, Ph.D., Bjorn Thoring Flagstad Jespersen, Ph.D.

Externalists: