Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Defeasible Reasoning via Datalog$^\neg$

Michael J. Maher

TL;DR

The paper presents a metaprogramming-based method to compile the scalable defeasible logic ${ DL}(\partial_{||})$ into $Datalog^\neg$ under the well-founded semantics $WF91$, with a proof of correctness and a linear-size translation. By transforming a propositional Metaprogram of the defeasible theory into a stratified, rule-aware form, it enables sound approximations and efficient execution even on incomplete $Datalog^\neg$ engines. The work identifies structural properties of ${ DL}(\partial_{||})$ that support efficient implementation, innovation in partial evaluation and unfolding/folding transformations, and a detailed pathway from a defeasible theory to a practical, scalable logic-programming representation. The approach is generalizable to other defeasible logics and provides a blueprint for leveraging metaprograms to bridge nonmonotonic reasoning with mature logic-programming ecosystems, offering both exact and approximate execution strategies. These contributions advance scalable reasoning in defeasible logics and inform design choices for future defeasible systems and their implementations.

Abstract

We address the problem of compiling defeasible theories to Datalog$^\neg$ programs. We prove the correctness of this compilation, for the defeasible logic $DL(\partial_{||})$, but the techniques we use apply to many other defeasible logics. Structural properties of $DL(\partial_{||})$ are identified that support efficient implementation and/or approximation of the conclusions of defeasible theories in the logic, compared with other defeasible logics. We also use previously well-studied structural properties of logic programs to adapt to incomplete Datalog$^\neg$ implementations.

Defeasible Reasoning via Datalog$^\neg$

TL;DR

The paper presents a metaprogramming-based method to compile the scalable defeasible logic into under the well-founded semantics , with a proof of correctness and a linear-size translation. By transforming a propositional Metaprogram of the defeasible theory into a stratified, rule-aware form, it enables sound approximations and efficient execution even on incomplete engines. The work identifies structural properties of that support efficient implementation, innovation in partial evaluation and unfolding/folding transformations, and a detailed pathway from a defeasible theory to a practical, scalable logic-programming representation. The approach is generalizable to other defeasible logics and provides a blueprint for leveraging metaprograms to bridge nonmonotonic reasoning with mature logic-programming ecosystems, offering both exact and approximate execution strategies. These contributions advance scalable reasoning in defeasible logics and inform design choices for future defeasible systems and their implementations.

Abstract

We address the problem of compiling defeasible theories to Datalog programs. We prove the correctness of this compilation, for the defeasible logic , but the techniques we use apply to many other defeasible logics. Structural properties of are identified that support efficient implementation and/or approximation of the conclusions of defeasible theories in the logic, compared with other defeasible logics. We also use previously well-studied structural properties of logic programs to adapt to incomplete Datalog implementations.

Paper Structure

This paper contains 19 sections, 19 theorems, 14 equations.

Table of Contents

  1. Introduction
  2. Logic Programming
  3. Syntax and Structure of Logic Programs
  4. Semantics of Logic Programs
  5. Defeasible Logics
  6. The scalable defeasible logic ${ DL}(\partial_{||})$
  7. Metaprogram for ${ DL}(\partial_{||})$
  8. Transforming the Metaprogram
  9. Partial Evaluation of the Metaprogram
  10. More transformation
  11. The Resulting Program
  12. Correctness of the Metaprogram
  13. Properties of the Compiled Program
  14. Executing Compiled Theories
  15. Well-Founded Semantics
  16. ...and 4 more sections

Key Result

Theorem 1

Let $P$ be a logic program, ${\cal P} \subseteq \Pi$ be a downward-closed set of predicates with floor ${\cal F}$, let ${\cal Q}$ be ${\cal P}\backslash{\cal F}$, and $s$ be a signing for ${\cal Q}$. Let $I$ be a fixed semantics for ${\cal F}$ and $p \in {\cal Q}$.

Theorems & Definitions (39)

  • Theorem 1: signings
  • Example 2
  • Example 3
  • Example 4
  • Example 5
  • Proposition 6
  • proof
  • Proposition 7
  • proof
  • Example 8
  • ...and 29 more