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

Cardinal: A finite sets constraint solver

constraintS 2007年第1期12卷 93-129页

作者： Azevedo, Francisco Univ Nova Lisboa FCTCENTRIA Dept Informat Monte De Caparica Portugal

In this paper we present Cardinal, a general finite sets constraint solver just made publicly available in ECUPSe constraint System, suitable for combinatorial problem solving by exploiting inferences over sets cardinality. In fact, to deal with set variables and set constraints, existing set constraint solvers are not adequate to handle a number of problems, as they do not actively use important information about the cardinality of the sets, a key feature in such problems. Cardinal is formally presented as a set of rewriting rules on a constraint store and we illustrate its efficiency with experimental results. We show the importance of propagating constraints on sets cardinality, by comparing Cardinal with other solvers. Another contribution of this paper is on modelling: we focus essentially on digital circuits problems, for which we present new modelling approaches and prove that sets alone can be used to model these problems in a clean manner and solve them efficiently using Cardinal. Results on a set of diagnostic problems show that Cardinal obtains a speed up of about two orders of magnitude over Conjunto, a previous available set constraint solver, which uses a more limited amount of constraint propagation on cardinalities. Additionally, to further extend modelling capabilities and efficiency, we generalized Cardinal to actively consider constraints over set functions other than cardinality. The Cardinal version just released allows declaring union, minimum and maximum functions on set variables, and easily constraining those functions, letting Cardinal especial inferences efficiently take care of different problems. We describe such extensions and discuss its potentialities, which promise interesting research directions.

关键词： CLP constraint logic programming PI, primary input TG, test generation

来源：评论

学校读者我要写书评

暂无评论

Proving correctness of imperative programs by linearizing constrained Horn clauses

引用

THEORY AND PRACTICE OF logic programming 2015年第4-5期15卷 635-650页

作者： De Angelis, Emanuele Fioravanti, Fabio Pettorossi, Alberto Proietti, Maurizio Univ G dAnnunzio DEC Pescara Italy Univ Roma Tor Vergata DICII Rome Italy CNR IASI Rome Italy

We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a program prog, we consider a partial correctness specification of the form {phi} prog {psi}, where the assertions phi and psi are predicates defined by a set Spec of possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also called constrained Horn clauses). The verification method consists in constructing a set PC of constrained Horn clauses whose satisfiability implies that {phi} prog {psi} is valid. We highlight some limitations of state-of-the-art constrained Horn clause solving methods, here called LA-solving methods, which prove the satisfiability of the clauses by looking for linear arithmetic interpretations of the predicates. In particular, we prove that there exist some specifications that cannot be proved valid by any of those LA-solving methods. These specifications require the proof of satisfiability of a set PC of constrained Horn clauses that contain nonlinear clauses (that is, clauses with more than one atom in their premise). Then, we present a transformation, called linearization, that converts PC into a set of linear clauses (that is, clauses with at most one atom in their premise). We show that several specifications that could not be proved valid by LA-solving methods, can be proved valid after linearization. We also present a strategy for performing linearization in an automatic way and we report on some experimental results obtained by using a preliminary implementation of our method.

关键词： Program verification Partial correctness specifications Horn clauses constraint logic programming Program transformation

来源：评论

学校读者我要写书评

暂无评论

Program Verification using constraint Handling Rules and Array constraint Generalizations

引用

FUNDAMENTA INFORMATICAE 2017年第1期150卷 73-117页

作者： De Angelis, Emanuele Pettorossi, Alberto Fioravanti, Fabio Proietti, Maurizio Univ G dAnnunzio Viale Pindaro 42 I-65127 Pescara Italy Univ Roma Tor Vergata Via Politecn 1 I-00133 Rome Italy CNR IASI Via Taurini 19 I-00185 Rome Italy

The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program progas a predicate incorrect defined by a CLP program T, and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs thatmanipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

关键词： constraint Handling Rules constraint logic programming Program transformation Program verification

来源：评论

学校读者我要写书评

暂无评论

Dischargeable Obligations in the SCIFF Framework

引用

FUNDAMENTA INFORMATICAE 2020年第3-4期176卷 321-348页

作者： Alberti, Marco Gavanelli, Marco Lamma, Evelina Riguzzi, Fabrizio Satoh, Ken Zese, Riccardo Univ Ferrara Dipartimento Matemat & Informat Via Saragat 1 I-44122 Ferrara Italy Univ Ferrara Dipartimento Ingn Via Saragat 1 I-44122 Ferrara Italy Natl Inst Informat Principles Informat Res Div Chiyoda Ku 2-1-2 Hitotsubashi Tokyo 1018430 Japan

Abductive logic programming (ALP) has been proven very effective for formalizing societies of agents, commitments and norms, in particular by mapping the most common deontic operators (obligation, prohibition, permission) to abductive expectations. In our previous works, we have shown that ALP is a suitable framework for representing norms. Normative reasoning and query answering were accommodated by the same abductive proof procedure, named SCIFF. In this work, we introduce a defeasible flavour in this framework, in order to possibly discharge obligations in some scenarios. Abductive expectations can also be qualified as dischargeable, in the new, extended syntax. Both declarative and operational semantics are improved accordingly, and proof of soundness is given under syntax allowedness conditions. Moreover, the dischargement itself might be proved invalid, or incoherent with the rules, due to new knowledge provided later on. In such a case, a discharged expectation might be reinstated and hold again after some evidence is given. We extend the notion of dischargement to take into consideration also the reinstatement of expectations. The expressiveness and power of the extended framework, named SCIFFD, is shown by modeling and reasoning upon a fragment of the Japanese Civil Code. In particular, we consider a case study concerning manifestations of intention and their rescission (Section II of the Japanese Civil Code).

关键词： Normative reasoning Abductive logic programming constraint logic programming Dischargement of expectations

来源：评论

学校读者我要写书评

暂无评论

TCHR: a framework for tabled CLP

引用

THEORY AND PRACTICE OF logic programming 2008年第4期8卷 491-526页

作者： Schrijvers, Tom Demoen, Bart Warren, David S. Katholieke Univ Leuven Dept Comp Sci Louvain Belgium SUNY Stony Brook Dept Comp Sci Stony Brook NY 11794 USA

Tabled constraint logic programming is a powerful execution mechanism for dealing with constraint logic programming without worrying about fixpoint computation. Various applications, e.g. in the fields of program analysis and model checking, have been proposed. Unfortunately, a high-level system for developing new applications is lacking, and programmers are forced to resort to complicated ad hoc solutions. This papers presents TCHR, a high-level framework for tabled constraint logic programming. It integrates in a light-weight manner constraint Handling Rules (CHR), a high-level language for constraint solvers, with tabled logic programming. The framework is easily instantiated with new application-specific constraint domains. Various high-level operations can be instantiated to control performance. In particular, we propose a novel, generalized technique for compacting answer sets.

关键词： constraint logic programming constraint handling rules tabled execution

来源：评论

学校读者我要写书评

暂无评论

CLP-based protein fragment assembly

引用

THEORY AND PRACTICE OF logic programming 2010年第4-6期10卷 709-724页

作者： Dal Palu, Alessandro Dovier, Agostino Fogolari, Federico Pontelli, Enrico Univ Parma Dept Math I-43100 Parma Italy Univ Udine Dept Math & Comp Sci I-33100 Udine Italy Univ Udine Dept Biomed Sci I-33100 Udine Italy New Mexico State Univ Dept Comp Sci Las Cruces NM 88003 USA

The paper investigates a novel approach, based on constraint logic programming (CLP), to predict the 3D conformation of a protein via fragments assembly. The fragments are extracted by a preprocessor-also developed for this work-from a database of known protein structures that clusters and classifies the fragments according to similarity and frequency. The problem of assembling fragments into a complete conformation is mapped to a constraint solving problem and solved using CLP. The constraint-based model uses a medium discretization degree C alpha-side chain centroid protein model that offers efficiency and a good approximation for space filling. The approach adapts existing energy models to the protein representation used and applies a large neighboring search strategy. The results shows the feasibility and efficiency of the method. The declarative nature of the solution allows to include future extensions, e.g., different size fragments for better accuracy.

关键词： constraint logic programming protein fragment assembly

来源：评论

学校读者我要写书评

暂无评论

Extending Constructive logic Negation with Types

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2009年 246卷 183-198页

作者： Munoz-Hernandez, Susana Jose Moreno-Navarro, Juan Univ Politecn Madrid Fac Informat Campus Montegancedo Boadilla Monte Madrid 28660 Spain IMDEA Software Madrid 28660 Spain

Negation has traditionally been a difficult issue in logic programming. Most of Prolog programmers have been restricted to use just a weak negation technique, like negation as failure. Many alternative semantics were proposed for achieving constructive negation in the last 20 years, but no implementation was provided so far because of its exponential complexity and the difficulty for developing it. First effective implementations of constructive negation into standard Prolog compilers are available just recently, around 2003, provided by our previous works. In this paper we present an extension of our implementations by introducing types in programs, thus improving usability as well as efficiency in some cases of our implementations of constructive negation. This can make constructive negation an interesting approach for its use in data bases querying, web search, filtered search, ontologies querying, coding rules, business rules, etc. Thanks to the use of types, our constructive negation can provide concrete values as results, instead of constraints (as in our previous works). We provide details about the semantics and the implementation in our approaches of classical, finite constructive, and intensional negation. The paper also includes some practical examples additionally allowing for providing measurements of computational behavior.

关键词： logic programming Implementation Negation Types constraint logic programming Constructive Negation Non-monotonic Reasoning

来源：评论

学校读者我要写书评

暂无评论

Capacitated vehicle routing problem with pick-up and alternative delivery (CVRPPAD): model and implementation using hybrid approach

引用

ANNALS OF OPERATIONS RESEARCH 2019年第1-2期273卷 257-277页

作者： Sitek, Pawel Wikarek, Jaroslaw Kielce Univ Technol Dept Informat Syst Kielce Poland

The paper presents an optimization model and its implementation using a hybrid approach for the Capacitated Vehicle Routing Problem with Pick-up and Alternative Delivery (CVRPPAD). The development of the CVRPPAD was motivated by postal items distribution issues. The model proposed combines various features of Vehicle Routing Problem variants. The novelty of this model lies in the introduction of alternativeness of item delivery points, differentiation of delivery point types in terms of their capacity (parcel lockers) and possibility of collecting the items during the execution of delivery routes. The model also takes into account a possibility of introducing time windows related to delivery time. The proposed data structure in the form of sets of facts facilitates the implementation of the model in all environments, constraint logic programming (CLP), Mathematical programming (MP), metaheuristics, databases, etc. The model is implemented in the MP, hybrid CLP/MP, and hybrid CLP/heuristic environments. The hybrid CLP/MP approach is the authors' original solution, which has already been used to solve Supply Chain Management problems, scheduling problems, routing problems etc. For large size problems, considering their combinatorial character, the proposed CLP/MP approach is ineffective. Its effectiveness will improve when MP is replaced by a heuristic. All implementations were performed on the same data instances (facts), which made it possible to compare them according to the solution search time, number of decision variables and number of constraints. The directions into which the model can be further developed were also presented.

关键词： VRP CVRP constraint logic programming mathematical programming Hybrid approach Optimization Heuristics

来源：评论

学校读者我要写书评

暂无评论

A constraint-BASED REASONING FRAMEWORK FOR BEHAVIORAL ANIMATION

引用

COMPUTER GRAPHICS FORUM 1994年第5期13卷 315-324页

作者： MAH, S CALVERT, TW HAVENS, W Graphics and Multimedia Research Lab / Intelligent Systems Lab School of Computing Science Simon Fraser University Burnaby B.C. Canada V5A 1S6 e-mail: sang@cs.sfu.ca tom@cs.sfu.ca havens@cs.sfu.ca

Behaviour is a reflection of a reasoning process that must deal with constraints imposed by an external environment, internal knowledge and physical structure. This paper proposes a framework for behavioural animation that is based on the next generation of object-oriented, constraint-based expert systems technology, and applies a control structure of knowledge agents and knowledge units to determine the behaviour of objects to be animated. Knowledge agents are responsible for planning, plan implementation and information extraction from the environment. The activity of an agent is dependent on the knowledge units ascribed to them by the animator. The interaction between agents and knowledge units is resolved by the reasoning engine, and thus, influences the eventual motion displayed. An example given in NSAIL, a pilot implementation using the model-based ECHIDNA constraint logic programming shell. With this approach, the motion for a sailing scenario and other behavioural domains can be specified at a high level through the characterization of the knowledge agents.

关键词： BEHAVIORAL ANIMATION constraint-BASED REASONING KNOWLEDGE-BASED ANIMATION constraint logic programming EXPERT SYSTEMS AGENTS SAILING

来源：评论

学校读者我要写书评

暂无评论

Typing constraint logic programs

引用

THEORY AND PRACTICE OF logic programming 2001年第6期1卷 751-777页

作者： Fages, F Coquery, E INRIA Rocquencourt Projet Contraintes F-78153 Le Chesnay France

We present a prescriptive type system with parametric polymorphism and subtyping for constraint logic programs. The aim of this type system is to detect programming errors statically. It introduces a type discipline for constraint logic programs and modules, while maintaining the capabilities of performing the usual coercions between constraint domains. and of typing meta-programming predicates, thanks to the flexibility of subtyping. The property of subject reduction expresses the consistency of a prescriptive type system w.r.t. the execution model: if a program is 'well-typed'. then all derivations starting from a 'well-typed' goat are again 'well-typed'. That property is proved w.r.t. the abstract execution model of constraint programming which proceeds by accumulation of constraints only. and w.r.t. an enriched execution model with type constraints for substitutions. We describe our implementation of the system for type checking and type inference. We report our experimental results on type checking ISO-Prolog, the (constraint) libraries of Sicstus Prolog and other Prolog programs.

关键词： type systems Prolog constraint logic programming subtyping Metaprogramming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：