Defeasible Reasoning via Datalog$^\neg$

TL;DR

This paper presents a method to compile defeasible theories into Datalog$^ eg$ programs, proving correctness for a specific defeasible logic and identifying properties that enable efficient implementation and approximation.

Contribution

It introduces a verified compilation approach from defeasible logic to Datalog$^ eg$, applicable to various defeasible logics and supporting efficient reasoning.

Findings

Proves correctness of the compilation for DL(∂₍∥₎)

Identifies structural properties supporting efficient implementation

Adapts properties of logic programs for incomplete Datalog$^ eg$ 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.