常规逻辑程序中扩展的ASP表和规则冗余
Extended ASP tableaux and rule redundancy in normal logic programs
摘要：
我们介绍了一个扩展的tableau演算的答案集编程（ASP）。证明系统基于[Gebser&Schaub，ICLP 2006]中定义的ASP表，并添加了扩展规则。我们从理论和经验两方面研究了扩展ASP表的功能。本文研究了扩展ASP表与Tseitin定义的子句集扩展归结证明系统的关系，并通过对一类正规逻辑程序P_n给出多项式长度证明，将扩展ASP表与ASP表分开，其中ASP表具有关于n的指数长度极小证明.此外，扩展ASP表格意味着有趣的洞察力的影响，程序简化的长度证明在ASP。密切相关的扩展ASP表格，我们实证研究的ASP解决效率的冗余规则的效果。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
英文摘要：
We introduce an extended tableau calculus for answer set programming (ASP). The proof system is based on the ASP tableaux defined in [Gebser&Schaub, ICLP 2006], with an added extension rule. We investigate the power of Extended ASP Tableaux both theoretically and empirically. We study the relationship of Extended ASP Tableaux with the Extended Resolution proof system defined by Tseitin for sets of clauses, and separate Extended ASP Tableaux from ASP Tableaux by giving a polynomial-length proof for a family of normal logic programs P_n for which ASP Tableaux has exponential-length minimal proofs with respect to n. Additionally, Extended ASP Tableaux imply interesting insight into the effect of program simplification on the lengths of proofs in ASP. Closely related to Extended ASP Tableaux, we empirically investigate the effect of redundant rules on the efficiency of ASP solving. To appear in Theory and Practice of Logic Programming (TPLP).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
