Name
Title | ||
|---|---|---|
Predicate Inequalities as a Basis for Automated Termination Proofs for Prolog Programs |
Abstract | ||
|---|---|---|
The purpose of this paper is to establish sufficient conditions for the termination of Prolog procedures which can be checked automatically. We consider Horn clauses containing function symbols. The focus is on the question how local variables in the body of recursive procedures can be handled. The idea is to map predicates on linear inequalities which relate the sizes of the terms of solved goals. These inequalities are used to prove termination. A technique for the deduction of valid linear inequalities for predicates is described. |
Year | DOI | Venue |
|---|---|---|
1988 | 10.1007/BFb0026306 | CSL |
Keywords | Field | DocType |
automated termination proofs,prolog programs,predicate inequalities | Discrete mathematics,Horn clause,Computer science,Prolog,Inequality,Mathematical proof,Predicate (grammar),Linear inequality,Recursion,Local variable | Conference |
Volume | ISSN | ISBN |
385 | 0302-9743 | 3-540-51659-X |
Citations | PageRank | References |
0 | 0.34 | 11 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Lutz Plümer | 1 | 141 | 23.12 |