this book constitutes the thoroughly refereed and extended post-workshop proceedings of the 12thannual ERCIM internationalworkshop on constraintsolving and constraintlogicprogramming, CSCLP 2007, held in Rocquenc...
详细信息
ISBN:
(数字)9783540898122
ISBN:
(纸本)9783540898115
this book constitutes the thoroughly refereed and extended post-workshop proceedings of the 12thannual ERCIM internationalworkshop on constraintsolving and constraintlogicprogramming, CSCLP 2007, held in Rocquencourt, France, in June 2007. the 10 revised full papers presented were carefully reviewed and selected from 16 initial submissions. the papers address all aspects of constraint and logicprogramming, including foundational issues, implementation techniques, new applications as well as teaching issues. Particular emphasis is placed on assessing the current state of the art and identifying future directions.
Constrained constructor patterns are pairs of a constructor term pattern and a quantifier-free first-order logicconstraint, built from conjunction and disjunction. they are used to express state predicates for reacha...
详细信息
ISBN:
(数字)9783030635954
ISBN:
(纸本)9783030635954;9783030635947
Constrained constructor patterns are pairs of a constructor term pattern and a quantifier-free first-order logicconstraint, built from conjunction and disjunction. they are used to express state predicates for reachability logic defined over rewrite theories. Matching logic has been recently proposed as a unifying foundation for programming languages, specification and verification. It has been shown to capture several logical systems and/or models that are important for programming languages, including first-order logic with fixpoints and order-sorted algebra. In this paper, we investigate the relationship between constrained constructor patterns and matching logic. the comparison result brings us a mutual benefit for the two approaches. Matching logic can borrow computationally efficient proofs for some equivalences, and the language of the constrained constructor patterns can get a more logical flavor and more expressiveness.
Encoding finite linear CSPs as Boolean formulas and solvingthem by using modern SAT solvers has proven to be highly effective by the award-winning sugar system. We here develop an alternative approach based on ASP th...
详细信息
An interesting class of production/inventory control problems considers a single product and a single stocking location, given a stochastic demand with a known non-stationary probability distribution. Under a widely-u...
详细信息
ISBN:
(纸本)9783540738169
An interesting class of production/inventory control problems considers a single product and a single stocking location, given a stochastic demand with a known non-stationary probability distribution. Under a widely-used control policy for this type of inventory system, the objective is to find the optimal number of replenishments, their timings and their respective order-up-to-levels that meet customer demands to a required service level. We extend a known CP approach for this problem using a cost-based filtering method. Our algorithm can solve to optimality instances of realistic size much more efficiently than previous approaches, often with no search effort at all.
the new generic scheme CFLP(D) has been recently proposed in [14] as a logical and semantic framework for lazy constraint Functional logicprogramming over a parametrically given constraint domain D. Further, [15] pre...
详细信息
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially devel...
详细信息
ISBN:
(纸本)3540482814
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like programs. Here, we go one step further by considering conditional rewriting and explicit quantifications and constraints on size annotations. this allows to describe more precisely how the size of the output of a function depends on the size of its inputs. Hence, we can check the termination of more functions. We first give a general type-checking algorithm based on constraintsolving. then, we give a termination criterion withconstraints in Presburger arithmetic. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination.
the proceedings contain 41 papers. the special focus in this conference is on Verification, Temporal logic, Lambda Calculus, Linear logic and Descriptive Complexity. the topics include: Topological queries in spatial ...
ISBN:
(纸本)3540665366
the proceedings contain 41 papers. the special focus in this conference is on Verification, Temporal logic, Lambda Calculus, Linear logic and Descriptive Complexity. the topics include: Topological queries in spatial databases;constraint-based analysis of broadcast protocols;applicative control and computational complexity;applying rewriting techniques to the verification of erlang processes;an expressively complete temporal logic without past tense operators for mazurkiewicz traces;using fields and explicit substitutions to implement objects and functions in a de bruijn setting;a linear logical view of linear type isomorphisms;choice logic programs and Nash equilibria in strategic games;resolution method for modal logic with well-founded frames;fixpoint alternation and the game quantifier;open least element principle and bounded query computation;anti-symmetry of higher-order subtyping;monadic presentations of lambda terms using generalized inductive types;a logical viewpoint on process-algebraic quotients;data-refinement for call-by value programming languages and interactive theorem proving using type theory.
the proceedings contain 48 papers. the special focus in this conference is on logicprogramming and Nonmonotonic Reasoning. the topics include: Stable models for temporal theories;algorithmic decision theory meets log...
ISBN:
(纸本)9783319232638
the proceedings contain 48 papers. the special focus in this conference is on logicprogramming and Nonmonotonic Reasoning. the topics include: Stable models for temporal theories;algorithmic decision theory meets logic;relational and semantic data mining;shift design with answer set programming;advances in WASP;improving coordinated SMT-based system synthesis by utilizing domain-specific heuristics;integrating ASP into ROS for reasoning in robots;automated inference of rules with exception from past legal cases using ASP;solvingconstraint satisfaction problems with answer set programming;a theory of intentions for intelligent agents;answer set programming modulo acyclicity;a framework for goal-directed query evaluation with negation;implementing preferences with asprin;diagnosing automatic whitelisting for dynamic remarketing ads using hybrid ASP;performance tuning in answer set programming;enablers and inhibitors in causal justifications of logic programs;efficient problem solving on tree decompositions using binary decision diagrams;knowledge acquisition via non-monotonic reasoning in distributed heterogeneous environments;a formal theory of justifications;a new computational logic approach to reason with conditionals;interactive debugging of non-ground ASP programs;linking open-world knowledge bases using nonmonotonic rules;ASP, amalgamation, and the conceptual blending workflow;diagnostic reasoning for robotics using action languages;connecting object-oriented and logicprogramming;reasoning with forest logic programs using fully enriched automata;ASP solving for expanding universes and combining heuristics for configuration problems using answer set programming;infinitary equilibrium logic and strong equivalence and compacting boolean formulae for inference in probabilistic logicprogramming.
We present a, formally specified first order temporal logic. We give its syntax, semantics, and describe its implementation using the Eclipse constraintlogicprogramming language. the main feature of the implementati...
详细信息
ISBN:
(纸本)3540676899
We present a, formally specified first order temporal logic. We give its syntax, semantics, and describe its implementation using the Eclipse constraintlogicprogramming language. the main feature of the implementation is a graphical user interface. Because color coded symbols and graphs are used, the interface assumes no logical knowledge on the part of the user.
暂无评论