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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Apt, K.R.: Introduction to Logic Programming. In van Leeuwen, J. (ed.): Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier, Amsterdam and The MIT Press, Cambridge (1990)
Apt, K.R.: Declarative Programming in Prolog. In Miller, D. (ed.): Proceedings of the 1993 International Symposium on Logic Programming, The MIT Press 1993 12–35
Apt, K.R.: From Logic Programming to Prolog. Prentice Hall International Series in Computer Science 1997
Apt, K. R., Etalle, S.: On the Unification Free Prolog Programs. In Borzkowski, A., Sokolowski, S. (eds.): Proceedings of the Conference on Mathematical Foundations of Computer Science (MFCS 93). Lecture Notes in Computer Science, vol. 711, Springer-Verlag, Berlin 1993 1–19
Apt, K. R., Marchiori, E.: Reasoning about Prolog Programs: from Modes through Types to Assertions. Formal Aspects of Computing, 6(6A) 1994 743–765
Apt, K. R., Pedreschi, D.: Studies in Pure Prolog: Termination. In Lloyd J.W. (ed.): Proceedings of the Simposium in Computational Logic, Springer-Verlag, Berlin 1990 150–176
Apt, K.R., Pedreschi, D.: Reasoning about Termination of Pure Prolog Programs. Information and Computation, 106(1) 1993 109–157
Bossi, A., Cocco, N.: Verifying Correctness of Logic Programs. In Diaz, J., Orejas, F. (eds.): Proceedings of TAPSOFT’ 89, Lecture Notes in Computer Science, vol. 352, Springer-Verlag, Berlin 1989 96–110
Bossi, A., Cocco, N.: Preserving Universal Termination through Unfold/Fold. In Levi, G., Rodriguez-Artalejo, M. (eds.): Algebraic and Logic Programming-Proceedings ALP’94, Lecture Notes in Computer Science, vol. 850, Springer-Verlag, Berlin 1994 269–286
Bossi, A., Cocco, N.: Programs without Failures. In Fuchs, N. (ed.): Proceedings LOPSTR’97, Lecture Notes in Computer Science, vol. 1463, Springer-Verlag, Berlin 1997 28–48
Bossi, A., Cocco, N., Etalle, S.: Transformation of Left Terminating Programs: The Reordering Problem. In Proietti, M. (ed.): Proceedings LOPSTR’95, Lecture Notes in Computer Science, vol. 1048, Springer-Verlag, Berlin 1996 33–45
Bossi, A., Cocco, N., Fabris, M.: Norms on Terms and their Use in Proving Universal Termination of a Logic Program. Theoretical Computer Science, 124 1994 297–328
Boye, J., Maluszynski, J.: Two Aspects of Directional Types. In Sterling L. (ed.): Proc. Int’l Conf. on Logic Programming, The MIT Press 1995 747–761
Bronsard, F., Lakshman, T. K., Reddy, U. S.: A Framework of Directionalities for Proving Termination of Logic Programs. In Apt, K.R. (ed.) Proceedings of the Joint International Conference and Symposium on Logic Programming, The MIT Press 1992 321–335
Bruynooghe, M., Janssens, G.: An Instance of Abstract Interpretation: Integrating Type and Mode Inferencing. In Proceedings of the International Conference on Logic Programming, The MIT Press 1988 669–683
Chadha, R., Plaisted, D.A.: Correctness of Unification Without Occur Check in Prolog. Journal of Logic Programming, 18(2) 1994 99–122
Le Charlier, B., Leclere, C., Rossi, S., Cortesi, A.: Automated Verification of Behavioural Properties of Prolog Programs. In Advances in Computing Science-ASIAN’97, Lecture Notes in Computer Science, vol. 1345 1997 225–237
Debray, S., Lopez-Garcia, P., Hermenegildo, M.: Non-Failure Analysis for Logic Programs. In Naish, L. (ed.): Proceedings of the International Symposium on Logic Programming, The MIT Press 1997 48–62
Debray, S.K.: Static Inference of Modes and Data Dependencies in Logic Programs. ACM Transactions on Programming Languages and Systems, 11(3) 1989 419–450
Debray, S.K., Lin, N.: Cost Analysis of Logic Programs. ACM Transactions on Programming Languages and Systems, 15(5) 1993 826–875
Drabent, W., Maluszynski, J.: Inductive Assertion Method for Logic Programs. Theoretical Computer Science, 59 1988133–155
Henderson, F., Conway, T., Somogyi, Z., Jeffery, D.: The Mercury Language Reference Manual. Technical Report TR 96/10, Dep. of Computer Science, University of Melbourne (1996)
Lloyd, J.W.: Foundations of Logic Programming. Springer-Verlag, Berlin 1987 Second edition.
De Schreye, D., Decorte, S.: Termination of Logic Programs: the Never-Ending Story. Journal of Logic Programming, 19-20 1994 199–260
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bossi, A., Cocco, N. (1999). Successes in Logic Programs. In: Flener, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 1998. Lecture Notes in Computer Science, vol 1559. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48958-4_12
Download citation
DOI: https://doi.org/10.1007/3-540-48958-4_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65765-1
Online ISBN: 978-3-540-48958-0
eBook Packages: Springer Book Archive