Hostname: page-component-74656f9884-54qdv Total loading time: 0 Render date: 2026-11-10T13:25:04.011Z Has data issue: false hasContentIssue false

Compiling Input* FO(·) inductive definitions into tabled prolog rules for IDP3

Published online by Cambridge University Press:  25 September 2013

JOACHIM JANSEN
Affiliation:
Department of Computer Science, KU Leuven (e-mail: firstname.secondname@cs.kuleuven.be, albert.jorissen@ulyssis.org)
ALBERT JORISSEN
Affiliation:
Department of Computer Science, KU Leuven (e-mail: firstname.secondname@cs.kuleuven.be, albert.jorissen@ulyssis.org)
GERDA JANSSENS
Affiliation:
Department of Computer Science, KU Leuven (e-mail: firstname.secondname@cs.kuleuven.be, albert.jorissen@ulyssis.org)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

FO(·)IDP3 extends first-order logic with inductive definitions, partial functions, types and aggregates. Its model generator IDP3 first grounds the theory and then uses search to find the models. The grounder uses Lifted Unit Propagation (LUP) to reduce the size of the groundings of problem specifications in IDP3. LUP is in general very effective, but performs poorly on definitions of predicates whose two-valued interpretation can be computed from data in the input structure. To solve this problem, a preprocessing step is introduced that converts such definitions to Prolog code and uses XSB Prolog to compute their interpretation. The interpretation of these predicates is then added to the input structure, their definitions are removed from the theory and further processing is done by the standard IDP3 system. Experimental results show the effectiveness of our method.

Information

Type
Regular Papers
Copyright
Copyright © 2013 [JOACHIM JANSEN, ALBERT JORISSEN and GERDA JANSSENS]