In this work, we devise an analysis that searches for semantically equivalent code fragments within a given logicprogram. the presence of duplicated code (or functionality) is a primary indication that the design of ...
详细信息
ISBN:
(纸本)3540266550
In this work, we devise an analysis that searches for semantically equivalent code fragments within a given logicprogram. the presence of duplicated code (or functionality) is a primary indication that the design of the program can be improved by performing a so-called refactoring transformation. Within the framework of our analysis, we formally characterize three situations of duplicated functionality and their associated refactorings: the extraction of a duplicated goal into a new predicate, the removal of equivalent predicates and the generalization of two predicates into a higher-order predicate. the resulting analysis detects in a completely automatic way what program fragments are suitable candidates for the considered refactoring transformations.
A variable is local if it occurs in a clause body but not in its head. Local variables appear naturally in practical logicprogramming, but they complicate several aspects such as negation, compilation, memoization, s...
详细信息
ISBN:
(纸本)3540326545
A variable is local if it occurs in a clause body but not in its head. Local variables appear naturally in practical logicprogramming, but they complicate several aspects such as negation, compilation, memoization, static analysis, program approximation by neural networks etc. As a consequence, the absence of local variables yields better performance of several tools and is a prerequisite for many technical results. In this paper, we introduce an algorithm that eliminates local variables from a wide proper subclass of normal logicprograms. the proposed transformation preserves the Clark-Kunen semantics for normal logicprograms.
We present a method based on logicprogramtransformation, for verifying Computation Tree logic (CTL*) properties of finite state reactive systems. the finite state systems and the CTL* properties we want to verify, a...
详细信息
ISBN:
(纸本)9783642125911
We present a method based on logicprogramtransformation, for verifying Computation Tree logic (CTL*) properties of finite state reactive systems. the finite state systems and the CTL* properties we want to verify, are encoded as logicprograms on infinite lists. Our verification method consists of two steps. In the first step we transform the logicprogramthat encodes the given System and the given property, into a monadic w-program, that is, a stratified program defining nullary or unary predicates on infinite lists. this transformation is performed by applying unfold/fold rules that preserve the perfect model of the initial program. In the second step we verify the property of interest by using a proof method for monadic w-programs.
In very recent work, we introduced a non-termination preserving transformation from logicprograms with cut to definite logicprograms. While that approach allows us to prove termination of a large class of logic prog...
详细信息
ISBN:
(纸本)9783642205507
In very recent work, we introduced a non-termination preserving transformation from logicprograms with cut to definite logicprograms. While that approach allows us to prove termination of a large class of logicprograms with cut automatically, in several cases the transformation results in a non-terminating definite logicprogram. In this paper we extend the transformation such that logicprograms with cut are no longer transformed into definite logicprograms, but into dependency triple problems. By the implementation of our new method and extensive experiments, we empirically evaluate the practical benefit of our contributions.
programtransformation and in particular partial evaluation are appealing techniques for declarative programs to improve not only their performance. this paper presents the first step towards developing program transf...
详细信息
ISBN:
(纸本)3540266550
programtransformation and in particular partial evaluation are appealing techniques for declarative programs to improve not only their performance. this paper presents the first step towards developing programtransformation techniques for a concurrent constraint programming language where guarded rules rewrite and augment multi-sets of atomic formulae, called Constraint Handling Rules (CHR). We study the specialization of rules with regard to a given goal (query). We show the correctness of this programtransformation: Adding and removing specialized rules in a program does not change the program's operational semantics. Furthermore termination and confluence of the program are shown to be preserved.
this paper discusses refinement of programs that may raise and catch exceptions. We show that exceptions are expressed by a class of predicate transformers built on Arieli and Avron's four-valued logic and develop...
详细信息
ISBN:
(纸本)9783642125911
this paper discusses refinement of programs that may raise and catch exceptions. We show that exceptions are expressed by a class of predicate transformers built on Arieli and Avron's four-valued logic and develop a refinement framework for the four-valued predicate transformers. the resulting framework enjoys several refinement laws that are useful for stepwise refinement of programs involving exception handling and partial predicates. We demonstrate some typical usages of the refinement laws in the proposed framework by a few examples of programtransformation.
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of programsynthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number ...
详细信息
ISBN:
(纸本)3540266550
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of programsynthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem term enumeration,. To solve the problem, we use the Curry-Howard correspondence (propositions-as-types, proofs-as-programs) to transform it into a proof enumeration problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. this in turn yields a proof enumeration algorithm.
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logicprogramming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for t...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logicprogramming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the query. We propose a method of programtransformationthat allows to transform logicprograms in such a way that proof evidence is computed alongside SLD-derivations. We discuss two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.
We propose a new grouping operator for logicprograms based on the bag of predicate. the novelty of our proposal lies in the use of modes, which allows us to prove properties regarding groundness of computed answer su...
详细信息
ISBN:
(纸本)9783642125911
We propose a new grouping operator for logicprograms based on the bag of predicate. the novelty of our proposal lies in the use of modes, which allows us to prove properties regarding groundness of computed answer substitutions and termination. Moreover, modes allow us to define a somewhat declarative semantics for it and to relax some rather unpractical constraints on variable occurrences while retaining a straightforward semantics.
this paper introduces a modular framework for termination analysis of logicprogramming. To this end, we adapt the notions of dependency pairs and dependency graphs (which were developed for term rewriting) to the log...
详细信息
ISBN:
(纸本)9783540787686
this paper introduces a modular framework for termination analysis of logicprogramming. To this end, we adapt the notions of dependency pairs and dependency graphs (which were developed for term rewriting) to the logicprogramming domain. the main idea of the approach is that termination conditions for a program are established based on the decomposition of its dependency graph into its strongly connected components. these conditions can then be analysed separately by possibly different well-founded orders. We propose a constraint-based approach for automating the framework. then, for example, termination techniques based on polynomial interpretations can be plugged in as a component to generate well-founded orders.
暂无评论