Forward analysis procedures for infinite-state systems such as timed systems were limited to safety properties. We give the first constraint-based forward analysis for infinite-state systems that goes beyond safety pr...
详细信息
ISBN:
(纸本)3540439307
Forward analysis procedures for infinite-state systems such as timed systems were limited to safety properties. We give the first constraint-based forward analysis for infinite-state systems that goes beyond safety properties. Namely, we take the restriction of the mu-calculus to least-fixpoint formulas where negation is applied to closed subformulas only. We characterize these properties as perfect models of constraintlogic programs, and we present a tabulation procedure for the top-down evaluation of stratified constraintlogic programs.
the proceedings contain 41 papers. the topics discussed include: representing arithmetic constraints with finite automata: an overview;logic databases on the semantic web: challenges and opportunities;an abductive app...
ISBN:
(纸本)3540439307
the proceedings contain 41 papers. the topics discussed include: representing arithmetic constraints with finite automata: an overview;logic databases on the semantic web: challenges and opportunities;an abductive approach for analyzing event-based requirements specifications;access control for deductive databases by logicprogramming;using hybrid concurrent constraintprogramming to model dynamic biological systems;efficient real-time model checking using tabled logicprogramming and constraints;a model theoretic semantics for multi-level secure deductive databases;propagation completeness of reactive constraints;towards a declarative query and transformation language for XML and semistructured data: simulation unification;a proof-theoretic foundation for tabled higher-order logicprogramming;and a purely logical account of sequentiality in proof search.
this paper presents two proof systems for the equivalence of programs. the language concerned is CLP to which the universal quantifier is added (CLPV). Both systems, axe based on first order classical logic. the first...
详细信息
ISBN:
(纸本)3540439307
this paper presents two proof systems for the equivalence of programs. the language concerned is CLP to which the universal quantifier is added (CLPV). Both systems, axe based on first order classical logic. the first uses an induction rule and allows one to prove that the set of finite successes of a program is included in another program's corresponding set. the second uses a coinduction rule for proving the inclusion of the sets of infinite successes which contain the finite successes. Finally we show that the proof systems axe equivalent under some natural conditions.
We develop a framework for addressing correctness and timeliness-of-propagation issues for reactive constraints - global constraints or user-defined constraints that are implemented through constraint propagation. the...
详细信息
ISBN:
(纸本)3540439307
We develop a framework for addressing correctness and timeliness-of-propagation issues for reactive constraints - global constraints or user-defined constraints that are implemented through constraint propagation. the notion of propagation completeness is introduced to capture timeliness of constraint propagation. A generalized form of arc-consistency is formulated which unifies many local consistency conditions in the literature. We show that propagation complete implementations of reactive constraints achieve this arc-consistency when propagation quiesces. Finally, we use the framework to state and prove an impossibility result: that CHR cannot implement a common relation with a desirable degree of timely constraint propagation.
We present a concrete proposal for enhancing Prolog and Prolog based constraintlogicprogramming languages with a new language construct, the logical loop. this is a shorthand notation for the most commonly used recu...
详细信息
ISBN:
(纸本)3540439307
We present a concrete proposal for enhancing Prolog and Prolog based constraintlogicprogramming languages with a new language construct, the logical loop. this is a shorthand notation for the most commonly used recursive control structure: the iteration or tail recursion. We argue that this enhancement fits well withthe existing language concepts, enhances productivity and maintainability, and helps newcomers to the language by providing concepts that are familiar from many other programming languages. the language extension is implemented and has been in everyday use over several years within the ECL(i)PS(e)system.
the proceedings contain 44 papers. the special focus in this conference is on logicprogramming. the topics include: Representing arithmetic constraints with finite automata;logic databases on the semantic web;an abdu...
ISBN:
(纸本)3540439307
the proceedings contain 44 papers. the special focus in this conference is on logicprogramming. the topics include: Representing arithmetic constraints with finite automata;logic databases on the semantic web;an abductive approach for analysing event-based requirements specifications;trailing analysis for HAL;access control for deductive databases by logicprogramming;reasoning about actions with CHRs and finite domain constraints;using hybrid concurrent constraintprogramming to model dynamic biological systems;efficient real-time model checking using tabled logicprogramming and constraints;constraint-based infinite model checking and tabulation for stratified CLP;a model theoretic semantics for multi-level secure deductive databases;propagation completeness of reactive constraints;on enabling the WAM with region support;a different look at garbage collection for the WAM;logical algorithms;learning in logic with richprolog;towards a declarative query and transformation language for XML and semistructured data;a proof-theoretic foundation for tabled higher-order logicprogramming;proving the equivalence of CLP programs;a purely logical account of sequentiality in proof search;disjunctive explanations;computing stable models;towards local search for answer sets;a rewriting method for well-founded semantics with explicit negation;embedding defeasible logic into logic programs;a polynomial translation of logic programs with nested expressions into disjunctive logic programs;using logicprogramming to detect activities in pervasive healthcare;logicprogramming for software engineering;a logic-based system for application integration;the limits of horn logic programs and multi-adjoint logicprogramming.
CHR Grammars (CHRGs) are a grammar formalism that provides a constraint-solving approach to language analysis, built on top of constraint Handling Rules in the same way as Definite Clause Grammars (DCGs) on Prolog. CH...
ISBN:
(纸本)3540439307
CHR Grammars (CHRGs) are a grammar formalism that provides a constraint-solving approach to language analysis, built on top of constraint Handling Rules in the same way as Definite Clause Grammars (DCGs) on Prolog. CHRGs work bottom-up and add the following features when compared with DCGs: – An inherent treatment of ambiguity without backtracking. – Robust parsing; do not give up in case of errors but return the recognized phrases. – Flexibility to produce and consume arbitrary hypotheses making it straightforward to deal with abduction, integrity constraints, operators á la assumption grammars, and to incorporate other constraint solvers. – References to left and right syntactic context; apply for disambiguation of simple and otherwise ambiguous grammars, coordination in natural language, and tagger-like grammar rules.
In this paper we present a declarative language that aims at combining valuable features of CLP languages - namely, nondeterminism, unification, constraint solving, dynamic data structures - with features of conventio...
详细信息
the simulation relation is largely used in Model Checking where it allows to reduce Kripke structures, on which verification takes place, while preserving significant fragments of Temporal logic. Our approach to the p...
详细信息
logicprogramming based tools for real-time model checking are beginning to emerge. In a previous work we had demonstrated the feasibility of building such a model checker by combining constraint processing and tabula...
详细信息
ISBN:
(纸本)3540439307
logicprogramming based tools for real-time model checking are beginning to emerge. In a previous work we had demonstrated the feasibility of building such a model checker by combining constraint processing and tabulation. But efficiency and practicality of such a model checker were not adequately addressed. In this paper we describe XMC/dbm, an efficient model checker for real-time systems using tabling. Performance gains in XMC/dbmdirectly arise from the use of a lightweight constraint solver combined with tabling. Specifically the timing constraints axe represented by difference bound matrices which are encoded as Prolog terms. Operations on these matrices, the dominant component in real-time model checking, are shared using tabling. We provide experimental evidence that the performance of XMC/dbmis considerably better than our previous real-time model checker and is highly competitive to other well known real-time model checkers implemented in C/C++. An important aspect of XMC/dbm is that it can handle verification of systems consisting of untimed components with performance comparable to verification systems built specifically for untimed systems.
暂无评论