IEEE 25th International Conference on Tools with Artificial Intelligence, ICTAI 2013, Washinton, USA, November 4-6, 2013 pages:1068-1075
International Conference on Tools For Aritificial Intelligence location:Washington D.C. date:4-6 Nov 2013
The traditional approach to model expansion (generating models of a logic theory extending a partial structure) is to reduce the theory to a propositional language and apply a search algorithm to the resulting theory.
Function symbols are typically replaced by predicate symbols representing the graph of the function, an operation that blows up the reduced theory.In this paper, we present an improved approach to handle function symbols in a ground-and-solve methodology, building on ideas from Constraint Programming.We do so in the context of FO(.)^IDP, the knowledge representation language that extends First-Order logic with, among others, inductive definitions, arithmetic and aggregates.A model expansion algorithm is developed, consisting of(i) a grounding algorithm for FO(.)^IDP that is parametrized by the function symbols the are allowed to occur in the reduced theory, and (ii) a search algorithm for unrestricted, ground FO(.)^IDP. The ideas are implemented within the IDP knowledge-base system and experimental evaluation shows that both more compact groundings and improved search performance are obtained.