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

Semantic foundations for generalized rewrite theories

THEORETICAL COMPUTER SCIENCE 2006年第1-3期360卷 386-414页

作者： Bruni, Roberto Meseguer, Jose Univ Pisa Dipartimento Informat I-56127 Pisa Italy Univ Illinois CS Dept Urbana IL 61801 USA

Rewriting logic (RL) is a logic of actions whose models are concurrent systems. Rewrite theories involve the specification of equational theories of data and state structures together with a set of rewrite rules that model the dynamics of concurrent systems. Since its introduction, more than one decade ago, RL has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. These extensions may develop along several dimensions, like the choice of the underlying equational logic, the kind of side conditions allowed in rewrite rules and operational concerns for the execution of certain rewrites. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites;moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories. Our results provide a mathematical semantics for Maude, and a foundation for formal reasoning about Maude specifications. (C) 2006 Elsevier B.V. All rights reserved.

关键词： conditional rewriting logic membership equational logic contextual rewrites semantics

来源：评论

学校读者我要写书评

暂无评论

Effective prover for minimal inconsistency logic

Effective prover for minimal inconsistency logic

引用

Conference on Artificial Intelligence in theory and practice held at the 19th World Computer Congress

作者： Neto, Adolfo Gustavo Serra Seca Finger, Marcelo Univ Sao Paulo Dept Comp Sci Inst Math & Stat Sao Paulo Brazil

ISBN: (纸本)0387346546

In this paper we present an effective prover for mbC, a minimal inconsistency logic. The mbC logic is a paraconsistent logic of the family of logics of formal inconsistency. Paraconsistent logics have several philosophical motivations as well as many applications in Artificial Intelligence such as in belief revision, inconsistent knowledge reasoning, and logic programming. We have implemented the KEMS prover for mbC, a theorem prover based on the KE tableau method for mbC. We show here that the proof system on which this prover is based is sound, complete and analytic. To evaluate the KEMS prover for mbC, we devised four families of mbC-valid formulas and we present here the first benchmark results using these families.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Set unification

引用

theory and practice of logic programming 2006年第0期6卷 645-701页

作者： Dovier, Agostino Pontelli, Enrico Rossi, Gianfranco Univ Udine Dipartimento Matemat & Informat I-33100 Udine Italy New Mexico State Univ Dept Comp Sci Las Cruces NM 88003 USA Univ Parma Dipartimento Matemat I-43100 Parma Italy

The unification problem in algebras capable of describing sets has been tackled, directly or indirectly, by many researchers and it finds important applications in various research areas, e.g. deductive databases, theorem proving, static analysis, rapid software prototyping. The various solutions proposed are spread across a large literature. In this paper we provide a uniform presentation of unification of sets, formalizing it at the level of set theory. We address the problem of deciding existence of solutions at an abstract level. This provides also the ability to classify different types of set unification problems. Unification algorithms are uniformly proposed to solve the unification problem in each of such classes. The algorithms presented are partly drawn from the literature - and properly revisited and analyzed - and partly novel proposals. In particular, we present a new goal-driven algorithm for general ACI l unification and a new simpler algorithm for general (Ab)(Cl) unification.

关键词： unification theory set theory ACI 1 unification

来源：评论

学校读者我要写书评

暂无评论

Innovations in computational type theory using Nuprl

引用

Journal of Applied logic 2006年第4期4卷 428-469页

作者： Allen, S.F. Bickford, M. Constable, R.L. Eaton, R. Kreitz, C. Lorigo, L. Moran, E. Department of Computer Science Cornell University Ithaca NY 14853-7501 United States

For twenty years the Nuprl ("new pearl") system has been used to develop software systems and formal theories of computational mathematics. It has also been used to explore and implement computational type theory (CTT)-a formal theory of computation closely related to Martin-Löf's intuitionistic type theory (ITT) and to the calculus of inductive constructions (CIC) implemented in the Coq prover. This article focuses on the theory and practice underpinning our use of Nuprl for much of the last decade. We discuss innovative elements of type theory, including new type constructors such as unions and dependent intersections, our theory of classes, and our theory of event structures. We also discuss the innovative architecture of Nuprl as a distributed system and as a transactional database of formal mathematics using the notion of abstract object identifiers. The database has led to an independent project called the Formal Digital Library, FDL, now used as a repository for Nuprl results as well as selected results from HOL, MetaPRL, and PVS. We discuss Howe's set theoretic semantics that is used to relate such disparate theories and systems as those represented by these provers. © 2005 Elsevier B.V. All rights reserved.

关键词： Computation theory

来源：评论

学校读者我要写书评

暂无评论

Executable structural operational semantics in Maude

引用

JOURNAL OF logic AND ALGEBRAIC programming 2006年第1-2期67卷 226-293页

作者： Verdejo, A Martí-Oliet, N Univ Complutense Madrid Dept Sistemas Informat & Programac E-28040 Madrid Spain

This paper describes in detail how to bridge the gap between theory and practice when implementing in Maude structural operational semantics described in rewriting logic, where transitions become rewrites and inference rules become conditional rewrite rules with rewrites in the conditions, as made possible by the new features in Maude 2. We validate this technique using it in several case studies: a functional language Fpl (evaluation and computation semantics), an imperative language WhileL (evaluation and computation semantics), Kahn's functional language Mini-ML (evaluation or natural semantics), Milner's CCS (with strong and weak transitions), and Full LOTOS (including ACT ONE data type specifications). In addition, on top of CCS we develop an implementation of the Hennessy-Milner modal logic for describing local capabilities of processes, and for LOTOS we build an entire tool where Full LOTOS specifications can be entered and executed (without user knowledge of the underlying implementation of the semantics). We also compare this method based on transitions as rewrites with another one based on transitions as judgements. (c) 2005 Elsevier Inc. All rights reserved.

关键词： rewriting logic Maude 2 executability structural operational semantics metalanguage CCS LOTOS ACT ONE

来源：评论

学校读者我要写书评

暂无评论

Equivalence-checking on infinite-state systems: Techniques and results

Equivalence-checking on infinite-state systems: Techniques a...

引用

作者： Kučera, Antonín Jančar, Petr Faculty of Informatics Masaryk University Botanická 68a CZ-602 00 Brno Czech Republic Dept. of Computer Science FEI Technical University of Ostrava 17. listopadu 15 CZ-708 33 Ostrava Czech Republic

The paper presents a selection of recently developed and/or used techniques for equivalence-checking on infinite-state systems, and an up-to-date overview of existing results (as of September 2004). © 2006 Cambri... 详细信息

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Computing minimal models, stable models and answer sets

引用

theory and practice of logic programming 2006年第0期6卷 395-449页

作者： Lonc, Zbigniew Truszczynski, Miroslaw Warsaw Univ Technol Fac Math & Informat Sci PL-00661 Warsaw Poland Univ Kentucky Dept Comp Sci Lexington KY 40506 USA

We propose and Study algorithms to compute minimal models. stable models and answer sets of t-CNF theories, and normal and disjunctive t-programs. We are especially interested in algorithms with non-trivial worst-case performance bounds. The bulk of the paper is concerned with the classes of 2- and 3-CNF theories, and normal and disjunctive 2- and 3-programs, for which we obtain significantly stronger results than those implied by our general considerations. We show that one can find all minimal models of 2-CNF theories and all answer sets of disjunctive 2-programs in time O(ml.4422.."). Our main results concern computing stable models of normal 3-programs, minimal models of 3-CNF theories and answer sets of disjunctive 3-programs. We design algorithms that run in time O(ml.6701.."), in the case of the first problem, and in time O(mn(2)2.2782..(n)), in the case of the latter two. All these bounds improve by exponential factors the best algorithms known previously. We also obtain closely related upper bounds on the number of minimal models, stable models and answer sets a t-CNF theory, a normal t-program or a disjunctive t-program may have.

关键词： stable models answer sets minimal models disjunctive logic programs

来源：评论

学校读者我要写书评

暂无评论

Detecting and repairing anomalous evolutions in noisy environments: logic programming formalization and complexity results

Detecting and repairing anomalous evolutions in noisy enviro...

引用

Conference on Artificial Intelligence in theory and practice held at the 19th World Computer Congress

作者： Angiulli, Fabrizio Greco, Gianluigi Palopoli, Luigi ICAR CNR Via P Bucci 41C I-87030 Arcavacata Di Rende Italy Univ Calabria Dept Math I-87030 Arcavacata Di Rende Italy Univ Calabria DEIS I-87030 Commenda Di Rende Italy

ISBN: (纸本)0387346546

In systems where agents are required to interact with a partially known and dynamic world, sensors can be used to obtain further knowledge about the environment. However, sensors may be unreliable, that is, they may deliver wrong information (due, e.g., to hardware or software malfunctioning) and, consequently, they may cause agents to take wrong decisions, which is a scenario that should be avoided. The paper considers the problem of reasoning in noisy environments in a setting where no (either certain or probabilistic) data is available in advance about the reliability of sensors. Therefore, assuming that each agent is equipped with a background theory (in our setting, an extended logic program) encoding its general knowledge about the world, we define a concept of detecting an anomaly perceived in sensor data and the related concept of agent recovering to a coherent status of information. In this context, the complexities of various anomaly detection and anomaly recovery problems are studied.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Automatic verification of timed concurrent constraint programs

引用

theory and practice of logic programming 2006年第3期6卷 265-300页

作者： Falaschi, Moreno Villanueva, Alicia Univ Udine Dipartimento Matemat & Informat I-33100 Udine Italy Univ Politecn Valencia Dept Sistemas Informat & Computac E-46022 Valencia Spain

The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. Constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp.

关键词： automatic verification reactive systems timed concurrent constraint programming model checking

来源：评论

学校读者我要写书评

暂无评论

A child's story to illustrate automated reasoning systems using opportunity and history

A child's story to illustrate automated reasoning systems us...

引用

IEEE InternationalConference on Intelligence and Security Informatics (ISI 2006)

作者： Jones, James D. Joshi, Hemant Topaloglu, Umit Nelson, Eric Angelo State Univ Dept Comp Sci San Angelo TX 76909 USA Univ Arkansas Dept Comp Sci Little Rock AR 72204 USA

ISBN: (纸本)3540344780

The primary author has performed previous work to create generalized, high-level reasoning software to identify deception on the basis of actions. The work here is to apply that software architecture to an entirely different domain. The original domain was an espionage scenario, and detected deception when communications were in conflict. This present domain is reasoning about a child's story to determine who is lying about the theft of some objects. Applying the previous work to a different domain is an attempt to demonstrate the generality of the architecture. It is also an attempt to further generalize the software, and to formalize additional "common sense" strategies in the detection of deception. This software detects deception on the basis of actions. This is in sharp contrast with present approaches that detect deception based on physiological factors, as well as on verbal and non-verbal cues. Our approach models agents and their actions in a logic programming framework using a theory of agents, a theory of actions, and a theory of reasoning with respect to time. As a test case, a children's mystery is analyzed and implemented. The goal of the story is to identify who stole some items. The software correctly reasons about who the potential suspects are, and ultimately, correctly identifies the chief culprit. Further, it can correctly introspect with regard to previously held beliefs. The program we have developed is able to mimic the thought processes and conclusions of a police investigation. To demonstrate our approach, we have created a scenario loosely based upon a child's book. The basic idea of the story is that a bat is missing, and the goal is to identify who stole the bat. The flow of the story is as follows. There is a practice at the beginning of the story. A particular baseball bat is missing, and presumed stolen. Everyone present at that practice is a suspect in the theft of the bat. There is a subsequent practice at which a glove becomes missin

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：