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.
翻译:可废止蕴涵关注于从不完整信息中得出合理结论。KLM框架是建模可废止蕴涵的基础性框架,由Kraus、Lehmann和Magidor提出,该框架阐述了可废止蕴涵的若干关键性质。该框架中最著名的算法之一是理性闭包(RC)。本文提出了一种使用回答集编程(ASP)计算RC的声明式定义方法。我们的方法能够从给定知识库自动构建最小分级模型,并支持对特定查询进行蕴涵检查。我们形式化证明了ASP编码的正确性,并通过实证评估将我们实现的性能与现有命令式实现(特别是InfOCF求解器)进行对比。结果表明,我们基于ASP的方法遵循RC的理论基础,并提供了更高的计算效率。