SATURATION-BASED QUERY ANSWERING AND REWRITING PROCEDURES FOR GUARDED FIRST-ORDER FRAGMENTS

Student thesis: Phd

Abstract

This thesis presents the first practical Boolean conjunctive query answering and the first saturation-based Boolean conjunctive query rewriting procedures for the guarded fragment and its extensions: the loosely guarded, the clique guarded, the guarded negation and the clique guarded negation fragments. All these fragments are robustly decidable, hence they are exceptionally qualified candidates as logical formalisms. The problems of answering Boolean conjunctive queries in all of these fragments are also decidable, nonetheless it is open whether there exist practical decision procedures for these problems. We close this gap by developing a theoretical framework for practical query answering procedures for all of these fragments, presenting new techniques, new inference systems and new procedures. In particular we devise a partial selection-based resolution rule, based on which we establish new, elegant and powerful saturation-based systems, named the top-variable inference systems. We formally prove the system are sound and refutationally complete for first-order clausal logic (with equality). Using these systems, we devise the first resolution-based decision procedure for the clique guarded fragment, and the first practical decision procedures for the unary negation, the guarded negation and the clique guarded negation fragments. Another significant contribution is the presentation of saturation-based rewriting approaches, allowing a new perspective to the topic of query rewriting through the use of powerful automated deduction techniques. Our rewriting procedures guarantee successful back-translation from the clausal sets, derived with our query answering procedures, to a first-order formula. In general the back-translation problem is undecidable and often fails, nonetheless by our rules, this problem is solvable for Boolean conjunctive queries for all the considered guarded fragments. For practicality we use a saturation-based approach as the basis, so that all the procedures are well-primed for implementation in state-of-the-art modern first-order theorem provers in the future.
Date of Award31 Dec 2021
Original languageEnglish
Awarding Institution
  • The University of Manchester
SupervisorRenate Schmidt (Supervisor) & Giles Reger (Supervisor)

Cite this

'