Logic in Computer Science (LICS 1988)

Paper: Proving termination properties of Prolog programs: a semantic approach (at LICS 1988)

Authors: Marianne Baudinet

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

BibTeX

  @InProceedings{Baudinet-Provingterminationp,
    author = 	 {Marianne Baudinet},
    title = 	 {Proving termination properties of Prolog programs: a semantic approach },
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {336--347},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }