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.
展开▼
