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

A parameterised hierarchy of argumentation semantics for extended logic programming and its application to the well-founded semantics

引用

theory and practice of logic programming 2005年第1-2期5卷 207-242页

作者： Schweimeier, R Schroeder, M Camtec Software GmbH D-12435 Berlin Germany Tech Univ Dresden Dept Comp Sci Dresden Germany

Argumentation has proved a useful tool in defining formal semantics for assumption-based reasoning by viewing a proof as a process in which proponents and opponents attack each others arguments by undercuts (attack to an argument's premise) and rebuts (attack to an argument's conclusion). In this paper, we formulate a variety of notions of attack for extended logic programs from combinations of undercuts and rebuts and define a general hierarchy of argumentation semantics parameterised by the notions of attack chosen by proponent and opponent. We prove the equivalence and subset relationships between the semantics and examine some essential properties concerning consistency and the coherence principle, which relates default negation and explicit negation. Most significantly, we place existing semantics put forward in the literature in our hierarchy and identify a particular argumentation semantics for which we prove equivalence to the paraconsistent well-founded semantics with explicit negation, WFSXp. Finally, we present a general proof theory, based on dialogue trees, and show that it is sound and complete with respect to the argumentation semantics.

关键词： non-monotonic reasoning extended logic programming argumentation semantics well-founded semantics with explicit negation

来源：评论

学校读者我要写书评

暂无评论

Specialization of functional logic programs based on needed narrowing

引用

theory and practice of logic programming 2005年第3期5卷 273-303页

作者： Alpuente, M Lucas, S Vidal, G Hanus, M Univ Politecn Valencia E-46020 Valencia Spain

Many functional logic languages are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction mechanism of functional languages and the resolution principle of logic languages. Needed narrowing is an optimal evaluation strategy which constitutes the basis of modern (narrowing-based) lazy functional logic languages. In this work, we present the fundamentals of partial evaluation in such languages. We provide correctness results for partial evaluation based on needed narrowing and show that the nice properties of this strategy are essential for the specialization process. In particular, the structure of the original program is preserved by partial evaluation and, thus, the same evaluation strategy can be applied for the execution of specialized programs. This is in contrast to other partial evaluation schemes for lazy functional logic programs which may change the program structure in a negative way. Recent proposals for the partial evaluation of declarative multi-paradigm programs use (some form of) needed narrowing to perform computations at partial evaluation time. Therefore, our results constitute the basis for the correctness of such partial evaluators.

关键词： partial evaluation functional logic programming needed narrowing

来源：评论

学校读者我要写书评

暂无评论

Schedulers and redundancy for a class of constraint propagation rules

引用

theory and practice of logic programming 2005年第4-5期5卷 441-465页

作者： Brand, S Apt, KR CWI NL-1090 GB Amsterdam Netherlands Natl Univ Singapore Singapore 117548 Singapore

We study here schedulers for a class of rules that naturally arise in the context of rule-based constraint programming. We systematically derive a scheduler for them from a generic iteration algorithm of Apt (2000). We apply this study to so-called membership rules of Apt and Monfroy (2001). This leads to an implementation that yields a considerably better performance for these rules than their execution as standard CHR rules. Finally, we show how redundant rules can be identified and how appropriately reduced sets of rules can be computed.

关键词： constraint programming rule-based programming constraint propagation

来源：评论

学校读者我要写书评

暂无评论

On termination of meta-programs

引用

theory and practice of logic programming 2005年第3期5卷 355-390页

作者： Serebrenik, A De Schreye, D TU LaQuSo NL-5600 MB Eindhoven Netherlands Katholieke Univ Leuven Dept Comp Sci B-3001 Heverlee Belgium

The term meta-programming refers to the ability of writing programs that have other programs as data and exploit their semantics. The aim of this paper is presenting a methodology allowing us to perform a correct termination analysis for a broad class of practical meta-interpreters, including negation and performing different tasks during the execution. It is based on combining the power of general orderings, used in proving termination of term-rewrite systems and programs, and on the well-known acceptability condition, used in proving termination of logic programs. The methodology establishes a relationship between the ordering needed to prove termination of the interpreted program and the ordering needed to prove termination of the meta-interpreter together with this interpreted program. If such a relationship is established, termination of one of those implies termination of the other one, i.e. the meta-interpreter preserves termination. Among the meta-interpreters that are analysed correctly are a proof trees constructing meta-interpreter, different kinds of tracers and reasoners.

关键词： termination analysis meta-programming meta-interpreter

来源：评论

学校读者我要写书评

暂无评论

Inferring termination conditions for logic programs using backwards analysis

引用

theory and practice of logic programming 2005年第1-2期5卷 75-91页

作者： Genaim, S Codish, M Univ Verona Dipartimento Informat Verona Italy Ben Gurion Univ Negev Dept Comp Sci IL-84105 Beer Sheva Israel

This paper focuses on the inference of modes for which a logic program is guaranteed to terminate. This generalises traditional termination analysis where an analyser tries to verify termination for a specified mode. Our contribution is a methodology in which components of traditional termination analysis are combined with backwards analysis to obtain an analyser for termination inference. We identify a condition on the components of the analyser which guarantees that termination inference will infer all modes which can be checked to terminate. The application of this methodology to enhance a traditional termination analyser to perform also termination inference is demonstrated.

关键词： program analysis abstract interpretation termination analysis backwards analysis

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Enhanced sharing analysis techniques: a comprehensive evaluation

引用

theory and practice of logic programming 2005年第1-2期5卷 1-43页

作者： Bagnara, R Zaffanella, E Hill, PM Univ Parma Dept Math Parma Italy Univ Leeds Sch Comp Leeds W Yorkshire England

Sharing, an abstract domain developed by D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information. It is well-known that a commonly used core of techniques, such as the integration of Sharing with freeness and linearity information, can significantly improve the precision of the analysis. However, a number of other proposals for refined domain combinations have been circulating for years. One feature that is common to these proposals is that they do not seem to have undergone a thorough experimental evaluation even with respect to the expected precision gains. In this paper we experimentally evaluate: helping Sharing with the definitely ground variables found using Pos, the domain of positive Boolean formulas;the incorporation of explicit structural information;a full implementation of the reduced product of Sharing and Pos;the issue of reordering the bindings in the computation of the abstract mgu;an original proposal for the addition of a new mode recording the set of variables that are deemed to be ground or free;a refilled way of using linearity to improve the analysis;the recovery of hidden information in the combination of Sharing with freeness information. Finally, we discuss the issue Of whether tracking compoundness allows the computation of more sharing information.

关键词： abstract interpretation logic programming sharing analysis experimental evaluation

来源：评论

学校读者我要写书评

暂无评论

A treatment of higher-order features in logic programming

引用

theory and practice of logic programming 2005年第3期5卷 305-354页

作者： Nadathur, G Univ Minnesota Digital Technol Ctr Minneapolis MN 55455 USA Univ Minnesota Dept Comp Sci & Engn Minneapolis MN 55455 USA

The logic programming paradigm provides the basis for a new intensional view of higher-order notions. This view is realized primarily by employing the terms of a typed lambda calculus as representational devices and by using a richer form of unification for probing their structures. These additions have important meta-programming applications but they also pose non-trivial implementation problems. One issue concerns the machine representation of lambda terms suitable to their intended use: an adequate encoding must facilitate comparison operations over terms in addition to supporting the usual reduction computation. Another aspect relates to the treatment of a unification operation that has a branching character and that sometimes calls for the delaying of the solution of unification problems. A final issue concerns the execution of goals whose structures become apparent only in the course of computation. These various problems are exposed in this paper and solutions to them are described. A satisfactory representation for lambda terms is developed by exploiting the nameless notation of de Bruijn as well as explicit encodings of substitutions. Special mechanisms are molded into the structure of traditional Prolog implementations to support branching in unification and carrying of unification problems over other computation steps;a premium is placed in this context on exploiting determinism and on emulating usual first-order behaviour. An extended compilation model is presented that treats higher-order unification and also handles dynamically emergent goals. The ideas described here have been employed in the Teyjus implementation of the lambda Prolog language, a fact that is used to obtain a preliminary assessment of their efficacy.

关键词： lambda calculus intensional higher-order programming higher-order unification abstract machine compilation

来源：评论

学校读者我要写书评

暂无评论

Optimization of bound disjunctive queries with constraints

引用

theory and practice of logic programming 2005年第6期5卷 713-745页

作者： Greco, G Greco, S Trubitsyna, I Zumpano, E Univ Calabria DEIS I-87030 Arcavacata Di Rende Italy

This paper presents a technique for the optimization of bound queries over disjunctive deductive databases with constraints. The proposed approach is an extension of the well-known Magic-Set technique and is well-suited for being integrated in current bottom-up (stable) model inference engines. More specifically, it is based on the exploitation of binding propagation technique, which reduce the size of the data relevant to answer the query and, consequently, reduces both the complexity of computing a single model and the number of models to be considered. The motivation of this work stems from the observation that traditional binding propagation optimization techniques for bottom-up model generator systems, simulating the goal driven evaluation of top-down engines, are only suitable for positive (disjunctive) queries, while hard problems are expressed using unstratified negation. The main contribution of the paper consists in the extension of a previous technique, defined for positive disjunctive queries, to queries containing both disjunctive heads and constraints (a simple and expressive form of unstratified negation). As the usual way of expressing declaratively hard problems is based on the guess-and-check technique, where the guess part is expressed by means of disjunctive rules and the check part is expressed by means of constraints, the technique proposed here is highly relevant for the optimization of queries expressing hard problems. The value of the technique has been proved by several experiments.

关键词： Disjunctive Datalog constraints theory magic set technique

来源：评论

学校读者我要写书评

暂无评论

Normal forms for Answer Sets programming

引用

theory and practice of logic programming 2005年第6期5卷 747-760页

作者： Costantini, S Provetti, A Univ Aquila Dipartimento Informat I-67100 Laquila Italy Univ Messina Dipartimento Fis I-98166 Messina Italy

Normal forms for logic programs under stable/answer set semantics are introduced. We argue that these forms can simplify the study of program properties, mainly consistency. The first normal form, called the kernel of the program, is useful for studying existence and number of answer sets. A kernel program is composed of the atoms which are undefined in the Well-founded semantics, which are those that directly affect the existence of answer sets. The body of rules is composed of negative literals only. Thus, the kernel form tends to be significantly more compact than other formulations. Also, it is possible to check consistency of kernel programs in terms of colorings of the Extended Dependency Graph program representation which we previously developed. The second normal form is called 3-kernel. A 3-kernel program is composed of the atoms which are undefined in the Well-founded semantics. Rules in 3-kernel programs have at most two conditions, and each rule either belongs to a cycle, or defines a connection between cycles. 3-kernel programs may have positive conditions. The 3-kernel normal form is very useful for the static analysis of program consistency, i.e. the syntactic characterization of existence of answer sets. This result can be obtained thanks to a novel graph-like representation of programs, called Cycle Graph which presented in the companion article Costantini (2004b).

关键词： answer set programming program transformation normal forms

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：