  Computational cognitive modeling investigates human cognition by building
detailed computational models for cognitive processes. Adaptive Control of
Thought - Rational (ACT-R) is a rule-based cognitive architecture that offers a
widely employed framework to build such models. There is a sound and complete
embedding of ACT-R in Constraint Handling Rules (CHR). Therefore analysis
techniques from CHR can be used to reason about computational properties of
ACT-R models. For example, confluence is the property that a program yields the
same result for the same input regardless of the rules that are applied.
  In ACT-R models, there are often cognitive processes that should always yield
the same result while others e.g. implement strategies to solve a problem that
could yield different results. In this paper, a decidable confluence criterion
for ACT-R is presented. It allows to identify ACT-R rules that are not
confluent. Thereby, the modeler can check if his model has the desired
behavior.
  The sound and complete translation of ACT-R to CHR from prior work is used to
come up with a suitable invariant-based confluence criterion from the CHR
literature. Proper invariants for translated ACT-R models are identified and
proven to be decidable. The presented method coincides with confluence of the
original ACT-R models.
