Non-well-founded approach to terminological cycles

In this paper, we proposed 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 defined, 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, K-REP, consists of constructing accessible pointed graphs, representing terms in the universal concept algebra, and checking a simulation relation between terms.