Manuel V. Hermenegildo

Louis Rustenholz, Manuel V. Hermenegildo, Pedro Lopez-Garcia et al.

We present the theory underpinning a complexity analysis tool (under development) that aims at automating tedious parts of the analysis of complex algorithms originating from the field of automated reasoning. Examples are given by super-exponential quantifier elimination procedures in real and integer arithmetics. Our tool implements the following pipeline. * Together with the algorithm to be analysed, the user (expert, e.g. the algorithm designer) can provide key metrics to track, and lemmas to improve the analysis. In pen-and-paper proofs, these correspond to the "non-tedious" and "creative" parts of the complexity analysis, that require human ingenuity. * The second step consists in the extraction of (generalised) recurrence equations. Here, we rely on a novel higher-order abstract interpretation technique, built on the concept of operator semantics. It enables (optimal) abstract compilation of symbolic programs to different kinds of purely numerical recursive representations, such as recurrence equations on interval-valued functions or numerical logic programs. * Finally, our tool solves the recurrence equations. We propose to go beyond the direct usage of computer algebra systems (CAS), and use pre/postfixpoint-based techniques to discover and verify candidate bounds on the solution. This approach makes use, in turn, of recent progress in SMT solvers, and can also be improved by techniques originating in termination analysis research.

Agostino Dovier, Andrea Formisano, Gopal Gupta et al.

Multi-core and highly-connected architectures have become ubiquitous, and this has brought renewed interest in language-based approaches to the exploitation of parallelism. Since its inception, logic programming has been recognized as a programming paradigm with great potential for automated exploitation of parallelism. The comprehensive survey of the first twenty years of research in parallel logic programming, published in 2001, has served since as a fundamental reference to researchers and developers. The contents are quite valid today, but at the same time the field has continued evolving at a fast pace in the years that have followed. Many of these achievements and ongoing research have been driven by the rapid pace of technological innovation, that has led to advances such as very large clusters, the wide diffusion of multi-core processors, the game-changing role of general-purpose graphic processing units, and the ubiquitous adoption of cloud computing. This has been paralleled by significant advances within logic programming, such as tabling, more powerful static analysis and verification, the rapid growth of Answer Set Programming, and in general, more mature implementations and systems. This survey provides a review of the research in parallel logic programming covering the period since 2001, thus providing a natural continuation of the previous survey. The goal of the survey is to serve not only as a reference for researchers and developers of logic programming systems, but also as engaging reading for anyone interested in logic and as a useful source for researchers in parallel systems outside logic programming. Under consideration in Theory and Practice of Logic Programming (TPLP).