A Non-Well-Founded Approach to Terminological Cycles

Abstract

In this paper, we propose a new approach to intensional semantics of term subsumption languages. We introduce concept algebras, whose signatures are given by sets of primitive concepts, roles, and the operations of the language. For a given set of variables, standard results give us free algebras. We next define, for a given set of concept definitions, a term algebra, as the quotient of the free algebra by a congruence generated by the definitions. The ordering on this algebra is called descriptive subsumption (⊒Δ). We also construct a universal concept algebra, as a non-well-founded set given by the greatest fixed point of a certain equation. The ordering on this algebra is called structural subsumption (≽Δ). We prove there are unique mappings from the free algebras, to each of these, and establish that our method for classifying cycles in a term subsumption language, KREP, consists of constructing accessible pointed graphs, representing terms in the universal concept algebra, and checking a simulation relation between terms.