检索结果-内蒙古大学图书馆

An infinite-game semantics for well-founded negation in logic programming

ANNALS OF PURE AND APPLIED logic 2008年第2-3期151卷 70-88页

作者： Galanaki, Chrysida Rondogiannis, Panos Wadge, William W. Univ Athens Dept Informat & Telecommun Athens 15784 Greece Univ Victoria Dept Comp Sci Victoria BC V8W 3P6 Canada

We present an infinite-game characterization of the well-founded semantics for function-free logic programs with negation. Our game is a simple generalization of the standard game for negation-less logic programs introduced by van Emden [M.H. van Emden, Quantitative deduction and its fixpoint theory, Journal of logic programming 3 (1) (1986) 37-53] in which two players, the Believer and the Doubter, compete by trying to prove (respectively disprove) a query. The standard game is equivalent to the minimum Herbrand model semantics of logic programming in the sense that a query succeeds in the minimum model semantics iff the Believer has a winning strategy for the game which begins with the Doubter doubting this query. The game for programs with negation that we propose follows the same rules as the standard one, except that the players swap roles every time the play "passes through" negation. We start our investigation by establishing the determinacy of the new game by using some classical tools from the theory of infinite-games. Our determinacy result immediately provides a novel and purely. game-theoretic characterization of the semantics of negation in logic programming. We proceed to establish the connections of the game semantics to the existing semantic approaches for logic programming with negation. For this purpose, we first define a refined version of the game that uses degrees of winning and losing for the two players. We then demonstrate that this refined game corresponds exactly to the infinite-valued minimum model semantics of negation [P. Rondogiannis,W.W. Wadge, Minimum model semantics for logic programs with negation-as-failure, ACM Transactions on Computational logic 6 (2) (2005) 441-467]. This immediately implies that the unrefined game is equivalent to the well-founded semantics (since the infinite-valued semantics is a refinement of the well-founded semantics). (c) 2007 Elsevier B.V. All rights reserved.

关键词： semantics of logic programming negation in logic programming infinite games

来源：评论

学校读者我要写书评

暂无评论

logic programming with default, weak and strict negations

引用

THEORY AND PRACTICE OF logic programming 2006年第6期6卷 737-749页

作者： Yamasaki, Susumu Okayama Univ Grad Sch Nat Sci & Technol Dept Comp Sci Okayama 7008530 Japan

This paper looks at logic programming with three kinds of negation: default, weak and strict negations. A 3-valued logic model theory is discussed for logic programs with three kinds of negation. The procedure is cons... 详细信息

关键词： negation in logic programming 3-valued logic

来源：评论

学校读者我要写书评

暂无评论

Strong equivalence of logic programs under the infinite-valued semantics

引用

INFORMATION PROCESSING LETTERS 2009年第11期109卷 576-581页

作者： Nomikos, Christos Rondogiannis, Panos Wadge, William W. Univ Athens Dept Informat & Telecommun Athens 15784 Greece Univ Ioannina Dept Comp Sci GR-45110 Ioannina Greece Univ Victoria Dept Comp Sci Victoria BC V8W 3P6 Canada

We consider the notion of strong equivalence [V. Lifschitz, D. Pearce, A. Valverde, Strongly equivalent logic programs, ACM Transactions on Computational logic 2 (4) (2001) 526-541] of normal propositional logic programs under the infinite-valued semantics [P. Rondogiannis, W.W. Wadge, Minimum model semantics for logic programs with negation-as-failure, ACM Transactions on Computational logic 6 (2) (2005) 441-467] (which is a purely model-theoretic semantics that is compatible with the well-founded one). We demonstrate that two such programs are strongly equivalent under the infinite-valued semantics if and only if they are logically equivalent in the corresponding infinite-valued logic. In particular, we show that strong equivalence of normal propositional logic programs is decidable, and more specifically coNP-complete. Our results have a direct implication for the well-founded semantics since, as we demonstrate, if two programs are strongly equivalent under the infinite-valued semantics, then they are also strongly equivalent under the well-founded semantics. (C) 2009 Elsevier B.V. All rights reserved.

关键词： Formal semantics negation in logic programming Strong equivalence

来源：评论

学校读者我要写书评

暂无评论

Proving correctness and completeness of normal programs - a declarative approach

引用

THEORY AND PRACTICE OF logic programming 2005年第6期5卷 669-711页

作者： Drabent, W Milkowska, M Polish Acad Sci Inst Comp Sci PL-01237 Warsaw Poland Linkoping Univ Dept Comp & Informat Sci S-58183 Linkoping Sweden Warsaw Univ Inst Informat PL-02097 Warsaw Poland

We advocate a declarative approach to proving properties of logic programs. Total correctness can be separated into correctness, completeness and clean termination;the latter includes nonfloundering. Only clean termination depends on the operational semantics, in particular on the selection rule. We show how to deal with correctness and completeness in a declarative way, treating programs only from the logical point of view. Specifications used in this approach are interpretations (or theories). We point out that specifications for correctness may differ from those for completeness, as usually there are answers which are neither considered erroneous nor required to be computed. We present proof methods for correctness and completeness for definite programs and generalize them to normal programs. For normal programs we use the 3-valued completion semantics;this is a standard semantics corresponding to negation as finite failure. The proof methods employ solely the classical 2-valued logic. We use a 2-valued characterization of the 3-valued completion semantics, which may be of separate interest. The method of proving correctness of definite programs is not new and can be traced back to the work of Clark in 1979. However a more complicated approach using operational semantics was proposed by some authors. We show that it is not stronger than the declarative one, as far as properties of program answers are concerned. For a corresponding operational approach to normal programs, we show that it is (strictly) weaker than our method. We also employ the ideas of this work to generalize a known method of proving termination of normal programs.

关键词： declarative programming negation in logic programming specifications program correctness and completeness termination teaching logic programming

来源：评论

学校读者我要写书评

暂无评论

Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order logic Programs

引用

THEORY AND PRACTICE OF logic programming 2018年第3-4期18卷 421-437页

作者： Charalambidis, Angelos Rondogiannis, Panos Symeonidou, Ioanna Univ Athens Dept Informat & Telecommun Athens Greece

We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of the type hierarchy. We prove that there exists a bijection between such Fitting-monotonic functions and pairs of two-valued-result functions where the first member of the pair is monotone-antimonotone and the second member is antimonotone-monotone. By deriving an extension of consistent approximation fixpoint theory (Denecker et al. 2004) and utilizing the above bijection, we define an iterative procedure that produces for any given higher-order logic program a distinguished extensional model. We demonstrate that this model is actually a minimal one. Moreover, we prove that our construction generalizes the familiar well-founded semantics for classical logic programs, making in this way our proposal an appealing formulation for capturing the well-founded semantics for higher-order logic programs.

关键词： Higher-Order logic programming negation in logic programming Approximation Fixpoint Theory

来源：评论

学校读者我要写书评

暂无评论

The intricacies of three-valued extensional semantics for higher-order logic programs

引用

THEORY AND PRACTICE OF logic programming 2017年第5-6期17卷 974-991页

作者： Rondogiannis, Panos Symeonidou, Ioanna Univ Athens Athens Greece

M. Bezem defined an extensional semantics for positive higher-order logic programs. Recently, it was demonstrated by Rondogiannis and Symeonidou that Bezem's technique can be extended to higher-order logic programs with negation, retaining its extensional properties, provided that it is interpreted under a logic with an infinite number of truth values. Rondogiannis and Symeonidou also demonstrated that Bezem's technique, when extended under the stable model semantics, does not in general lead to extensional stable models. In this paper, we consider the problem of extending Bezem's technique under the well-founded semantics. We demonstrate that the well-founded extension fails to retain extensionality in the general case. On the positive side, we demonstrate that for stratified higher-order logic programs, extensionality is indeed achieved. We analyze the reasons of the failure of extensionality in the general case, arguing that a three-valued setting cannot distinguish between certain predicates that appear to have a different behaviour inside a program context, but which happen to be identical as three-valued relations.

关键词： Extensional higher-order logic programming negation in logic programming

来源：评论

学校读者我要写书评

暂无评论

The intricacies of three-valued extensional semantics for higher-order logic programs

The intricacies of three-valued extensional semantics for hi...

引用

33rd International Conference on logic programming colocated with the 23rd International Conference on Principles and Practice of Constraint programming / 20th International Conference on Theory and Applications of Satisfiability Testing

作者： Rondogiannis, Panos Symeonidou, Ioanna Univ Athens Athens Greece

关键词： Extensional higher-order logic programming negation in logic programming

来源：评论

学校读者我要写书评

暂无评论

A real implementation for constructive negation

引用

19th International Conference on logic programming

作者： Muñoz, S Moreno-Navarro, JJ Univ Politecn Madrid Fac Informat LSIIS Madrid 28660 Spain

ISBN: (纸本)3540206426

logic programming has been advocated as a language for system specification, especially for logical behaviours, rules and knowledge. However, modeling problems involving negation, which is quite natural in many cases, is somewhat restricted if Prolog is used as the specification/implementation language. These constraints are not related to theory viewpoint, where users can find many different models with their respective semantics; they concern practical implementation issues. The negation capabilities supported by current Prolog systems are rather limited, and a correct and complete implementation there is not available. Of all the proposals, constructive negation [1,2] is probably the most promising because it has been proven to be sound and complete [4], and its semantics is fully compatible with Prolog’s.

关键词： constructive negation negation in logic programming constraint logic programming implementations of logic programming

来源：评论

学校读者我要写书评

暂无评论

Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order logic Programs

Approximation Fixpoint Theory and the Well-Founded Semantics...

引用

34th International Conference on logic programming (ICLP)

作者： Charalambidis, Angelos Rondogiannis, Panos Symeonidou, Ioanna Univ Athens Dept Informat & Telecommun Athens Greece

关键词： Higher-Order logic programming negation in logic programming Approximation Fixpoint Theory

来源：评论

学校读者我要写书评

暂无评论

EXTENSION AL SEMANTICS FOR HIGHER-ORDER logic PROGRAMS WITH negation

引用

logicAL METHODS IN COMPUTER SCIENCE 2018年第2期14卷

作者： Rondogiannis, Panos Symeonidou, Ioanna Univ Athens Dept Informat & Telecommun Athens Greece

We develop an extensional semantics for higher-order logic programs with negation, generalizing the technique that was introduced in [2, 3] for positive higher-order programs. In this way we provide an alternative extensional semantics for higher-order logic programs with negation to the one proposed in [6]. We define for the language we consider the notions of stratification and local stratification, which generalize the familiar such notions from classical logic programming, and we demonstrate that for stratified and locally stratified higher-order logic programs, the proposed semantics never assigns the unknown truth value. We conclude the paper by providing a negative result: we demonstrate that the well-known stable model semantics of classical logic programming, if extended according to the technique of [2, 3] to higher-order logic programs, does not in general lead to extensional stable models.

关键词： Higher-Order logic programming negation in logic programming Extensional Semantics

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：