25.01. Fred Freitas: A Connection Method for Reasoning with the Description Logic ALC

The connection method earned good reputation in the field of automated theorem proving for around three decades, due to its simplicity, clarity and parsimonious use of memory. It employs easy to understand and implement matrices that deal with formulae and theorems directly, in opposition to the classical refutation methods like resolution and tableaux, which require formulae to be negated.

Such distinctive features attracted our attention in order to propose a connection method especially tailored to infer over description logic (DL) Semantic Web ontologies. This work is a first formal attempt in this direction. First, we present the Description Logic family of languages, focusing in the basic one ALC; then an ALC normal form which saves columns in the matrix is proposed, and then our ALC connection method is formalized in sequent style, although matrices should be employed instead of sequents for practical reasons.

The inference system has some interesting features: it is able to perform all four classical DL reasoning services (subsumption, inconsistency checking, equivalence, subsumption and disjointness) and, as the most widespread DL tableaux systems, reduces them to subsumption or validity (instead of unsatisfiability, which is used by the other refutation methods). Future work includes extending the approach to other more expressive DL languages.