Given a query, such a program does not simply either terminate or not terminate, but it terminates with a certain probability. Termination of a probabilistic program is not a crisp notion. As far as we know, the termination of probabilistic logical programs has not received any attention in the community so far. Languages like PRISM, CP-Logic, ProbLog, and CHRiSM have been introduced and proved very useful for addressing problems in which a combination of logical and probabilistic reasoning is required. In recent years, probabilistic extensions of Logic Programming languages have become increasingly important. Termination analysis has received considerable attention in Logic Programming for several decades. In Section 3, we report on extensive experimentation with the system and comparison with several other systems. In the next section we describe the approach, comment on the various compo- nents and illustrate them with fragments of a termination proof. We will only present the main intuitions in order to make the paper reasonably self-contained. Space restrictions do not allow us to give a formal account of this theory. The theoretical foundations of Polytool are formulated and proved in (9). More precisely, the system implements the constraint-based approach to termi- nation analysis, presented in (6), but extended to non-linear, polynomial level mappings and norms.
Polytool is based on a termination condition that is rooted on acceptability (2).
This is a direct extension of the well-founded orders based on (semi-)linear level mappings and norms that are used in most of the existing LP termination analysis systems. The aim of Polytool is to extend the power of existing termination analysers by using well-founded orders based on polynomial interpretations. In this system description, we present Polytool, a fully automated system for proving left-termination of denite logic programs (LPs).
0 kommentar(er)
