Solvers on finite domains use local consistency notions to remove values from the domains. this paper defines value withdrawal explanations. Domain reduction is formalized with chaotic iterations of monotonic operator...
详细信息
the traditional investigation of rewriting and narrowing strategies aims at establishing fundamental properties, such as soundness, completeness and/or optimality, of a strategy. In this work, we analyze and compare r...
详细信息
the replacement is a very powerful transformation operation which - both within the functional paradigm as well as within the logicprogramming one - can mimic the most common transformation operations such as unfold,...
详细信息
ISBN:
(纸本)3540676287
the replacement is a very powerful transformation operation which - both within the functional paradigm as well as within the logicprogramming one - can mimic the most common transformation operations such as unfold, fold, switching, distribution. Because of this flexibility, it can be incorrect if used without specific applicability conditions. In this paper we present applicability conditions which ensure the correctness of the replacement operation in the context of Concurrent constraint Programs. Furthermore we show that, under these conditions, the replacement generalizes boththe unfolding operation as well as a restricted form of folding operation.
It has become popular to express dataflow analyses in logical form. In this paper we investigate a new approach to the analysis of functional programs, based on synthesis of constraintlogic programs. We sketch how th...
详细信息
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
It has become popular to express dataflow analyses in logical form. In this paper we investigate a new approach to the analysis of functional programs, based on synthesis of constraintlogic programs. We sketch how the language Toupie, originally designed withlogic program analysis as one objective, lends itself also to sophisticated strictness analysis. Strictness analysis is straightforward in the simplest case, that of analysing a first-order functional language using just two strictness values, namely divergence and "don't know". Mycroft's classical translation immediately yields perfectly valid Boolean constraintlogic programs, which, when run, provide the desired strictness information. However, more sophisticated analysis requires more complex domains of strictness values. We recast Wadler's classical analysis over a 2n-point domain as finite-domain constraint solving. this approach has several advantages. First, the translation is relatively simple. We translate a recursive function definition into one or two constraint program clauses, in a manner which naturally extends Mycroft's translation for the 2-point case, where the classical approach translate the definition of an n-place function over lists into 4(n) mutually recursive equations. Second, the resulting program produces relational information, allowing for example to ask which combinations of properties of input will produce a given output. third, the approach allows us to leverage from established technology, for solving finite-domain constraints, as well as for finding fixed points. Finally, the use of (disjunctive) constraints can yield a higher precision in the analysis of some programs.
the proceedings contain 30 papers. the special focus in this conference is on Computer Science logic. the topics include: Call-by-value games;a specification language based on WS2S;evolution as a computational engine;...
ISBN:
(纸本)3540645705
the proceedings contain 30 papers. the special focus in this conference is on Computer Science logic. the topics include: Call-by-value games;a specification language based on WS2S;evolution as a computational engine;timeless games;from action calculi to linear logic;a sequent calculus for circumscription;linear lower bounds and simulations in frege systems with substitutions;a formulation of linear logic based on dependency-relations;resolution and the weak pigeonhole principle;higher-order matching and tree automata;spectra with only unary function symbols;classical proofs via basic logic;full abstractness for a functional/concurrent language with higher-order value-passing;a duality theory for quantitative semantics;a mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion;equational axioms of test algebra;the logic-automaton connection in practice;existence of reduction hierarchies;a game-theoretic, concurrent and fair model of the typed A-calculus, with full recursion;a conjunctive logical characterization of nondeterministic linear time;on the computational complexity of type 2 functionals;categories with algebraic structure;concurrent constraintprogramming and non-commutative logic;a hierarchical approach to monadic second-order logic over graphs and the monadic quantifier alternation hierarchy over grids and pictures.
the model-checking problem for 1-safe Petri nets and linear-time temporal logic (LTL) consists of deciding, given a 1-safe Petri net and a formula of LTL, whether the Petri net satisfies the property encoded by the fo...
详细信息
ISBN:
(纸本)3540631399
the model-checking problem for 1-safe Petri nets and linear-time temporal logic (LTL) consists of deciding, given a 1-safe Petri net and a formula of LTL, whether the Petri net satisfies the property encoded by the formula. this paper introduces a semidecision test for this problem. By a semidecision test we understand a procedure which may answer 'yes', in which case the Petri net satisfies the property, or 'don't know'. the test is based on a variant of the so called automata-theoretic approach to model-checking and on the notion of T-invariant. We analyse the computational complexity of the test, implement it using 2lp - a constraintprogramming tool, and apply it to two case studies. this paper is a (very) abbreviated version of [6].
the proceedings contain 18 papers. the special focus in this conference is on functional and logicprogramming. the topics include: Safe folding/unfolding with conditional narrowing;optimal non-deterministic functiona...
ISBN:
(纸本)3540634592
the proceedings contain 18 papers. the special focus in this conference is on functional and logicprogramming. the topics include: Safe folding/unfolding with conditional narrowing;optimal non-deterministic functionallogic computations;a semantic basis for termination analysis of logic programs and its realization using symbolic norm constraints;parallelizing functional programs by generalization;higher-order equational unification via explicit substitutions;parameterised higher-order algebraic specifications;a computation model for a higher-order functionallogic language;on composable properties of term rewriting systems;needed reductions with context-sensitive rewriting;conditional term graph rewriting;lazy narrowing with parametric order sorted types;termination of algebraic type systems;proof net semantics of proof search computation;perpetuality and uniform normalization;model generation with existentially quantified variables and constraints and optimal left-to-right pattern-matching automata.
the proceedings contain 17 papers. the special focus in this conference is on logic Program Synthesis and Transformation. the topics include: A multi-level approach to program synthesis;programs without failures;gener...
ISBN:
(纸本)3540650741
the proceedings contain 17 papers. the special focus in this conference is on logic Program Synthesis and Transformation. the topics include: A multi-level approach to program synthesis;programs without failures;generalised logic program transformation schemas;logic program schemas, constraints and semi-unification;implicit program synthesis by a reversible metainterpreter;termination analysis for tabled logicprogramming;on correct program schemas;analysis of logic programs with delay;constraint-based partial evaluation of rewriting-based functionallogic programs;preserving termination of tabled logic programs while unfolding;unfolding the mystery of mergesort;towards a logic for reasoning about logic programs transformation;a higher order reconstruction of stepwise enhancement;development of correct transformation schemata for prolog programs;constrained regular approximation of logic programs;a logic framework for the incremental inductive synthesis of datalog theories and to parse or not to parse.
the proceedings contain 25 papers. the special focus in this conference is on Application and theory of Petri Nets. the topics include: Model checking LTL using constraintprogramming;on the composition of timed syste...
ISBN:
(纸本)3540631399
the proceedings contain 25 papers. the special focus in this conference is on Application and theory of Petri Nets. the topics include: Model checking LTL using constraintprogramming;on the composition of timed systems;some issues about petri net application to manufacturing and process supervisory control;on the abstraction of coloured petri nets;multi-agent-systems based on coloured petri nets;on the complexity of the linear-time mu-calculus for petri nets;improved implementations via a new structural equivalence on labelled nets;time processes for time petri nets;timed petri nets and temporal linear logic;efficient handling of phase-type distributions in generalized stochastic petri nets;analysis of petri nets with a dynamic priority method;a compositional partial order semantics for petri net components;covering step graph preserving failure semantics;siphons, traps and high-level nets with infinite color domains;a gentle introduction to formal methods in a distributed systems course;transition systems of elementary net systems with inhibitor arcs;coupling asynchrony and interrupts;modelling and solving constraint satisfaction problems through petri nets;fault detection in telecommunication networks based on petri net representation of alarm propagation;verification of workflow nets;verification of siphons and traps for algebraic petri nets and orthogonal transformations for coloured petri nets.
the proceedings contain 21 papers. the special focus in this conference is on Extensions of logicprogramming. the topics include: Semantics of constraintlogic programs with bounded quantifiers;translating a modal la...
ISBN:
(纸本)9783540609834
the proceedings contain 21 papers. the special focus in this conference is on Extensions of logicprogramming. the topics include: Semantics of constraintlogic programs with bounded quantifiers;translating a modal language with embedded implication into horn clause logic;pruning the search space of logic programs;a significant extension of logicprogramming by adapting model building rules;efficient resource management for linear logic proof search;a logic language based on GAMMA-like multiset rewriting;handling equality in logicprogramming via basic folding;an abstract machine for reasoning about situations, actions, and causality;on the computational complexity of propositional logic programs with nested implications;proof-theory for extensions of logicprogramming;a fibrational semantics for logic programs;language and implementation;a new framework for declarative programming;extending constructive negation for partial functions in lazy functional-logic languages;total correctness of logic programs;a declarative semantics for the prolog cut operator;a definitional approach to functionallogicprogramming;soundness and completeness of non-classical extended SLD-resolution and some postulates for nonmonotonic theory revision applied to logicprogramming.
暂无评论