Helmut Prendinger and Mitsuru Ishizuka, University of Tokyo
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.