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

Operational semantics of Framed Tempura

JOURNAL OF logic AND ALGEBRAIC programming 2008年第1期78卷 22-51页

作者： Yang, Xiaoxiao Duan, Zhenhua Xidian Univ Inst Comp Theory & Technol Xian Shaanxi Peoples R China

This paper investigates the operational semantics of temporal logic programs. To this end, a temporal logic programming language called Framed Tempura is employed. The evaluation rules for both the arithmetic and Boolean expressions are defined. The semantic equivalence rules for the reduction of a program within a state is formalized. Furthermore, the transition rules within a state and transition rules over an interval between configurations are also specified. Moreover, some examples are given to illustrate how these rules work. Thus, the executable behavior of framed programs can be captured in an operational way. In addition, the consistency between the operational semantics and the minimal model semantics based on model theory is proved in detail. (c) 2008 Elsevier Inc. All rights reserved.

关键词： temporal logic programming Non-monotonicity Minimal model Operational semantics Consistency

来源：评论

学校读者我要写书评

暂无评论

A Framed temporal logic programming Language

引用

Journal of Computer Science & Technology 2004年第3期19卷 341-351页

作者： Zhen-HuaDuan MaciejKoutny UniversityofNewcastleuponTyne NewcastleuponTyneNE17RUU.K. XidianUniversity Xi＇an710071P.R.China／／LaboratoryofComputerScienceISCASBeijing100080P.R.China

We discuss the projection temporal logic (PTL), based on a primitiveprojection operator, prj. A framing technique is also presented, using which a synchronizationoperator, await, is defined within the underlying logic. A framed temporal logic programminglanguage (FTLL) is presented. To illustrate how to use both the language and framing technique, someexamples are given.

关键词： temporal logic temporal logic programming frame projection concurrency

来源：评论

学校读者我要写书评

暂无评论

A proof procedure for temporal logic programming

引用

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE 2004年第2期15卷 417-443页

作者： Gergatsoulis, M Nomikos, C Ionian Univ Dept Arch & Lib Sci Corfu 49100 Greece Univ Ioannina Dept Comp Sci GR-45110 Ioannina Greece

In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs.

关键词： temporal logic programming proof procedures branching-time theorem proving

来源：评论

学校读者我要写书评

暂无评论

An interpreter for Framed Tempura and its application

An interpreter for Framed Tempura and its application

引用

1st IEEE/IFIP International Symposium on Theoretical Aspects of Softwave Engineering

作者： Ma, Yongtao Duan, Zhenhua Wang, Xiaobing Yang, Xiaoxiao Xidian Univ Inst Comp Theory & Technol Xian 710071 Peoples R China

ISBN: (纸本)9780769528564

This paper discusses the implementation mechanism and its application of an interpreter for a framed temporal logic programming language called Framed Tempura. Firstly, the basic approach based on the normal form is presented. Then, the structure of the interpreter is illustrated and each of its modules is explained. The workflow of the reduction of programs is given in detail. In particular, the implementation approaches of several important new constructs including frame, await, projection, pointer are presented. As an application, the interpreter is used as a simulator of service models of OWL-S for the Web service composition.

关键词： framing projection normal form temporal logic programming

来源：评论

学校读者我要写书评

暂无评论

temporal stratification tests for linear and branching-time deductive databases

引用

THEORETICAL COMPUTER SCIENCE 2005年第2-3期342卷 382-415页

作者： Nomikos, C Rondogiannis, P Gergatsoulis, M Univ Ioannina Dept Comp Sci GR-45110 Ioannina Greece Ionian Univ Dept Arch & Lib Sci Corfu 49100 Greece

We consider the problem of extending temporal deductive databases with stratified negation. We argue that the classical stratification test for deductive databases is too restrictive when one shifts attention to the temporal case. Moreover, as we demonstrate, the (more general) local stratification approach is impractical: detecting whether a temporal deductive database is locally stratified is shown to be co-NP hard (even if one restricts attention to programs that only use one predicate symbol and two constants). For these reasons we define temporal stratification, an intermediate notion between stratification and local stratification. We demonstrate that for the temporal deductive databases we consider, temporal stratification coincides with local stratification in certain important cases in which the latter is polynomial-time decidable. We then develop two algorithms for detecting temporal stratification. The first algorithm applies to linear-time temporal deductive databases and it is efficient and more general than existing approaches;however, the algorithm sacrifices completeness for efficiency since it does not cover the whole class of temporally stratified programs. The second algorithm applies to branching-time temporal deductive databases (which include as a special case the linear-time ones). This algorithm is more expensive from a computational point of view, but it covers the whole class of temporally stratified programs. We discuss the relative merits of the two algorithms and compare them with other existing approaches. (c) 2005 Elsevier B.V. All rights reserved.

关键词： temporal deductive databases temporal logic programming stratified negation

来源：评论

学校读者我要写书评

暂无评论

Semantics of framed temporal logic programs

Semantics of framed temporal logic programs

引用

21st International Conference on logic programming

作者： Duan, ZH Yang, XX Koutny, M Xidian Univ Sch Engn & Comp Sci Xian 710071 Peoples R China Univ Newcastle Dept Comp Sci Newcastle Upon Tyne NE1 7RU Tyne & Wear England

ISBN: (纸本)354029208X

This paper investigates semantics of framed temporal logic programs. To this end, a projection temporal logic and its executable subset are presented. Based on this language, a framing technique is introduced. The semantics of a non-framed program is well interpreted by the canonical model. However, since introducing a framing operator destroys monotonicity, a canonical model may no longer capture the intended meaning of a program. Hence, a minimal model theory is developed. Within this model, negation by default is used to manipulate frame operator. Further, the temporal semantics of framed programs is captured by means of the minimal models. The existence of a minimal model for a given framed program is also proved. An example is given to illustrate how the semantics of framed programs can be captured.

关键词： temporal logic programming framing minimal model monotonicity semantics

来源：评论

学校读者我要写书评

暂无评论

Stratified negation in temporal logic programming and the cycle-sum test

引用

THEORETICAL COMPUTER SCIENCE 2001年第1-2期254卷 663-676页

作者： Rondogiannis, P Univ Athens Dept Informat Athens 15784 Greece

We consider stratified negation in temporal logic programming. We demonstrate that the cycle-sum test (which was initially proposed for detecting deadlocks in the context of temporal functional programming) can also be used as a syntactic stratification test for temporal logic programming. Therefore, on the one hand we exhibit a class of temporal logic programs with negation which have a well-defined semantics, and on the other hand we provide further evidence that the cycle-sum test is a fundamental one in the area of temporal programming. (C) 2001 Elsevier Science B.V. All rights reserved.

关键词： temporal logic programming negation stratification cycle-sum test

来源：评论

学校读者我要写书评

暂无评论

temporal disjunctive logic programming

引用

NEW GENERATION COMPUTING 2001年第1期19卷 87-100页

作者： Gergatsoulis, M Rondogiannis, P Panayiotopoulos, T NCSR Demokritos Inst Informat & Telecommun GR-15310 Athens Greece Univ Ioannina Dept Comp Sci GR-45110 Ioannina Greece Univ Piraeus Dept Informat Piraeus 18534 Greece

In this paper we introduce the logic programming language Disjunctive Chronology which combines the programming paradigms of temporal and disjunctive logic programming. Disjunctive Chronolog is capable of ex pressing dynamic behaviour as well as uncertainty, two notions that are very common in a variety of real systems. We present the minimal temporal model semantics and the fixpoint semantics for the new programming language and demonstrate their equivalence. We also show how proof procedures developed for disjunctive logic programs can be easily extended to apply to Disjunctive Chronolog programs.

关键词： temporal logic programming disjunctive logic programming semantics proof procedures

来源：评论

学校读者我要写书评

暂无评论

The branching-time transformation technique for chain datalog programs

引用

JOURNAL OF INTELLIGENT INFORMATION SYSTEMS 2001年第1期17卷 71-94页

作者： Rondogiannis, P Gergatsoulis, M Univ Athens Dept Informat & Telecommun Athens 15784 Greece Natl Ctr Sci Res Demokritos Inst Informat & Telecommun Athens 15310 Greece

The branching-time transformation technique has proven to be an efficient approach for implementing functional programming languages. In this paper we demonstrate that such a technique can also be defined for logic programming languages. More specifically, we first introduce Branching Datalog, a language that can be considered as the basis for branching-temporal deductive databases. We then present a transformation algorithm from Chain Datalog programs to the class of unary Branching Datalog programs with at most one IDB atom in the body of each clause. In this way, we obtain a novel implementation approach for Chain Datalog, shedding at the same time new light on the power of branching-time logic programming.

关键词： deductive databases chain programs program transformation temporal logic programming branching time

来源：评论

学校读者我要写书评

暂无评论

A parallel execution model for Chronolog

引用

COMPUTER SYSTEMS SCIENCE AND ENGINEERING 2001年第4期16卷 215-228页

作者： Liu, CC Orgun, MA Zhang, K Def Sci & Technol Org Div Informat Technol Salisbury SA 5108 Australia Macquarie Univ Dept Comp Sydney NSW 2109 Australia Univ Texas Dept Comp Sci Richardson TX 75083 USA

Chronolog(z) is a logic programming language based on a linear-time temporal logic with unbounded past and future. By adding 'choice predicates' to Chronolog(z), it is possible to obtain exactly one answer to a given goal when we want to model dataflow, style of stream-oriented computations. In this paper, we propose a parallel execution model for Chronclog(z) that supports AND- and OR-parallelism in the highly distributed dataflow environment. In order to exploit the inherent context-paralellism that exist in temporal logic programs, we introduce the concept of parallel context-processes into the model. We also introduce an intermediate virtual machine (CVM), which is granulated to exploit the argument parallelism through temporal unification. The details of the CVM instruction set are given. The use of a warehouse facility as an associate memory to store the results of previous computations is an important feature of this model. This paper discusses the structure of the warehouse, its role and use in parallel execution of Chronolog programs. We in particular outline an algorithm to manage the warehouse.

关键词： temporal logic programming operational semantics context-parallelism warehouse dataflow computation

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：