Abstract
In this paper we shall consider proofs of declarative properties of Logic Programs, i.e. properties associated with the logical semantics of pure Logic Programs, in particular what is called the partial correctness of a logic program with respect to a specification. A specification consists of a logical formula associated with each predicate and establishing a relation between its arguments. A definite clause program is partially correct iff every possible answer substitution satisfies the specification.
This paper generalizes known results in logic programming in two ways : first it considers any kind of specification, second its results can be applied to extensions of logic programming such as functions or constraints.
In this paper we present two proof methods adapted from the Attribute Grammar field to the field of Logic Programming. Both are proven sound and complete. The first one consists of defining a specification stronger than the original one, which furthermore is inductive (fix-point induction).
The second method is a refinement of the first one : with every predicate, we associate a finite set of formulas (we call this an annotation), together with implications between formulas. The proofs become more modular and tractable, but the user has to verify the consistency of his proof, which is a decidable property. This method is particularly suitable for proving the validity of specifications which are not inductive.
Chapter PDF
Similar content being viewed by others
References
K.R. Apt, M.H. Van Emden: Contributions to the theory of Logic Programming. JACM V29, No 3, July 1982 pp 841–862.
B. Courcelle, P. Deransart: Proof of partial Correctness for Attribute Grammars with application to Recursive Procedure and Logic Programming. Information and Computation 78, 1, July 1988 (First publication INRIA RR 322-July 1984).
K.L. Clark: Predicate Logic as a Computational Formalism. Res. Mon. 79/59 TOC. Imperial College, December 1979.
S.A. Cook: Soundness and Completeness of an Axiom System for Programs Verification. SIAM Journal. Comput. V7, no 1, February 1978.
B. Courcelle: Attribute Grammars: Definitions, Analysis of Dependencies, Proof Methods. In Methods and Tools for Compiler Construction, CEC-INRIA Course (B. Lorho ed.). Cambridge University Press 1984.
P. Deransart: Logical Attribute Grammars. Information Processing 83, pp 463–469, R.E.A. Mason ed. North Holland, 1983.
Y. Deville: A Methodology for Logic Program Construction.PhD Thesis, Institut d'Informatique, Facultés Universitaires de Namur (Belgique), February 1987.
P. Deransart, G. Ferrand: Programmation en Logique avec Négation: Présentation Formelle. Publication du laboratoire d'Informatique, University of Orléans, RR 87-3 (June 1987).
P. Deransart, G. Ferrand: Logic Programming, Methodology and Teaching. K. Fuchi, L. Kott editors, French Japan Symposium, North Holland, pp 133–147, August 1988.
P. Deransart, G. Ferrand: On the Semantics of Logic Programming with Negation. RR 88-1, LIFO, University of Orléans, January 1988.
P. Deransart, M. Jourdan, B. Lorho: Attribute Grammars: Definitions, Systems and Bibliography, LNCS 323, Springer Verlag, August 1988.
P. Deransart, J. Maluszynski: Modelling Data Dependencies in Logic Programs by Attribute Schemata. INRIA, RR 323, July 1984.
P. Deransart, J. Maluszynski: Relating Logic Programs and Attribute Grammars. J. of Logic Programming 1985, 2 pp 119–155. INRIA, RR 393, April 1985.
P. Deransart, J. Maluszynski: A Grammatical View of Logic Programming. PLILP'88, Orléans, France, May 16–18, 1988, LNCS 348, Springer Verlag, 1989.
P. Deransart, G. Richard: The Formal Specification of PROLOG standard. Draft 3, December 1987. (Draft 1 published as BSI note PS 198, April 1987, actually ISO-WG17 document, August 1988).
W. Drabent, J. Maluszynski: Do Logic Programs Resemble Programs in Conventional Languages. SLP87, San Francisco, August 31–September 4 1987.
W. Drabent, J. Maluszynski: Inductive Assertion Method for Logic Programs. CFLP 87, Pisa, Italy, March 23–27 1987 (also: Proving Run-Time Properties of Logic Programs. University of Linköping. IDA R-86-23 Logprog, July 1986).
G. Ferrand: Error Diagnosis in Logic Programming, an Adaptation of E. Y. Shapiro's Methods. INRIA, RR 375, March 1985. J. of Logic Programming Vol. 4, 1987, pp 177–198 (French version: University of Orléans, RR no 1, August 1984).
N. Francez, O. Grumberg, S. Katz, A. Pnuelli: Proving Termination of Prolog Programs. In “Logics of Programs, 1985”, R. Parikh Ed., LNCS 193, pp 89–105, 1985.
L. Fribourg: Equivalence-Preserving Transformations of Inductive Properties of Prolog Programs. ICLP'88, Seattle, August 1988.
C.J. Hogger: Introduction to Logic Programming. APIC Studies in Data Processing no 21, Academic Press, 1984.
T. Katayama, Y. Hoshino: Verification of Attribute Grammars. 8th ACM POPL Conference. Williamsburg, VA pp 177–186, January 1981.
D.E. Knuth: Semantics of Context Free Languages. Mathematical Systems Theory 2, 2, pp 127–145, June 1968.
T. Kanamori, H. Seki: Verification of Prolog Programs using an Extension of Execution. In (Shapiro E., ed.), 3rd ICLP, LNCS 225, pp 475–489, Springer Verlag, 1986.
J. W. Lloyd: Foundations of Logic Programming. Springer Verlag, Berlin, 1987.
L. Sterling, E. Y. Shapiro: The Art of Prolog. MIT Press, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Deransart, P. (1989). Proofs of declarative properties of logic programs. In: DĂaz, J., Orejas, F. (eds) TAPSOFT '89. CAAP 1989. Lecture Notes in Computer Science, vol 351. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50939-9_134
Download citation
DOI: https://doi.org/10.1007/3-540-50939-9_134
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50939-4
Online ISBN: 978-3-540-46116-6
eBook Packages: Springer Book Archive