The case challenges in automated reasoning within decidable fragments of first-order logic, which is crucial for structured data management in fields like Computer Science. Although first-order logic is undecidable in general (i.e., no universal algorithm can solve it), certain fragments of this logic are decidable, enabling practical applications. Research focuses on balancing the expressive power of these fragments with computational efficiency, as more expressive fragments tend to be harder to reason with. The abstract highlights three key fragments: the two-variable fragment, the guarded two-variable fragment, and the fluted fragment. These are important in IT systems, where reasoning with data involves inferring answers from both the data and background theories, rather than simple matching. The challenges particularly arise when dealing with ordered data or tree-like structures (e.g., XML). The proposed work seeks to resolve open problems in this area, using mathematical techniques to improve reasoning systems for knowledge retrieval.
List of publications:
Challenges to automated reasoning in decidable fragments of first-order logic: trees, orders and numerals
UNIFDL
Institute of Computer Science
University of Opole
Room no. 210
48 Oleska St.
45-052 Opole, Poland
unifdl@uni.opole.pl
+48 (77) 452 7210