Usage
  • 2 views
  • 5 downloads

Paving the Way for Efficient Disjunctive Hybrid MKNF Knowledge Base Solvers

  • Author / Creator
    Spencer Killen
  • Can efficient solvers be built for disjunctive hybrid MKNF knowledgebases? Recent breakthroughs in solver construction have proven AnswerSet Programming (ASP) to be a fruitful medium for tackling problemsthat lie within the lower two levels of the polynomial hierarchy. Thelogic of hybrid MKNF presents a powerful knowledge representationlanguage by elegantly pairing ASP with ontologies. It would seem thatstrong answer set solvers that incorporate the reasoning power ofontologies are within close grasp. Alas, some of the foundational workrequired to construct conflict-driven nogood learning (CDNL) solversdoes not yet exist for hybrid MKNF. In this thesis, we build upon theexisting foundation of hybrid MKNF to move towards the possibility of constructing a CDNL-based solver. Welift the existing definition of unfounded sets for knowledge baseswith non-disjunctive rules to knowledge bases that contain disjunctiverules. Unfounded sets serve as the basis for building operators thatcan be used to propagate information during the solving process. Because our operators cannot be used to verify arbitraryinterpretations, we provide a characterization of knowledge bases thatleverages a family of fixpoint operators for model-checking. Thischaracterization is reminiscent of prior techniques that leverage loopformulas to identify classes of knowledge bases that can be solved inNP-time. We identify an analogous case for disjunctive hybrid MKNFwhere interpretations can be verified in polynomial time instead ofrequiring an NP oracle. Finally, we outline an abstract solver thatutilizes this technique.

  • Subjects / Keywords
  • Graduation date
    Fall 2021
  • Type of Item
    Thesis
  • Degree
    Master of Science
  • DOI
    https://doi.org/10.7939/r3-zrkh-k859
  • License
    This thesis is made available by the University of Alberta Libraries with permission of the copyright owner solely for non-commercial purposes. This thesis, or any portion thereof, may not otherwise be copied or reproduced without the written consent of the copyright owner, except to the extent permitted by Canadian copyright law.