Abstract
In the logic programming community, the concept of interargument relation, that is, the relation that holds between the size of the arguments of a procedure, appears in numerous works on termination proofs for logic programs. In this paper, we present a method for proving linear interargument inequalities. Our technique relies on the notion of abstract procedures and on CLP({ie308-02}). We prove its correctness and fully describe its implementation in Prolog III. The applications we present go beyond termination proofs and demonstrate its usefulness.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.N. Bol: Toward More Efficient Loop Checks. In Proc. of NACLP'90, pp. 465–479, 1990.
D.R. Brough, A. Walker: Some practical properties of logic programming interpreters. In Proc. of FGCS'84, pp. 149–156, 1984.
J. Cohen: Constraint Logic Programming Language. In CACM, vol. 33, n∘7, pp. 54–68, July 1990.
A. Colmerauer: An introduction to Prolog III. In CACM, vol. 33, n∘7, pp. 70–90, July 1990.
D.C. Cooper: Theorem Proving in arithmetic without multiplication. In Machine Intelligence 7, pp. 91–99, 1972.
P. Cousot, N. Halbwachs: Automatic discovery of linear restraints among variables of a program. In Proc. of the 5th ACM Symposium of the POPL, pp. 84–97, 1987.
[De Schreye et al., 89] D. De Schreye, M. Bruynooghe, K. Versaechtse: On the Existence of Nonterminating Queries for a Restricted Class of PROLOG-Clauses. In Artificial Intelligence 41, pp. 237–248, 1989.
M. Dincbas, P. Van Hentenryck, H. Simonis, A. Aggoun, T. Graf, F. Berthier: The Constraint Logic Programming Language CHIP. In Proc. of FGCS'88, 1988.
J. Jaffar, J-L. Lassez: Constraint logic programming. In Proc. of the 14th ACM Symposium of the POPL, pp. 111–119, 1987.
G. Janssens, M. Bruynooghe: Deriving descriptions of possible values of program variables by means of abstract interpretation. Report CW 107, Dpt of Computer Science, K.U. Leuven, March 1990.
M. Karr: Affine Relationships Among Variables of a Program. In Acta Informatica 6, pp.133–151, 1976.
R.A. Kowalski: Predicate Logic as a Programming Language. In IFIP, pp. 569–574, 1974.
A. Lane: Trilogy: a New Approach to Logic Programming. In Byte, March 1988.
J.W. Lloyd: Foundations of Logic Programming; Springer-Verlag, 1987.
M. Presburger: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. In Comptes-rendus du Ier Congrès des Mathématiciens des Pays Slaves, Warsaw, pp. 92–101,1930.
L. Plümer: Termination Proofs for Logic Programs, LNAI 446, Springer-Verlag, 1990.
J.D. Ullman & A. Van Gelder: Efficient tests for top-down termination of logical rules. In JACM, vol. 35, n∘ 2, pp. 345–373, April 1988.
A. Van Gelder: Deriving Constraints Among Arguments Sizes on Logic Programs. In Proc. of the 9th Symp. of the PODS, pp. 47–60, 1990.
T. Vasak & J. Potter: Characterisation of terminating logic programs. In Proc. of SLP'86, pp. 140–147, 1986
K. Verschaetse & D. De Schreye: Deriving Termination Proofs for Logic Programs, using Abstract Procedures. In Proc. of the 8th ICLP, pp. 301–315, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mesnard, F., Ganascia, J.G. (1992). CLP({ie308-01}) for proving interargument relations. In: Pettorossi, A. (eds) Meta-Programming in Logic. META 1992. Lecture Notes in Computer Science, vol 649. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56282-6_21
Download citation
DOI: https://doi.org/10.1007/3-540-56282-6_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56282-5
Online ISBN: 978-3-540-47505-7
eBook Packages: Springer Book Archive