Johan Wittocx, Maarten Mariën, Marc Denecker
Many computational settings are concerned with finding (all) models of a first-order logic theory for a fixed, finite domain. In this paper, we present a method to compute from a given theory and finite domain an approximate structure: a structure that approximates all models. We show confluence of this method and investigate its complexity. We discuss some applications, including 3-valued query answering in integrated and partially incomplete databases, and improved grounding in the context of model expansion for first-order logic.
Subjects: 11. Knowledge Representation; 3. Automated Reasoning
Submitted: Jun 12, 2008