@article{ait-kaci-jlp97,
author = {Hassan, Ait-Kaci and Podelski, Andreas and Goldstein, Seth
Copen},
title = {Order-sorted feature theory unification},
journal = {The Journal of Logic Programming},
volume = {30},
month = {Feb},
year = {1997},
abstract = {Order-sorted feature (OSF) terms provide an adequate
representation for objects as flexible records. They are sorted,
attributed, possibly nested structures, ordered thanks to a
subsort ordering. Sorts definitions offer the functionality of
classes imposing structural constraints on objects. These
constraints involve variable sorting and equations among feature
paths, including self-reference. Formally, sort definitions may
be seen as axioms forming an OSF theory. OSF theory unification
is the process of normalizing an OSF term taking into account
sort definitions, enforcing structural constraints imposed by an
OSF theory. It allows objects to inherit, and thus abide by,
constraints from their classes. We propose a formal system that
logically models record objects with (possibly recursive) class
definitions accommodating multiple inheritance. We show that OSF
theory unification is undecidable in general. However, we give a
set of confluent normalization rules which is complete for
detecting the inconsistency of an object with respect to an OSF
theory. Furthermore, a subset consisting of all rules but one is
confluent and terminating. This yields a practical complete
normalization strategy, as well as an effective compilation
scheme.},
pages = {99--124},
number = {2},
url = {http://www.cs.cmu.edu/~seth/papers/ait-kaci-jlp97.pdf},
doi = {doi:10.1016/S0743-1066(96)00053-2},
also = {Proceedings of the International Symposium on Logic
Programming (ILPS), 1993 and as DEC Technical Report PRL-RR-32},
keywords = {Logic Programming},
}