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.

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.