hProlog is a high-performance Prolog system for experimental purposes.

hProlog Home Page

We present a new approach to termination analysis of numerical computations in logic programs. Traditional approaches fail to analyse them due to non well-foundedness of the integers. We present a technique that allows overcoming these difficulties. Our approach is based on transforming a program in a way that allows integrating and extending techniques originally developed for analysis of numerical computations in the framework of query-mapping pairs with the well-known framework of acceptability. Such an integration not only contributes to the understanding of termination behaviour of numerical computations, but also allows us to perform a correct analysis of such computations automatically, by extending previous work on a constraint-based approach to termination. Finally, we discuss possible extensions of the technique, including incorporating general term orderings.

• Termination analyser: [web.tar.gz]
• Type inference of Janssens and Bruynooghe used by our system: [aisys.tar.gz]

The K.U.Leuven CHR system is a competitive Constraint Handling Rules system for Prolog, consisting of a compiler and runtime. The system is currently available for hProlog, SWI-Prolog and XSB.

The K.U.Leuven CHR system

The K.U.Leuven JCHR System is a user-friendly, flexible and efficient integration of Constraint Handling Rules and Java.

The K.U.Leuven JCHR system

ViPReSS consists of several Prolog refactoring tools, currently available as VIM scripts for SICStus Prolog.

ViPReSS Home Page

Barvinok is a library for (weighted) counting of integer points in (projections of) parametric polytopes.

Barvinok

...

Polytool

isl is a library for manipulating sets and relations of integer points bounded by linear constraints. Supported operations on sets include intersection, union, set difference, emptiness check, convex hull, (integer) affine hull, integer projection, computing the lexicographic minimum using parametric integer programming, coalescing and parametric vertex enumeration. It also includes an ILP solver based on generalized basis reduction, transitive closures on maps (which may encode infinite graphs), dependence analysis and bounds on piecewise step-polynomials. isl is released under LGPLv2.1

isl