Non-termination analysis of logic programs with integer arithmetics

DOI10.1017/S1471068411000159zbMATH Open1222.68068arXiv1109.3256OpenAlexW3099640838MaRDI QIDQ3087440FDOQ3087440

Authors: Dean Voets, Danny De Schreye 

Publication date: 16 August 2011

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Abstract: In the past years, analyzers have been introduced to detect classes of non-terminating queries for definite logic programs. Although these non-termination analyzers have shown to be rather precise, their applicability on real-life Prolog programs is limited because most Prolog programs use non-logical features. As a first step towards the analysis of Prolog programs, this paper presents a non-termination condition for Logic Programs containing integer arithmetics. The analyzer is based on our non-termination analyzer presented at ICLP 2009. The analysis starts from a class of queries and infers a subclass of non-terminating ones. In a first phase, we ignore the outcome (success or failure) of the arithmetic operations, assuming success of all arithmetic calls. In a second phase, we characterize successful arithmetic calls as a constraint problem, the solution of which determines the non-terminating queries.

Full work available at URL: https://arxiv.org/abs/1109.3256

Recommendations

• Non-termination Analysis of Logic Programs Using Types
• A new approach to non-termination analysis of logic programs
• A practical analysis of non-termination in large logic programs
• A non-termination criterion for binary constraint logic programs
• A general framework for automatic termination analysis od logic programs

zbMATH Keywords

numerical computationnon-termination analysisconstraint-based approach

Mathematics Subject Classification ID

Logic programming (68N17)

Cites Work

• Title not available (Why is that?)
• Termination of logic programs: the never-ending story
• A dynamic approach to characterizing termination of general logic programs
• Inference of Termination Conditions for Numerical Loops in Prolog
• Polytool: polynomial interpretations as a basis for termination analysis of logic programs
• Termination prediction for general logic programs

Cited In (7)

• A non-termination criterion for binary constraint logic programs
• Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
• A new approach to non-termination analysis of logic programs
• Non-termination Analysis of Logic Programs Using Types
• Terminating evaluation of logic programs with finite three-valued models
• Using linear constraints for logic program termination analysis
• A practical analysis of non-termination in large logic programs

Uses Software

• MiniSat
• AProVE

This page was built for publication: Non-termination analysis of logic programs with integer arithmetics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3087440)