Computing change and specificity with equational logic programs

Recent deductive approaches to reasoning about action and chance allow us to model objects and methods in a deductive framework. In these approaches, inheritance of methods comes for free, whereas overriding of methods is unsupported. In this paper, we present an equational logic framework for objects, methods, inheritance and overriding of methods. Overriding is achieved via the concept of specificity, which states that more specific methods are preferred to less specific ones. Specificity is computed with the help of negation as failure. We specify equational logic programs and show that their completed versions behave as intended. Furthermore, we prove that SLDENF-resolution is complete if the equational theory is finitary, the completed programs are consistent and no derivation flounders or is infinite. Moreover, we give syntactic conditions which guarantee that no derivation flounders or is infinite. Finally, we discuss how the approach can be extended to reasoning about the past in the context of incompletely specified objects or situations. It will turn out that constructive negation is needed to solve these problems.