Defeasible Conditionals using Answer Set Programming

TL;DR

This paper introduces a novel ASP-based method for computing Rational Closure in defeasible reasoning, enabling automatic model construction and efficient entailment checking, with proven correctness and improved performance.

Contribution

It provides the first declarative ASP encoding for Rational Closure, facilitating automatic minimal model construction and entailment verification in defeasible logic.

Findings

ASP implementation correctly computes Rational Closure

The approach outperforms existing imperative solvers in efficiency

Formal proofs confirm the correctness of the ASP encoding

Abstract

Defeasible entailment is concerned with drawing plausible conclusions from incomplete information. A foundational framework for modelling defeasible entailment is the KLM framework. Introduced by Kraus, Lehmann, and Magidor, the KLM framework outlines several key properties for defeasible entailment. One of the most prominent algorithms within this framework is Rational Closure (RC). This paper presents a declarative definition for computing RC using Answer Set Programming (ASP). Our approach enables the automatic construction of the minimal ranked model from a given knowledge base and supports entailment checking for specified queries. We formally prove the correctness of our ASP encoding and conduct empirical evaluations to compare the performance of our implementation with that of existing imperative implementations, specifically the InfOCF solver. The results demonstrate that our ASP-based approach adheres to RC's theoretical foundations and offers improved computational efficiency.