Connection Method for Defeasible Description Logics

Abstract

The modelling of exceptions in ontologies, provided through defeasible logics, and the reasoning behind their presence have received significant attention in the last decade. The development

of proof methods for defeasible Description Logics (DLs), following the methods for classi- cal DLs, is mainly based on semantic tableaux. However, the literature offers equally viable

alternatives for developing automatic theorem provers, such as the connection method. This

method consists of a goal-oriented proof search algorithm for connections (pairs of comple- mentary literals) in sets of literal clauses called a matrix. This thesis presents a connection

method for a family of exception-tolerant DLs. The work presents the following contributions: (i) definition of a matrix representation of a knowledge base that establishes conditions for a given axiom to be provable by the matrix; (ii) definition of a blocking condition in the presence of typicality operators; (iii) providing a bond between the matrix structures of the proposed method and the semantics of defeasible DLs; (iv) proofs of correctness, completeness and termination for the proposed inference system, grounded only on the semantics of defeasible

description logics; and (v) an architecture of polymorphic connection method provers, Poly- CoP, developed for the ALCH∙

language. Such an architecture can encompass any other logic,

with subtle modifications in its methods and classes.