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

Abstract Diagnosis for tccp using a Linear Temporal logic

theory and practice of logic programming 2014年第4-5期14卷 787-801页

作者： Comini, Marco Titolo, Laura Villanueva, Alicia Univ Udine DIMI I-33100 Udine Italy Univ Politecn Valencia DSIC Valencia Spain

Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge. In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpretation techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.

关键词： concurrent constraint paradigm linear temporal logic abstract diagnosis decision procedures program verification

来源：评论

学校读者我要写书评

暂无评论

Dynamic Consistency Checking in Goal-Directed Answer Set programming

Dynamic Consistency Checking in Goal-Directed Answer Set Pro...

引用

30th International Conference on logic programming

作者： Marple, Kyle Gupta, Gopal Univ Texas Dallas Dept Comp Sci Richardson TX 75083 USA

In answer set programming, inconsistencies arise when the constraints placed on a program become unsatisfiable. In this paper, we introduce a technique for dynamic consistency checking for our goal-directed method for computing answer sets, under which only those constraints deemed relevant to the partial answer set are tested, allowing inconsistent knowledgebases to be successfully queried. However, the algorithm guarantees that, if a program has at least one consistent answer set, any partial answer set returned will be a subset of some consistent answer set.

关键词： dynamic consistency checking answer set programming goal-directed consistent query answering

来源：评论

学校读者我要写书评

暂无评论

Using Tabled logic programming to Solve the Petrobras Planning Problem

引用

theory and practice of logic programming 2014年第4-5期14卷 697-710页

作者： Bartak, Roman Zhou, Neng-Fa Charles Univ Prague Fac Math & Phys Prague Czech Republic CUNY Brooklyn Coll New York NY USA

Tabling has been used for some time to improve efficiency of Prolog programs by memorizing answered queries. The same idea can be naturally used to memorize visited states during search for planning. In this paper we present a planner developed in the Picat language to solve the Petrobras planning problem. Picat is a novel Prolog-like language that provides pattern matching, deterministic and non-deterministic rules, and tabling as its core modelling and solving features. We demonstrate these capabilities using the Petrobras problem, where the goal is to plan transport of cargo items from ports to platforms using vessels with limited capacity. Monte Carlo Tree Search has been so far the best technique to tackle this problem and we will show that by using tabling we can achieve much better runtime efficiency and better plan quality.

关键词： tabling resource-bounded search symmetry breaking planning logistics

来源：评论

学校读者我要写书评

暂无评论

Rewriting and narrowing for constructor systems with call-time choice semantics

引用

theory and practice of logic programming 2014年第2期14卷 165-213页

作者： Lopez-Fraguas, Francisco J. Martin-Martin, Enrique Rodriguez-Hortala, Juan Sanchez-Hernandez, Jaime Univ Complutense Madrid Dept Sistemas Informat & Comp Madrid Spain

Non-confluent and non-terminating constructor-based term rewriting systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kinds of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non-trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper, we develop thoroughly the theory for the first-order version of let-rewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide a notion of let-narrowing, which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to let-rewriting. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing, providing in particular soundness and completeness of let-rewriting with respect to term rewriting for a class of programs which are deterministic in a semantic sense.

关键词： term rewriting systems constructor-based rewriting logic narrowing non-determinism call-time choice semantics sharing local bindings

来源：评论

学校读者我要写书评

暂无评论

Singular and plural functions for functional logic programming

引用

theory and practice of logic programming 2014年第1期14卷 65-116页

作者： Riesco, Adrian Rodriguez-Hortala, Juan Univ Complutense Madrid Fac Informat Dept Sistemas Informat & Computac Madrid 28040 Spain

Modern functional logic programming (FLP) languages use non-terminating and non-confluent constructor systems (CSs) as programs in order to define non-strict and non-deterministic functions. Two semantic alternatives have been usually considered for parameter passing with this kind of functions: call-time choice and run-time choice. While the former is the standard choice of modern FLP languages, the latter lacks some basic properties - mainly compositionality - that have prevented its use in practical FLP systems. Traditionally it has been considered that call-time choice induces a singular denotational semantics, while run-time choice induces a plural semantics. We have discovered that this latter identification is wrong when pattern matching is involved, and thus in this paper we propose two novel compositional plural semantics for CSs that are different from run-time choice. We investigate the basic properties of our plural semantics - compositionality, polarity, and monotonicity for substitutions, and a restricted form of the bubbling property for CSs - and the relation between them and to previous proposals, concluding that these semantics form a hierarchy in the sense of set inclusion of the set of values computed by them. Besides, we have identified a class of programs characterized by a simple syntactic criterion for which the proposed plural semantics behave the same, and a program transformation that can be used to simulate one of the proposed plural semantics by term rewriting. At the practical level, we study how to use the new expressive capabilities of these semantics for improving the declarative flavor of programs. As call-time choice is the standard semantics for FLP, it still remains the best option for many common programming patterns. Therefore, we propose a language that combines call-time choice and our plural semantics, which we have implemented in the Maude system. The resulting interpreter is then employed to develop and test several signif

关键词： non-deterministic functions semantics program transformation term rewriting Maude

来源：评论

学校读者我要写书评

暂无评论

Resource Usage Analysis of logic Programs via Abstract Interpretation Using Sized Types

引用

theory and practice of logic programming 2014年第4-5期14卷 739-754页

作者： Serrano, A. Lopez-Garcia, P. Hermenegildo, M. V. Univ Utrecht Dept Informat & Comp Sci NL-3508 TC Utrecht Netherlands IMDEA Software Inst Madrid Spain CSIC Spanish Council Sci Res Madrid Spain Tech Univ Madrid UPM Madrid Spain

We present a novel general resource analysis for logic programs based on sized types. Sized types are representations that incorporate structural (shape) information and allow expressing both lower and upper bounds on the size of a set of terms and their subterms at any position and depth. They also allow relating the sizes of terms and subterms occurring at different argument positions in logic predicates. Using these sized types, the resource analysis can infer both lower and upper bounds on the resources used by all the procedures in a program as functions on input term (and subterm) sizes, overcoming limitations of existing resource analyses and enhancing their precision. Our new resource analysis has been developed within the abstract interpretation framework, as an extension of the sized types abstract domain, and has been integrated into the Ciao preprocessor, CiaoPP. The abstract domain operations are integrated with the setting up and solving of recurrence equations for inferring both size and resource usage functions. We show that the analysis is an improvement over the previous resource analysis present in CiaoPP and compares well in power to state of the art systems.

关键词： analysis programme Upper bound Formal logic logic programming

来源：评论

学校读者我要写书评

暂无评论

A Module System for Domain-Specific Languages

引用

theory and practice of logic programming 2014年第4-5期14卷 771-785页

作者： Jackson, Ethan K. Microsoft Res Res Software Engn RiSE Redmond WA 98052 USA

Domain-specific languages (DSLs) are routinely created to simplify difficult or specialized programming tasks. They expose useful abstractions and design patterns in the form of language constructs, provide static semantics to eagerly detect misuse of these constructs, and dynamic semantics to completely define how language constructs interact. However, implementing and composing DSLs is a non-trivial task, and there is a lack of tools and techniques. We address this problem by presenting a complete module system over LP for DSL construction, reuse, and composition. LP is already useful for DSL design, because it supports executable language specifications using notations familiar to language designers. We extend LP with a module system that is simple (with a few concepts), succinct (for key DSL specification scenarios), and composable (on the level of languages, compilers, and programs). These design choices reflect our use of LP for industrial DSL design. Our module system has been implemented in the formula language, and was used to build key Windows 8 device drivers via DSLs. Though we present our module system as it actually appears in our formula language, our emphasis is on concepts adaptable to other LP languages.

关键词： module systems domain-specific languages logic programming

来源：评论

学校读者我要写书评

暂无评论

Pengines: Web logic programming Made Easy

Pengines: Web Logic Programming Made Easy

引用

30th International Conference on logic programming

作者： Lager, Torbjorn Wielemaker, Jan Gothenburg Univ S-41124 Gothenburg Sweden Vrije Univ Amsterdam Amsterdam Netherlands

When developing a (web) interface for a deductive database, functionality required by the client is provided by means of HTTP handlers that wrap the logical data access predicates. These handlers are responsible for converting between client and server data representations and typically include options for paginating results. Designing the web accessible API is difficult because it is hard to predict the exact requirements of clients. Pengines changes this picture. The client provides a Prolog program that selects the required data by accessing the logical API of the server. The pengine infrastructure provides general mechanisms for converting Prolog data and handling Prolog non-determinism. The Pengines library is small (2000 lines Prolog, 150 lines JavaScript). It greatly simplifies defining an AJAX based client for a Prolog program and provides non-deterministic RPC between Prolog processes as well as interaction with Prolog engines similar to Paul Tarau's engines. Pengines are available as a standard package for SWI-Prolog 7.(1)

关键词： web programming query languages agent programming distributed programming

来源：评论

学校读者我要写书评

暂无评论

Automatically checking commitment protocols in ProVerif without false attacks

引用

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2015年 9036卷 137-155页

作者： Chothia, Tom Smyth, Ben Staite, Chris School of Computer Science University of Birmingham United Kingdom Mathematical and Algorithmic Sciences Lab France Research Center Huawei Technologies Co. Ltd France

ISBN: (纸本)9783662466650

ProVerif over-approximates the attacker’s power to enable verification of processes under replication. Unfortunately, this results in ProVerif finding false attacks. This problem is particularly common in protocols whereby a participant commits to a particular value and later reveals their value. We introduce a method to reduce false attacks when analysing secrecy. First, we show how inserting phases into nonreplicated processes enables a more accurate translation to Horn clauses which avoids some false attacks. Secondly, we generalise our methodology to processes under replication. Finally, we demonstrate the applicability of our technique by analysing BlueTooth Simple Pairing. Moreover, we propose a simplification of this protocol that achieves the same security goal. © Springer-Verlag Berlin Heidelberg 2015.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

A Proof Theoretic Study of Soft Concurrent Constraint programming

A Proof Theoretic Study of Soft Concurrent Constraint Progra...

引用

30th International Conference on logic programming

作者： Pimentel, Elaine Olarte, Carlos Nigam, Vivek Univ Fed Rio Grande do Norte BR-59072970 Natal RN Brazil Pontificia Univ Javeriana Cali Javeriana Colombia Univ Fed Paraiba BR-58059900 Joao Pessoa Paraiba Brazil

Concurrent Constraint programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic -ILL- and processes can be interpreted as formulas in ILL. Constraints as ILL formulas fail to represent accurately situations where "preferences" (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical meaning to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings. This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systems.

关键词： Concurrent Constraint programming Linear logic Soft Constraints

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：