| Popis: |
Computational cognitive modeling explores cognition by building detailed computational models for cognitive processes, mechanisms and representations. Currently, computational cognitive modeling architectures as well as the implementations of cognitive models are typically ad-hoc constructs. There are many variants of architectures to support modeling for a certain domain. The architectures lack a formalization from the computer science point of view. This impedes analysis of the underlying languages and the programmed models. In this work, we present how cognitive models in the popular cognitive architecture Adaptive Control of Thought - Rational (ACT-R) can be formalized and analyzed with the help of formal methods that come from the field of logic programming. In particular, analysis methods of the declarative programming language Constraint Handling Rules (CHR) are used and extended, such that ACT-R models can be analyzed. Our work contains the following contributions: An abstract operational semantics of ACT-R has been formalized that allows for specifying different implementations by creating instances of the abstract formulation. For instance, the abstract semantics generalizes the conflict resolution mechanism, i.e. the rule choice of the procedural system of ACT-R, by introducing non-determinism on the rule choices. To allow for formal analysis, a sound and complete translation of ACT-R models to CHR has been developed. Due to the strong relation of CHR to formal logic, the translation is suitable for analysis. The analysis methods of CHR have to be extended to analyze ACT-R models. By introducing user-defined equivalence relations on states, the confluence condition can be relaxed such that translated ACT-R states can be considered. We have proposed a criterion for confluence modulo equivalence and operational equivalence modulo equivalence for CHR that can also be used in the context of ACT-R models. A necessary and sufficient confluence criterion for ACT-R models has been formulated that is based on our translation to CHR and the extended analysis methods. |
