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.

Successes in Logic Programs

COCCO, Nicoletta
1999

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10278/31956
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact