Decidability properties for fragments of CHR

DOI10.1017/S1471068410000311MaRDI QIDQ3585171zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Maurizio Gabbrielli, Jacopo Mauro, Maria Chiara Meo, Jon Sneyers

Publication date 19 August 2010

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

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

zbMATH Keywords

constraint programmingexpressivitywell-structured transition systems

Mathematics Subject Classification ID

Logic programming (68N17) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity >0). Both languages allow the use of the = built-in in the body of rules, thus are built on a host language that supports unification. However each imposes one further restriction. The first CHR dialect allows only range-restricted rules, that is, it does not allow the use of variables in the body or in the guard of a rule if they do not appear in the head. We show that the existence of an infinite computation is decidable for this dialect. The second dialect instead limits the number of atoms in the head of rules to one. We prove that in this case, the existence of a terminating computation is decidable. These results show that both dialects are strictly less expressive than Turing Machines. It is worth noting that the language (without function symbols) without these restrictions is as expressive as Turing Machines.

Recommendations

• Decidable and undecidable fragments of first-order concatenation theory
• Decidable fragments of many-sorted logic
• Decidable Fragments of Many-Sorted Logic
• scientific article; zbMATH DE number 4016859
• Publication:4938629
• Turing-Complete Subclasses of CHR
• A decidable fragment of predicate calculus
• On the fragmentary complexity of symbolic sequences
• A Decidable Fragment of Recursive Arithmetic
• Solvable (and unsolvable) cases of the decision problem for fragments of analysis

Cites work

• A timed concurrent constraint language.
• As time goes by: constraint handling rules
• Constraint Handling Rules
• Well-structured transition systems everywhere!

This page was built for publication: Decidability properties for fragments of CHR

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