文章基本信息

标题：Completeness of a Procedure to Calculate Logic Programs by Replacement with the Bodies of Rules and a Proof Procedure with Respect to a General Axiom
本地全文：下载
作者：Sumitaka Akiba
期刊名称：人工知能学会論文誌
印刷版ISSN：1346-0714
电子版ISSN：1346-8030
出版年度：2008
卷号：23
期号：2
页码：68-75
DOI：10.1527/tjsai.23.68
出版社：The Japanese Society for Artificial Intelligence
摘要：In this paper, a logic program is considered as the union of a set of rules and an axiom which defines basic predicates and functions, and a procedure to calculate logic programs is considered as the combination of a replacement procedure with the bodies of the rules and a proof procedure with respect to the axiom. It is proved that a goal is a logical consequence of Δ ∪ Γ if and only if there exists n such that the logical formula obtained by replacing atomic formulae in the goal n times is a logical consequence of Δ, where Γ is the set of the rules, and Δ is the axiom. Moreover, conditions concerning Γ and Δ are described.
关键词：logic program ; three-valued logic ; completeness ; ultraproduct