Title :
Proving termination properties of Prolog programs: a semantic approach
Author :
Baudinet, Marianne
Author_Institution :
Dept. of Comput. Sci., Stanford Univ., CA, USA
Abstract :
A method for proving termination properties of Prolog programs including program with cuts. Programs are viewed as functions mapping goals into finite or infinite sequences of answer substitutions. Associated with each program is a system of functional equations, the least fixed point of which is the meaning of the program. Various termination or nontermination properties as well as partial correctness statements can then be proved by reasoning with the program equations and using fixpoint or structural induction. The method is amenable to automatic implementation.<>
Keywords :
PROLOG; logic programming; program verification; Prolog programs; answer sequences; answer substitutions; functional equations; partial correctness statements; program equations; program with cuts; structural induction; termination properties; Automatic logic units; Computer science; Contracts; Equations; Lattices; Logic programming;
Conference_Titel :
Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
Conference_Location :
Edinburgh, UK
Print_ISBN :
0-8186-0853-6
DOI :
10.1109/LICS.1988.5131
