DocumentCode
2287419
Title
Proving termination properties of Prolog programs: a semantic approach
Author
Baudinet, Marianne
Author_Institution
Dept. of Comput. Sci., Stanford Univ., CA, USA
fYear
1988
fDate
0-0 1988
Firstpage
336
Lastpage
347
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/LICS.1988.5131
Filename
5131
Link To Document