In 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  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.
|Data di pubblicazione:||1999|
|Titolo:||Successes in Logic Programs|
|Titolo del libro:||Proceedings LOPSTR'98|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1007/3-540-48958-4_12|
|Appare nelle tipologie:||4.1 Articolo in Atti di convegno|