Resolution for Feature Logics

A common approach to combine the object-oriented and logic programming paradigms is to formulate a set of inference rules for an object logic. We show how resolution is expressed using the full feature logic. In contrast to similar approaches we do not only exchange the underlying term universe but discard the predicate calculus completely. We demonstrate that an untyped resolution violates a closed world assumption and introduce a type discipline to solve this problem. To integrate inheritance into this framework we introduce polymorphic types and rules.