Preparing a First-Order Knowledge Base for Fast Inference
Helmut Prendinger, Mitsuru Ishizuka · 1999
This paper presents an effective method to encode function-free first-order Horn theories in propositional logic. To keep the resulting theory within manageable size, we employ techniques from (ir)relevance reasoning and theory transformation. Our approach allows for the compactness of knowledge representation in first-order logic and the efficiency of propositional reasoning mechanisms. The empirical evaluation with a hypothetical reasoning mechanism indicates that our approach has the potential to solve notoriously hard problems in diagnosis, planning, and vision. Introduction and Motivation Declarative knowledge generated by a knowledge engineer is not always in a form that can be efficiently processed by present-day reasoning mechanisms. In particular, knowledge bases should at least have the expressiveness of first-order Horn clauses, and it is wellknown that reasoning with first-order theories is computationally expensive. On the other hand, in recent years considerable progress...