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

BACKTRACKING WITHOUT TRAILING IN CLP(R(LIN))

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 1995年第4期17卷 635-671页

作者： VANHENTENRYCK, P RAMACHANDRAN, V Department of Computer Science Brown University Box 1910 Providence RI

Existing CLP languages support backtracking by generalizing traditional Prolog implementations: modifications to the constraint system are trailed and restored an backtracking. Although simple and efficient, trailing may be very demanding in memory space, since the constraint system may potentially be saved at each choice point. This article proposes a new implementation scheme for backtracking in CLP languages over linear (rational or real) arithmetic. The new scheme, called semantic backtracking, does not use trailing but rather exploits the semantics of the constraints to undo the effect, of newly added constraints. Semantic backtracking reduces the space complexity compared to implementations based on trailing by making it essentially independent of the number of choice points. In addition, semantic backtracking introduces negligible space and time overhead on deterministic programs. The price for this improvement is an increase in backtracking time. although constraint-solving time may actually decrease. The scheme has been implemented as part of a complete CLP system CLP(R(Lin)) and compared analytically and experimentally with optimized trailing implementations. Experimental results on small and real-life problems indicate that semantic backtracking produces significant reduction in memory space, while keeping the time overhead reasonably small.

关键词： BACKTRACKING constraint logic programming TRAILING

来源：评论

学校读者我要写书评

暂无评论

logic, modeling, and programming

引用

ANNALS OF OPERATIONS RESEARCH 1997年第s期71卷 335-372页

作者： McAloon, K Tretkoff, C CUNY GRAD CTR LOG BASED SYST LAB BROOKLYN NY 11210 USA CUNY BROOKLYN COLL BROOKLYN NY 11210 USA

In this paper we discuss the integration of logic, modeling, and programming in order to solve problems in operations research, artificial intelligence, and decision support programming in general. Our goals are to integrate modeling into the larger programming scheme of things and, conversely, to inject programming into modeling. To accomplish these ends, we use the language 2LP, which is based on ideas from constraint logic programming. This leads to a technologically open way to handle problems, one which supports flexible treatment of goal programming, hybrid MIP/local search algorithms, libraries for distributed processing, disjunctive programming, etc. An additional advantage of the programming language approach is that problem solving and model management can be abetted by software engineering techniques. In this paper, by means of variations on a single example, we will illustrate how the logical connectives and linear constraints interact in the solution of a linear program, a goal program, a disjunctive program, a branch and bound search, a randomized shuffle algorithm, and a parallel solution to a model with stochastic data.

关键词： Commodity auction market constraint logic programming electronic market hierarchical constraint reasoning stable matching.

来源：评论

学校读者我要写书评

暂无评论

Combining Type Checking and Set constraint Solving to Improve Automated Software Verification

引用

THEORY AND PRACTICE OF logic programming 2024年第5期24卷 1011-1030页

作者： Cristia, Maximiliano Rossi, Gianfranco Univ Nacl Rosario Rosario Argentina CIFASIS CONICET UNR Rosario Argentina Univ Parma Parma Italy

This technical note shows how we have combined prescriptive type checking and constraint solving to increase automation during software verification. We do so by defining a type system and implementing a typechecker for {log} (read 'setlog'), a constraint logic programming language and satisfiability solver based on set theory. The constraint solver is proved to be safe w.r.t. the type system. Two industrial-strength case studies are presented where this combination is used with very good results.

关键词： {log} set theory constraint logic programming type system typechecker

来源：评论

学校读者我要写书评

暂无评论

A logical model for relational abstract domains

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 1998年第5期20卷 1067-1109页

作者： Giacobazzi, R Scozzari, F Univ Pisa Dipartimento Informat I-56125 Pisa Italy

In this article we introduce the notion of Heyting completion in abstract interpretation. We prove that Heyting completion provides a model for Cousot's reduced cardinal power of abstract domains and that it supplies a logical basis to specify relational domains for program analysis and abstract interpretation. We study the algebraic properties of Heyting completion in relation with other well-known domain transformers, like reduced product and disjunctive completion. This provides a uniform algebraic setting where complex abstract domains can be specified by simple logic formulas, or as solutions of recursive abstract domain equations, involving few basic operations for domain construction, all characterized by a clean logical interpretation. We apply our framework to characterize directionality and condensing in downward closed analysis of (constraint) logic programs.

关键词： languages theory abstract interpretation closure operators condensing analysis constraint logic programming directional types domains Heyting completion intuitionistic logic reduced cardinal power static analysis

来源：评论

学校读者我要写书评

暂无评论

Program verification via iterated specialization

引用

SCIENCE OF COMPUTER programming 2014年第Part2期95卷 149-175页

作者： De Angelis, E. Fioravanti, F. Pettorossi, A. Proietti, M. Univ G DAnnunzio DEC I-65127 Pescara Italy Univ Roma Tor Vergata DICII I-00133 Rome Italy CNR IASI I-00185 Rome Italy

We present a method for verifying properties of imperative programs by using techniques based on the specialization of constraint logic programs (CLP). We consider a class of imperative programs with integer variables and we focus our attention on safety properties, stating that no error configuration can be reached from any initial configuration. We introduce a CLP program I that encodes the interpreter of the language and defines a predicate unsafe equivalent to the negation of the safety property to be verified. Then, we specialize the CLP program I with respect to the given imperative program and the given initial and error configurations, with the objective of deriving a new CLP program I-sp that either contains the fact unsafe (and in this case the imperative program is proved unsafe) or contains no clauses with head unsafe (and in this case the imperative program is proved safe). If Isp enjoys neither of these properties, we iterate the specialization process with the objective of deriving a CLP program where we can prove unsafety or safety. During the various specializations we may apply different strategies for propagating information (either propagating forward from an initial configuration to an error configuration, or propagating backward from an error configuration to an initial configuration) and different operators (such as the widening and the convex hull operators) for generalizing predicate definitions. Each specialization step is guaranteed to terminate, but due to the undecidability of program safety, the iterated specialization process may not terminate. By an experimental evaluation carried out on a significant set of examples taken from the literature, we show that our method improves the precision of program verification with respect to state-of-the-art software model checkers. (C) 2014 Elsevier B.V. All rights reserved.

关键词： Software model checking constraint logic programming Program specialization Program transformation

来源：评论

学校读者我要写书评

暂无评论

MECHANIZING THE VERIFICATION OF REAL-TIME DISCRETE-SYSTEMS

MICROPROCESSING AND MICROPROGRAMMING

引用

MICROPROCESSING AND MICROprogramming 1989年第1-5期27卷 649-656页

作者： OSTROFF, JS YORK UNIV DEPT COMP SCIYORK M3J 1P3ONTARIOCANADA

This paper shows that constraint logic programming languages (such as CLP ()) provide a useful computational logic for modelling, simulating and verifying real-time discrete event processes. The designer's knowledge about discrete processes can be represented in a fashion that stays close to the mathematical definition of the processes, and can be used to semi-automate verification of (possibly infinite state) systems.

关键词： Real-time discrete event processes constraint logic programming automated verification representation of discrete systems

来源：评论

学校读者我要写书评

暂无评论

Incremental analysis of constraint logic programs

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 2000年第2期22卷 187-223页

作者： Hermenegildo, M Puebla, G Marriott, K Stuckey, PJ Univ Politecn Madrid Fac Informat E-28660 Madrid Spain Monash Univ Sch Comp Sci & Software Engn Clayton Vic 3168 Australia Univ Melbourne Dept Comp Sci & Software Engn Parkville Vic 3052 Australia

Global analyzers traditionally read and analyze the entire program at once, in a nonincremental way. However, there are many situations which are not well suited to this simple model and which instead require reanalysis of certain parts of a program which has already been analyzed. In these cases, it appears inefficient to perform the analysis of the program again from scratch, as needs to be done with current systems. We describe how the fixed-point algorithms used in current generic analysis engines for (constraint) logic programming languages can be extended to support incremental analysis. The possible changes to a program are classified into three types: addition, deletion, and arbitrary change. For each one of these, we provide one or more algorithms for identifying the parts of the analysis that must be recomputed and for performing the actual recomputation. The potential benefits and drawbacks of these algorithms are discussed. Finally, we present some experimental results obtained with an implementation of the algorithms in the PLAI generic abstract interpretation framework. The results show significant benefits when using the proposed incremental analysis algorithms.

关键词： languages abstract interpretation constraint logic programming incremental computation static analysis

来源：评论

学校读者我要写书评

暂无评论

Recurrence with affine level mappings is P-time decidable for CLP(R)

引用

THEORY AND PRACTICE OF logic programming 2008年第1期8卷 111-119页

作者： Mesnard, Fred Serebrenik, Alexander Univ Reunion IREMIA St Denis Reunion France Tech Univ Eindhoven Lab Qual Software NL-5600 MB Eindhoven Netherlands

In this paper we introduce a class of constraint logic programs such that their termination can be proved by using affine level mappings. We show that membership to this class is decidable in polynomial time.

关键词： constraint logic programming termination decidability

来源：评论

学校读者我要写书评

暂无评论

Multivalued action languages with constraints in CLP(FD)

引用

THEORY AND PRACTICE OF logic programming 2010年第2期10卷 167-235页

作者： Dovier, Agostino Formisano, Andrea Pontelli, Enrico Univ Udine Dipartimento Matemat & Informat I-33100 Udine Italy Univ Perugia Dipartimento Matemat & Informat I-06123 Perugia Italy New Mexico State Univ Dept Comp Sci Las Cruces NM 88003 USA

Action description languages, such as A and B (Gelfond and Lifschitz, Electronic Transactions on Artificial Intelligence, 1998, vol. 2, pp. 193-210), are expressive instruments introduced for formalizing planning domains and planning problem instances. The paper starts by proposing a methodology to encode an action language (with conditional effects and static causal laws), a slight variation of 0, using constraint logic programming over Finite Domains. The approach is then generalized to raise the use of constraints to the level of the action language itself. A prototype implementation has been developed, and the preliminary results are presented and discussed.

关键词： action description languages knowledge representation planning constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

Integrating on-line performance visualization and real-time system design

引用

REAL-TIME SYSTEMS 2005年第3期30卷 163-185页

作者： Bakic, AM Mutka, MW Vlatacom Ltd Belgrade Serbia Monteneg Michigan State Univ Dept Comp Sci & Engn E Lansing MI 48824 USA

Emerging parallel or distributed, heterogeneous real-time computer systems with many disparate constraints and requirements would benefit from a unifying and comprehensive systems engineering support in the design, testing and deployment phases, which interfaces with a human at a very high level and efficiently handles the system complexity. We present an approach to integration of (1) a compiler- and constraint logic programming-based approach to design and engineering of real-time systems, and (2) an on-line performance analysis and visualization technology. An example distributed real-time system is used to help describe the integrated approach. Details are presented about how the involved technologies are used to help system developers and users achieve better system performance through on-line repair and reconfiguration.

关键词： constraint logic programming extension and glue language real-time design real-time linux real-time visualization

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：