Sciweavers

JAIR
2010

Grounding FO and FO(ID) with Bounds

13 years 2 months ago
Grounding FO and FO(ID) with Bounds
Grounding is the task of reducing a first-order theory and finite domain to an equivalent propositional theory. It is used as preprocessing phase in many logic-based reasoning systems. Such systems provide a rich first-order input language to a user and can rely on efficient propositional solvers to perform the actual reasoning. Besides a first-order theory and finite domain, the input for grounders contains in many applications also additional data. By exploiting this data, the size of the grounder’s output can often be reduced significantly. A common practice to improve the efficiency of a grounder in this context is by manually adding semantically redundant information to the input theory, indicating where and when the grounder should exploit the data. In this paper we present a method to compute and add such redundant information automatically. Our method therefore simplifies the task of writing input theories that can be grounded efficiently by current systems. We first...
Johan Wittocx, Maarten Mariën, Marc Denecker
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where JAIR
Authors Johan Wittocx, Maarten Mariën, Marc Denecker
Comments (0)