Supervisor

Suitable for

Abstract

In a seminal paper, Selman and Kautz proposed a resolution-based algorithm for compiling a set of propositional clauses S into a set of Horn clauses H such that every Horn consequence in S is derivable from H too.

This algorithm was subsequently extended to first-order logic, but without any termination guarantees.

Recently, this classical knowledge compilation technique based on resolution has found a novel application in the area of ontology reasoning. In particular, it can be used for “encoding away” disjunctive axioms in ontologies while preserving (for every data set) answers to practically relevant queries.

The main goal of the project is to implement the classical resolution-based knowledge compilation algorithm for a given fragment of first-order logic, optimize it and test it on a library of realistic ontologies. The results of the project could be used to assess the applicability of mainstream knowledge compilation techniques to ontology reasoning.

Prerequisites: Logic and Proof, Knowledge Representation and Reasoning; Optional: Theory of Data and Knowledge Bases