Login Logged in as anonymous / My BiBiServ / Logout
Navigation
TALP
Welcome
Download
References
Authors: E. Ohlebusch, C. Claves

The BiBiServ team discontinued the online service for TALP. TALP doesn't run on our current server environment anymore due to a new hardware architecture / OS upgrade.

TALP is a tool that can generate termination proofs for logic programs automatically. It transforms a well-moded logic program into a term rewriting system (TRS) such that termination of the TRS implies termination of the logic program under Prolog's selection rule. It uses the CiME system for proving termination of the generated TRS.


Talp (Talpa europaea)

In the last decade, the automatic termination analysis of logic programs has been receiving increasing attention. Among other methods, techniques have been proposed that transform a well-moded logic program into a TRS so that termination of the TRS implies termination of the logic program under Prolog's selection rule. In [OHL:CLA:MAR:1999] it has been shown that the two-stage transformation obtained by combining the transformations of Ganzinger and Waldmann [GAN:WAL:1993] into deterministic conditional TRSs with a further transformation into TRSs (first described by Chtourou and Rusinowitch in an unpublished manuscript) yields the transformation proposed by Arts and Zantema [ART:ZAN:1996], and that these three transformations are equally powerful. In most cases simplification orderings are not sufficient to prove termination of the TRSs obtained by the two-stage transformation. However, if one uses the dependency pair method [ART:GIE:2000] of Arts and Giesl in combination with polynomial interpretations instead, then most of the examples described in the literature can automatically be proven terminating.

Based on these findings, we have implemented a tool for proving termination of logic programs automatically. This tool consists of a front-end which implements the two-stage transformation and a back-end, the CiME system, for proving termination of the generated TRS. Experiments show that our tool can compete with other tools (e.g. TermiLog or TerminWeb) based on sophisticated norm-based approaches.


Users of TALP are requested to cite :
Ohlebusch, Enno and Claves, Claus and Marche, Claude Transforming conditional rewrite systems with extra variables into unconditional systems, Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning, volume 1705 of Lecture Notes in Artificial Intelligence, pages 111-130, Berlin, Springer-Verlag, 1999
built on June 10 2015 (0:c7a00060b53b)