Grounding with Bounds

Johan Wittocx, Maarten Mariën, Marc Denecker

Grounding is the task of reducing a first-order theory to an equivalent propositional one. Typical grounders work on a sentence-by-sentence level, substituting variables by domain elements and simplifying where possible. In this work, we propose a method for reasoning on the first-order theory as a whole to optimize the grounding process. Concretely, we develop an algorithm that computes bounds for subformulas. Such bounds indicate for which tuples the subformulas are certainly true and for which they are certainly false. These bounds can then be used by standard grounding algorithms to substantially reduce grounding sizes, and consequently also grounding times. We have implemented the method, and demonstrate its practical applicability.

Subjects: 11. Knowledge Representation; 15. Problem Solving

Submitted: Apr 15, 2008

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.