Implementing Tabled Hypothetical Datalog

Hypothetical Datalog is based on an intuitionistic semantics rather than a classical logic semantics, and allows embedded implications in rule bodies. While the usual implication (i.e., the neck of a Horn clause) stands for inferencing facts, an embedded implication plays the role of assuming its premise for deriving its consequence. Although this topic has received considerable attention along time and nowadays is gaining renewed interest, there has not been a tabled implementation of hypothetical Datalog. We present here such a proposal including the formal background and its application to a goal-oriented tabled setting with negation, where non-monotonicity due to negation and implication is handled via stratification and contexts. In addition, we implement it in the deductive system DES, also providing support to duplicates and integrity constraints in the hypothetical framework.