1,720,983 research outputs found
Successes in Logic Programs
No full textIn this paper we study how to verify that a pure Prolog program has solutions for a given query. The detailed analysis of the failure/ success behaviour of a program is necessary when dealing with transformation and verification of pure Prolog programs. In a previous work [10] we defined the class of noFD programs and queries which are characterized statically. We proved that a noFD query cannot have finitely failing derivations in a noFD program. Now, by introducing the concept of a set of exhaustive tests, we define the larger class of successful predicates. We prove that a noFD terminating query for successful predicates have at least one successful derivation. Moreover we propose some techniques based on program transformations for simplifying the verification of the successful condition
Programs Without Failures
No full textWe try to formalize the intuitive reasoning which we normally use to get convinced that a query has successful LD-derivations in a program. To this purpose we define the class of programs and queries without failures which have the property of not having finitely failing derivations. Such property is simple to verify, it is preserved through leftmost unfolding and it can be useful both in verifying properties of logic programs and in program transformation. The class of programs without failures is very restricted but in program transformations it is sufficient that only some predicates in the program are in the class
Basic Transformation Operations which preserve Computed Answer Substitutions of Logic Programs
No full textAbstractSome transformation operations for logic programs, basic for partial deduction, program specialization, and transformation, and for program synthesis from specifications, are studied with respect to the minimal S-model semantics defined in [31, 15–17]. Such a semantics is, in our opinion, more interesting than the usual least Herbrand model one since it captures the program's behavior with respect to computed answers. The S-semantics is also the strongest semantics which is maintained by unrestricted unfolding [31]. For such operations, we single out general applicability conditions, and prove that they guarantee that the minimal S-model semantics of a program is not modified by the transformation. Some sufficient conditions, which are very common in practice and easy to verify, since they are mostly syntactical, are also supplied with simple exemplifications
Preserving Universal Termination through Unfold/Fold
No full textWe study how to preserve universal termination besides computed answer substitutions while transforming definite programs. We consider the unfold operation both alone and combined with the introduction of a new definition and fold operations. We prove that unfold always preserves universal termination. Moreover we define a restricted version of the Tamaki-Sato's transformation sequence and show that it preserves universal termination as well
Norms on Terms and their use in Proving Universal Termination of a Logic Program
No full textAbstractIn this paper semi-linear norms, a class of functions to weight the terms occurring in a program, are defined and studied. All the functions in this class have the nice property of allowing a syntactical characterization of rigid terms, i.e. terms whose weight does not change under substitution. Based on these norms, a general proof method for universal termination of pure Prolog programs can be adapted to deal with a large class of programs in a simple way. The proof method requires pre/post specifications well-behaved with respect to substitutions to be associated with each predicate symbol in the program, and ordering functions not increasing with respect to substitutions to be associated with cycles in the program. The specification collects information on term properties which are useful to prove that the ordering functions actually decrease at each traversal of each cycle. Some examples of termination proof are also given
- …
