Research
My research is focused on algorithmic and model-theoretic aspects of decidable fragments of First-Order Logic, with their applications to database-related reasoning problems. I study their expressive power, complexity of satisfiability, definability, related preservation theorems, and succinctness. I enjoy the interplay between logic, databases, automata theory and algebra. I strongly believe that my research does not have any practical applications, nevertheless its true value comes from its mathematical beauty.
Among other stuff, I am particularly interested in logics describing properties of trees and words, such as temporal logics (LTL, CTL), XPath and logics enjoining tree model property (modal logics, description logics, guarded fragments) and logics with restricted sequences allowed to appear in atoms (fluted fragment, adjacent fragment).
Research interests
- Modal and description logics
- Ontology mediated data access
- Query answering, XML documents
- Logics with counting and arithmetics
- Craig Interpolation, Preservation Theorems
- Finite and Algorithmic Model theory
Ongoing research projects
-
Project webpage: here
The project deals with the formal foundations of knowledge management as well as their application in today's information society. Among the biggest challenges in this area are the intelligent access to digital information as well as the automated composition of information from diverse sources. For these purposes, logical specifications of background knowledge - so-called ontologies - can be used together with automated reasoning techniques in order to enable a "meaning-aware" handling of data. Unfortunately, reasoning in ontology languages of high expressivity is impossible to capture algorithmically – they are undecidable. Therefore, the quest for "good" ontology languages consists in identifying logical formalisms which are as expressive as possible, yet still decidable. Hitherto, the obtained results in this area have, however, been patchy and fragmented. The goal of the DeciGUT project is the creation of a unified theory of decidability, which in turn will enable the definition of new, advanced ontology languages. The project is of high relevance to diverse scientific fields like mathematical logic, artificial intelligence, and database theory with potentially far-reaching impact in areas such as semantic technologies and information systems.
Past projects
-
Project webpage: [not yet]
The main goal of the project is to develop decision procedures and to study theoretical properties of logics extended with generalized counting quantifiers. Such quantifiers will formalize a numerous constructs from natural language e.g. "at most", "an even number", "every five of", "at least" or "less than 70%".
We will study satisfiability problem for logics on arbitrary structures as well as on data trees and words. We will also take a look at conjunctive query answering problem, where such quantifiers can be used to describe a potential knowledge base. -
Project webpage: link [pl], Project description: link [pl]
During my employment in the project, I studied query languages to process XML documents, augmented with counting quantifiers. To be more precise, I studied the satisfiability problem for Two-Variable Fragment of First-Order Logic with various ways of counting interpreted on finite trees. I successfully produced three research papers, which were presented at ESSLLI 2017, CSL 2017 and FSTTCS 2017.