We introduce negation into coinductive logicprogramming (co-LP) via what we term Coinductive SLDNF (co-SLDNF) resolution. We present declarative and operational semantics of co-SLDNF resolution and present their equi...
详细信息
ISBN:
(纸本)9783642125911
We introduce negation into coinductive logicprogramming (co-LP) via what we term Coinductive SLDNF (co-SLDNF) resolution. We present declarative and operational semantics of co-SLDNF resolution and present their equivalence under the restriction of rationality. Co-LP with co-SLDNF resolution provides a powerful, practical and efficient operational semantics for Fitting's Kripke-Kleene three-valued logic with restriction of rationality. Further, applications of co-SLDNF resolution are also discussed and illustrated where Co-SLDNF resolution allows one to develop elegant implementations of modal logics. Moreover it provides the capability of non-monotonic inference (e.g., predicate Answer Set programming) that can be used to develop novel and effective first-order modal non-monotonic inference engines.
We introduce a new native code compiler for Curry code-named Sprite. Sprite is based on the Fair Scheme, a compilation strategy that provides instructions for transforming declarative, non-deterministic programs of a ...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
We introduce a new native code compiler for Curry code-named Sprite. Sprite is based on the Fair Scheme, a compilation strategy that provides instructions for transforming declarative, non-deterministic programs of a certain class into imperative, deterministic code. We outline salient features of Sprite, discuss its implementation of Curry programs, and present benchmarking results. Sprite is the first-to-date operationally complete implementation of Curry. Preliminary results show that ensuring this property does not incur a significant penalty.
Recent progress in Biology and data-production technologies push research toward a new interdisciplinary field, named Systems Biology, where the challenge is to break the complexity walls for reasoning about large bio...
详细信息
ISBN:
(纸本)3540326545
Recent progress in Biology and data-production technologies push research toward a new interdisciplinary field, named Systems Biology, where the challenge is to break the complexity walls for reasoning about large biomolecular interaction systems. Pioneered by Regev, Silverman and Shapiro, the application of process calculi to the description of biological processes has been a source of inspiration for many researchers coming from the programming language community. In this presentation, we give an overview of the Biochemical Abstract Machine (BIOCHAM), in which biochemical systems are modeled using a simple language of reaction rules, and the biological properties of the system, known from experiments, are formalized in temporal logic. In this setting, the biological validation of a model can be done by model-checking, both qualitatively and quantitatively. Moreover, the temporal properties can be turned into specifications for learning modifications or refinements of the model, when incorporating new biological knowledge.
there are mainly two approaches for structuring logicprograms. the first one is based on defining some notion of program unit or module and on providing a number of composition operators. the second approach consists...
详细信息
ISBN:
(纸本)3540326545
there are mainly two approaches for structuring logicprograms. the first one is based on defining some notion of program unit or module and on providing a number of composition operators. the second approach consists in enriching logicprogramming with a mechanism of abstraction and scoping rules that are frequently found, for instance, in procedural programming. More precisely, this approach has been advocated by Miller and others using implications embedded in the goals of the given program as a structuring mechanism. However, as Giordano, Martelli and Rossi pointed out, we can associate two different visibility rules (static and dynamic) to this kind of structuring mechanism where, obviously, the semantics of the given program depends on the chosen rule. In this paper we consider normal constraint logicprograms (with constructive negation a la Drabent as operational semantics) extended with embedded implications with a static visibility rule. this class of programs combines the expressive power of normal programs withthe capability to organize and to enhance dinamically their sets of clauses. In particular, first, we introduce an operational semantics based on constructive negation for this class of programs, taking into account the static visibility rule. then, we present an alternative semantics in terms of a transformation of the given structured program into a flat one. Finally, we prove the adequacy of this transformation by showing that it preserves the computed answers of the given program. Obviously, this transformation semantics can be used as the basis for an implementation of this structuring mechanism.
Constraint Handling Rules (CHR) is a committed-choice rule-basedprogramming language. Rules rewrite a global multi-set of constraints to another. Overlapping sets of constraints within the rules and the order of cons...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
Constraint Handling Rules (CHR) is a committed-choice rule-basedprogramming language. Rules rewrite a global multi-set of constraints to another. Overlapping sets of constraints within the rules and the order of constraints within rules and queries entail different derivation paths. In this work, a novel operational strategy is proposed which enables a high-level form of execution control that empowers a comprehensive and customizable execution strategy. It allows full space exploration for any CHR program, thus finding all possible results to a query which is interesting for many non-confluent programs. the proposed transformation is performed as a source-to-source transformation from any CHR program to one utilizing disjunction to force an exhaustive explorative execution strategy. the work is complemented by formal arguments to prove the correctness and completeness of the transformation.
Constraint Handling Rules (CHR) has expanded its application range over the past few years to include different algorithms rather than only constraint solvers. Animation of algorithms has been used over the past few d...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Constraint Handling Rules (CHR) has expanded its application range over the past few years to include different algorithms rather than only constraint solvers. Animation of algorithms has been used over the past few decades to aid the understanding of programming languages and how they are processed. In this work, we present a generic form of animating CHR programs using source-to-source transformation. the transformation converts CHR programs into their equivalent CHR programs enhanced with animation features, in an automated manner.
this paper presents a hybrid method for verification and synthesis of parameterized self-stabilizing protocols where algorithmic design and mechanical verification techniques/tools are used hand-in-hand. the core idea...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
this paper presents a hybrid method for verification and synthesis of parameterized self-stabilizing protocols where algorithmic design and mechanical verification techniques/tools are used hand-in-hand. the core idea behind the proposed method includes the automated synthesis of self-stabilizing protocols in a limited scope (i.e., fixed number of processes) and the use of theorem proving methods for the generalization of the solutions produced by the synthesizer. Specifically, we use the Prototype Verification System (PVS) to mechanically verify an algorithm for the synthesis of weakly self-stabilizing protocols. then, we reuse the proof of correctness of the synthesis algorithm to establish the correctness of the generalized versions of synthesized protocols for an arbitrary number of processes. We demonstrate the proposed approach in the context of an agreement and a coloring protocol on the ring topology.
this paper addresses the problem of synthesizing an asynchronous system from a temporal specification. We show that the cost of synthesizing a single-process implementation is the same for synchronous and asynchronous...
详细信息
ISBN:
(纸本)9783540714095
this paper addresses the problem of synthesizing an asynchronous system from a temporal specification. We show that the cost of synthesizing a single-process implementation is the same for synchronous and asynchronous systems (2EXPTIME-complete for CTL* and EXPTIME-complete for the mu-calculus) if we assume a full scheduler (i.e., a scheduler that allows every possible scheduling), and exponentially more expensive for asynchronous systems without this assumption (3EXPTIME-complete for CTL* and 2EXPTIME-complete for the mu-calculus). While multi-process synthesis for synchronous distributed systems is possible for certain architectures (like pipelines and rings), we show that the synthesis of asynchronous distributed systems is decidable if and only if at most one process implementation is unknown.
We show how to combine the two most powerful approaches for automated termination analysis of logicprograms (LPs): the direct approach which operates directly on LPs and the transformational approach which transforms...
详细信息
ISBN:
(纸本)9783642125911
We show how to combine the two most powerful approaches for automated termination analysis of logicprograms (LPs): the direct approach which operates directly on LPs and the transformational approach which transforms LPs to term rewrite systems (TRSs) and tries to prove termination of the resulting TRSs. To this end, we adapt the well-known dependency pair framework from TRSs to LPs. Withthe resulting method;one can combine arbitrary termination techniques for LPs in a completely modular way and one call use both direct and transformational techniques for different parts of the same LP.
We present a type theory characterizing the mobility and locality of program terms in a distributed computation. the type theory of our calculus is derived from logical notions of necessity (square A) and possibility ...
详细信息
ISBN:
(纸本)3540266550
We present a type theory characterizing the mobility and locality of program terms in a distributed computation. the type theory of our calculus is derived from logical notions of necessity (square A) and possibility (lozenge A) of the modal logic S4 via a Curry-Howard style isomorphism. logical worlds are interpreted as sites for computation, accessibility corresponds to dependency between processes at those sites. Necessity (square A) describes terms of type A which have a structural kind of mobility or location-independence. Possibility (lozenge A) describes terms of type A located somewhere, perhaps at a remote site. the modalities square and lozenge are defined in a clean, orthogonal manner, leading to a simple account of mobility and higher-order functions. For illustration, we assume an execution environment with each location distinguished by a mutable store. Here modal types ensure that store addresses never escape from the location where they are defined, eliminating a source of runtime errors. We speculate as to other advantages or trade-offs of this disciplined style of distributed programming.
暂无评论