Recurrence with affine level mappings is P-time decidable for CLP(R)

2007/01/12 by Fred Mesnard, Frédéric Mesnard, Alexander Serebrenik +2
Computer Science · #D.1.6 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.LO #cs.PL

paper · pdf · doi:10.48550/arxiv.cs/0701082

To appear in Theory and Practice of Logic Programming (TPLP)

arxiv created 2007/01/12 · openalex publication_date 2007/01/12 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

In this paper we introduce a class of constraint logic programs such that their termination can be proved by using affine level mappings. We show that membership to this class is decidable in polynomial time.

Related

• Separating LREC from LFP
• On the Termination of Linear and Affine Programs over the Integers
• Bounded Termination of Monotonicity-Constraint Transition Systems
• The 2-Dimensional Constraint Loop Problem is Decidable
• Termination of Linear Programs with Nonlinear Constraints