Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

ICLP

1997

Springer

1997

Springer

Abstract This paper describes a general framework for automatic termination analysis of logic programs, where we understand by termination" the niteness of the LD-tree constructed for the program and a given query. A general property of mappings from a certain subset of the branches of an in nite LD-tree into a nite set is proved. From this result several termination theorems are derived, by using di erent nite sets. The rst two are formulated for the predicate dependency and atom dependency graphs. Then a general result for the case of the query-mapping pairs relevant to a program is proved cf. 29,21 . The correctness of the TermiLog system described in 22 follows from it. In this system it is not possible to prove terminationfor programsinvolvingarithmetic predicates, since the usual order for the integers is not well-founded. A new method, which can be easily incorporated in TermiLog or similar systems, is presented, which makes it possible to prove termination for programs i...

Related Content

Added |
08 Aug 2010 |

Updated |
08 Aug 2010 |

Type |
Conference |

Year |
1997 |

Where |
ICLP |

Authors |
Naomi Lindenstrauss, Yehoshua Sagiv |

Comments (0)