Title: Grounding FO and FO(ID) with bounds
Authors: Wittocx, Johan ×
Mariƫn, Maarten
Denecker, Marc #
Issue Date: May-2010
Publisher: AI Access Foundation
Series Title: The Journal of Artificial Intelligence Research vol:38 pages:223-269
Abstract: 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 present our method for classical first-order logic (FO) theories. Then we extend it to FO(ID), the extension of FO with inductive definitions, which allows for more concise and comprehensive input theories. We discuss implementation issues and experimentally validate the practical applicability of our method.
ISSN: 1076-9757
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
wittocx10a.pdf Published 429KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science