Abstract
In this paper, we address the issue of representing and reasoning about documents for which an explicit structure is provided. Specifically, we devise a framework where Document Type Definitions (DTDs) expressed in the Standard Generalized Markup Language (SGML) are formalized in an expressive Description Logic equipped with sound, complete, and terminating inference procedures. In this way, we provide a general reasoning mechanism that enables various reasoning tasks on DTDs, including the verification of typical forms of equivalences between DTDs, such as strong equivalence and structural equivalence, as well as parametric versions of these equivalences. Notably, this general reasoning mechanism allows for verifying structural equivalence in worst case deterministic exponential time, in contrast to the known algorithms which are double exponential. As a whole, the study in this paper provides some of the fundamental building blocks for developing articulated inference systems that support tasks involving the intelligent navigation of large document databases such as the World Wide Web.