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

An abductive proof procedure for reasoning about actions in modal logic programming 2nd

2nd international workshop on Non-Monotonic extensions of logic programming

作者： Baldoni, M Giordano, L Martelli, A Patti, V Univ Turin Dipartimento Informat I-10149 Turin Italy

ISBN: (纸本)3540628436

In this paper we propose a modal approach for reasoning about actions in a logic programming framework. We introduce a modal language which makes use of abductive assumptions to deal with persistency, and provides a solution to the ramification problem, by allowing one-way "causal rules" to be defined among fluents. We define the abductive semantics of the language and a goal directed abductive proof procedure to compute abductive solutions for a goal from a given domain description. Both the semantics and the procedure are defined within the argumentation framework. In particular, we focus on a specific semantics, which is essentially an extension of Dung's admissibility semantics to a modal setting. The proof procedure is proved to be sound with respect to this semantics.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Model checking linear logic specifications

引用

THEORY And PRACTICE OF logic programming 2004年第5-6期4卷 573-619页

作者： Bozzano, M DelZanno, G Martelli, M IRST ITC I-38050 Trento Italy Univ Genoa Dipartimento Informat & Sci Informaz I-16146 Genoa Italy

The overall goal of this paper is to investigate the theoretical foundations of algorithmic verification techniques for first order linear logic specifications. The fragment of linear logic we consider in this paper is based on the linear logic programming language called LO (Andreoli and Pareschi, 1990) enriched with universally quantified goal formulas. Although LO was originally introduced as a theoretical foundation for extensions of logic programming languages, it can also be viewed as a very general language to specify a wide range of infinite-state concurrent systems (Andreoli, 1992;Cervesato, 1995). Our approach is based on the relation between backward reachability and provability highlighted in our previous work on propositional LO programs (Bozzano et al., 2002). Following this line of research, we define here a general framework for the bottom-up evaluation of first order linear logic specifications. The evaluation procedure is based on an effective fixpoint operator working on a symbolic representation of infinite collections of first order linear logic formulas. The theory of well quasi-orderings (Abdulla et al., 1996;Finkel and Schnoebelen, 2001) can be used to provide sufficient conditions for the termination of the evaluation of non trivial fragments of first order linear logic.

关键词： linear logic fixpoint semantics bottom-up evaluation

来源：评论

学校读者我要写书评

暂无评论

CONFLUENCE OF THE DISJOINT UNION OF COndITIONAL TERM REWRITING-SYSTEMS 2nd

引用

2nd international workshop ON COndITIONAL And TYPED REWRITING SYSTEMS

作者： MIDDELDORP, A Centre for Mathematics and Computer Science Kruislaan 413 Amsterdam 1098 SJ Netherlands

ISBN: (纸本)3540543171

Toyama proved that confluence is a modular property of term rewriting systems. This means that the disjoint union of two confluent term rewriting systems is again confluent. In this paper we extend his result to the class of conditional term rewriting systems. In view of the important role of conditional rewriting in equational logic programming, this result may be of relevance in integrating functional programming and logic programming. © Springer-Verlag Berlin Heidelberg 1991.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Computation of non-ground disjunctive well-founded semantics with constraint logic programming 2nd

引用

2nd international workshop on Non-Monotonic extensions of logic programming

作者： Dix, J Stolzenburg, F Univ Koblenz Dept Comp Sci D-56075 Koblenz Germany

ISBN: (纸本)3540628436

Impressive work has been done in the last;years concerning the meaning of negation and disjunction in logic programs, but most of this research concentrated on propositional programs only. While it suffices to consider the propositional case for investigating general properties and the overall behaviour of a semantics, we feel that for real applications and for computational purposes an implementation should be able to handle first-order programs without grounding them. In this paper we present a theoretical framework by defining a calculus of program transformations that apply directly to rules with variables and function symbols. Our main results are that (1) this calculus is confluent for arbitrary programs, (2) for finite ground programs it is equivalent to a terminating calculus introduced by Brass and Dir (1995), and (3) it approximates a generalisation of D-WFS for arbitrary programs. We achieve this by transforming program rules into rules with equational constraints thereby using heavily methods and techniques from constraint logic programming. In particular, disconnection-methods play a crucial role. In principle, any constraint theory known from the field of constraint logic programming can be exploited in the context of nonmonotonic reasoning, not only equational constraints over the Herbrand domain. However, the respective constraint solver must be able to treat negative constraints of the considered constraint domain. In summary, this work yields the basis for a general combination of two paradigms: constraint logic programming and non-monotonic reasoning.

关键词： constraint logic programming equational constraints disjunctive logic programming well-founded semantics non-monotonic reasoning

来源：评论

学校读者我要写书评

暂无评论

The near-horn approach to disjunctive logic programming 2nd

The near-horn approach to disjunctive logic programming

引用

2nd international workshop on extensions of logic programming, elp 1991

作者： Reed, David W. Loveland, Donald W. Smith, Bruce T. Department of Computer Science Duke University DurhamNC27706 United States Department of Computer Science University of North Carolina Chapel HillNC27599 United States

ISBN: (纸本)9783540554981

This paper presents an overview of the near-Horn Prolog project at Duke University. The basic goal behind this project has been to extend Prolog to disjunctive logic programs (and thus full first-order expressibility) while retaining as much of the clarity and procedural simplicity of Prolog as possible. The approach taken to achieve this goal has been to combine Prolog with case analysis reasoning. The research work within the project can roughly be divided into three areas: procedure design, semantics, and implementation. Three different variants of Near-Horn Prolog have been devised, of which the most recent, Inheritance near-Horn Prolog (InH-Prolog), is the variant currently being favored. The semantics for the near-Horn Prologs, specifically for InH-Prolog, have been investigated, resulting in a case-analysis based fixpoint semantics which mimics the procedural behavior of InH-Prolog. Also, both classical and default negation have been incorporated into the neaz-Horn Prolog systems. Finally, an interpreter for the original near-Horn Prolog variant has been implemented, and a compiler for the Intt-Prolog variant is currently nearing completion. © Springer-Verlag Berlin Heidelberg 1992.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

2nd international workshop on programming Language Implementation and logic programming, PLILP 1990

引用

2nd international workshop on programming Language Implementation and logic programming, PLILP 1990

ISBN: (纸本)9783540530107

The proceedings contain 26 papers. The special focus in this conference is on programming Language Implementation and logic programming. The topics include: Implementing parallel rewriting;a new data structure for implementing extensions to prolog;finding the least fixed point using wait-declarations in Prolog;elementary logic programs;a new Presburger arithmetic decision procedure based on extended prolog execution;reasoning about programs with effects;towards a characterization of termination of logic programs;static type analysis of prolog procedures for ensuring correctness;integrating strict and lazy evaluation: The λ-calculus;efficient data representation in polymorphic languages;a logic-based approach to data flow analysis problems (Preliminary version);compilation of narrowing;systematic semantic approximations logic programs;interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity;on the automatic generation of events in Delta Prolog;compilation of non-linear, second order patterns on s-expressions;pattern matching in a functional transformation language using treeparsing;logic programming within a functional framework;compiling logic programs with equality;inference-based overloading resolution for ADA;an approach to verifiable compiling specification and prototyping;bug localization by algorithmic debugging and program slicing;a constraint logic programming shell;modifying the simplex algorithm to a constraint solver;implementing a meta-logical scheme;the Vienna abstract machine.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Transformation-based bottom-up computation of the well-founded model 2nd

引用

2nd international workshop on Non-Monotonic extensions of logic programming

作者： Brass, S Zukowski, U Freitag, B Univ Hildesheim Inst Informat D-31141 Hildesheim Germany Univ Passau Fak Math & Informat D-94030 Passau Germany

ISBN: (纸本)3540628436

We present a bottom-up algorithm for the computation of the well-founded model of non-disjunctive logic programs. Our method is based on the elementary program transformations studied by BRASS and Dnr [6, 7]. However, their "residual program" can grow to exponential size, whereas for function-free programs our "program remainder" is always polynomial in the size, i.e. the number of tuples, of the extensional database (EDB). As in the SLG-resolution of CHEN and WARREN [11, 12, 13], we do not only delay negative but also positive literals if they depend on delayed negative literals. When disregarding goal-directedness, which needs additional concepts, our approach can be seen as a simplified bottom-up version of SLG-resolution applicable to range-restricted Datalog programs. Since our approach is also closely related to the alternating fixpoint procedure [27, 28], it can possibly serve as a basis for an integration of the resolution-based, fixpoint-based, and transformation-based evaluation methods.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Properties of maximal cliques of a pair-wise compatibility graph for three nonmonotonic reasoning systems

Properties of maximal cliques of a pair-wise compatibility g...

引用

2nd international workshop on Answer Set programming Advances in Theory and Implementation, ASP 2003

作者： Mercer, R.E. Risch, V. Cognitive Engineering Laboratory Department of Computer Science University of Western Ontario London ON N6A 5B7 Canada InCA Team LSIS - UMR CNRS 6168 Domaine Universitaire de Saint-Jérôme avenue Escadrille Normandie Niemen 13397 Marseille cédex 20 France

In this paper we define the notion of a compatibility relation so as to have a common framework for three nonmonotonic reasoning systems: normal logic programming, extended logic programming, and a restricted form of default logic. We show some properties of the maximal cliques of the pair-wise compatibility graph givn by the relation between the rules of the various reasoning systems. Properties that these maximal cliques possess are presented. A procedure to compute stable models (resp. answer sets, extensions) by enumerating maximal cliques with intelligent pruning is sketched.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

AN INFERENCE SYSTEM FOR HORN CLAUSE logic WITH EQUALITY - A FOUndATION FOR COndITIONAL E-UNIFICATION And FOR logic programming IN THE PRESENCE OF EQUALITY 2nd

引用

2nd international workshop ON COndITIONAL And TYPED REWRITING SYSTEMS

作者： SNYDER, W LYNCH, C Boston University Department of Computer Science 111 Cummington St. Boston 02215 MA United States

ISBN: (纸本)3540543171

In this extended abstract of a full paper we present an inference system for Horn clause logic with equality which is complete not only refutationally but also with respect to the answer substitutions returned, without using functional reflexivity axioms or paramodulating at variable positions. It is goal directed in the sense that—as in SLD resolution—inference rules are only applied to the goal statement. We present the inference system (which subsumes those used for SLD-resolution and for general E-unification), prove its soundness and completeness, and then suggest how this approach forms the appropriate foundation for the study of inference systems (like logic programming interpreters) which return answer substitutions. © Springer-Verlag Berlin Heidelberg 1991.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Model checking linear logic specifications

Model checking linear logic specifications

引用

2nd international workshop on Verification and Computational logic (VCL 2001)

作者： Bozzano, M DelZanno, G Martelli, M IRST ITC I-38050 Trento Italy Univ Genoa Dipartimento Informat & Sci Informaz I-16146 Genoa Italy

关键词： linear logic fixpoint semantics bottom-up evaluation

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：