NCN

Challenges to automated reasoning in decidable fragments of first-order logic: trees, orders and numerals

About NCN Project

 

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:

  1. Ian Pratt-Hartmann and Lidia Tendera: The Fluted Fragment with Transitivity, in Forty-fourth International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), 18:1–15 Leibniz International Proceedings in Mathematics, vol. 138.
  2. Ian Pratt-Hartmann: Fluted Logic with Counting, in 48th International Colloquium on Automata, Languages and Programming (ICALP 2021), pp. 141:1-141:17, Leibniz International Proceedings in Informatics (LIPIcs), 2021.
  3. Ian Pratt-Hartmann and Lidia Tendera: The fluted fragment with transitive relations, Annals of Pure and Applied Logic 173, 2022, art. 103042, pp. 1-43.
  4. Ian Pratt-Hartmann and Lidia Tendera: Adding Transitivity and Counting to the Fluted Fragment, in 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pp. 32:1–32:22, Leibniz International Proceedings in Informatics (LIPIcs), 2023.
  5. Bartosz Bednarczyk, Daumantas Kojelis and Ian Pratt-Hartmann: On the Limits of Decision: the Adjacent Fragment of First-Order Logic, in 50th International Conference on Automata, Languages and Programming (ICALP 2023), pp. 111:1–21.
  6. Bartosz Bednarczyk and Emanuel Kieroński: Finite-Entailment of Local Queries in the Z family of Description Logics, in 36th AAAI Conference on Artificial Intelligence, AAAI 2022.
  7. Bartosz Bednarczyk, Emanuel Kieronski: Finite-Controllability of Conjunctive Queries in the Z family of Description Logics (Extended Abstract). Description Logics 2021
  8. Ian Pratt-Hartmann: Walking on Words, in 35th Annual Symposium on Combinatorial Pattern Matching (CPM 2024), pp. 25:1–25:17.
  9. Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann: On the of Limits of Decision: the Adjacent Fragment of First-Order Logic (Extended Abstract). Description Logics 2024.
  10. Dariusz Marzec and Lidia Tendera: On Two-variable First-order Logic with a Partial Order, in 39th Italian Conference on Computational Logic (CILC 2024).
  11. Tharindu Madusanka, Ian Pratt-Hartmann and Riza Batista-Navarro: Natural Language Satisfiability: Exploring the Problem Distribution and Evaluating Transformer-based Language Models, in 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 15278–15294, 2024.
  12. Bartosz Bednarczyk, Daumantas Kojelis and Ian Pratt-Hartmann: The Adjacent Fragment and Quine’s Limits of Decision. (extended version of ICALP 2023 paper; submitted)
  13. Dariusz Marzec and Lidia Tendera: On Two-variable First-order Logic with a Partial Order. (extended version of CILC 2024 paper; submitted).
  14. Daumantas Kojelis: On homogenous Models of Fluted Languages. (submitted)