English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

There are two kinds of approaches for termination analysis of logic programs:"transformational" and "direct" ones. Direct approaches prove terminationdirectly on the basis of the logic program. Transformational approachestransform a logic program into a term rewrite system (TRS) and then analyzetermination of the resulting TRS instead. Thus, transformational approachesmake all methods previously developed for TRSs available for logic programs aswell. However, the applicability of most existing transformations is quiterestricted, as they can only be used for certain subclasses of logic programs.(Most of them are restricted to well-moded programs.) In this paper we improvethese transformations such that they become applicable for any definite logicprogram. To simulate the behavior of logic programs by TRSs, we slightly modifythe notion of rewriting by permitting infinite terms. We show that ourtransformation results in TRSs which are indeed suitable for automatedtermination analysis. In contrast to most other methods for termination oflogic programs, our technique is also sound for logic programming without occurcheck, which is typically used in practice. We implemented our approach in thetermination prover AProVE and successfully evaluated it on a large collectionof examples.

Automated Termination Proofs for Logic Programs by Term Rewriting