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 [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.
Autori: | ||
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 |