逻辑程序设计
非单调逻辑
计算机科学
论证理论
证明理论
自认知逻辑
稳定模型语义
程序设计语言
理论计算机科学
论证框架
否定为失败
语义学(计算机科学)
有根据的语义学
数学证明
数学
操作语义
多模态逻辑
描述逻辑
指称语义学
认识论
哲学
几何学
标识
DOI:10.1093/logcom/9.4.515
摘要
In recent years, argumentation has been shown to be an appropriate framework in which logic programming with negation as failure as well as other logics for non-monotonic reasoning can be encompassed. Many of the existing semantics for negation as failure in logic programming can be understood in a uniform way using argumentation. Moreover, other logics for non-monotonic reasoning that can also be formulated via argumentation can be given new semantics, by a direct extension of the logic programming semantics. In this paper we develop an abstract computational framework where various argumentation semantics can be computed via different parametric variations of a simple basic proof theory. This proof theory is given in terms of derivations of trees where each node in a tree contains an argument (or attack) against its corresponding parent node. The proposed proof theory, defined here for the case of logic programming, generalizes directly to other logics for non-monotonic reasoning that can also be formalized via argumentation. The abstract proof theory forms the basis for developing concrete top-down proof procedures for query evaluation. These proof procedures are obtained by adopting specific search strategies and ways of computing attacks in the particular argumentation framework. For logic programming these procedures can be seen as a generalization of the Eshghi-Kowalski abductive proof procedure that in turn generalizes SLDNF.
科研通智能强力驱动
Strongly Powered by AbleSci AI