认知结构ACT-R的操作语义及其约束处理规则的转换
An Operational Semantics for the Cognitive Architecture ACT-R and its Translation to Constraint Handling Rules
摘要：
计算心理学的目标是通过认知过程的计算模型来解释人类的认知。认知架构ACT-R是流行的开发这样的模型。虽然ACT-R有一个定义良好的心理学理论，并已被用来解释许多认知过程，有两个问题，使它很难正式推理的认知模型：首先，ACT-R缺乏一个形式化的底层产生式规则系统，其次，有许多不同的实现和扩展的ACT-R的技术工件复杂的形式推理。本文描述了一个正式的操作语义-非常抽象的语义-抽象尽可能多的技术细节，保持开放的扩展和不同的实现的ACT-R理论。在第二步中，此语义被细化以定义其在ACT-R的许多实现中发现的一些抽象特征-抽象语义。它集中在ACT-R的程序核心，适合于分析过渡系统，因为它仍然抽象的细节，如时间，子符号层或冲突解决。此外，定义了ACT-R模型到程序设计语言约束处理规则（Constraint Handling Rules，简称CSTR）的翻译。这使得抽象语义成为ACT-R的可执行规范。它已成功地用于嵌入其他基于规则的形式主义，如图转换系统或函数式编程。有许多结果和工具，支持形式化推理和分析的可重构程序。将ACT-R模型转换为XML已被证明是可靠和完整的。ACT-R的抽象操作语义。这为通过CHR分析ACT-R模型铺平了道路。因此，据我们所知，我们的抽象语义是第一个适合分析和执行的ACT-R公式。
英文摘要：
Computational psychology has the aim to explain human cognition by computational models of cognitive processes. The cognitive architecture ACT-R is popular to develop such models. Although ACT-R has a well-defined psychological theory and has been used to explain many cognitive processes, there are two problems that make it hard to reason formally about its cognitive models: First, ACT-R lacks a formalization of its underlying production rule system and secondly, there are many different implementations and extensions of ACT-R with technical artifacts complicating formal reasoning even more. This paper describes a formal operational semantics - the very abstract semantics - that abstracts from as many technical details as possible keeping it open to extensions and different implementations of the ACT-R theory. In a second step, this semantics is refined to define some of its abstract features that are found in many implementations of ACT-R - the abstract semantics. It concentrates on the procedural core of ACT-R and is suitable for analysis of the transition system since it still abstracts from details like timing, the sub-symbolic layer or conflict resolution. Furthermore, a translation of ACT-R models to the programming language Constraint Handling Rules (CHR) is defined. This makes the abstract semantics an executable specification of ACT-R. CHR has been used successfully to embed other rule-based formalisms like graph transformation systems or functional programming. There are many results and tools that support formal reasoning about and analysis of CHR programs. The translation of ACT-R models to CHR is proven sound and complete w.r.t. the abstract operational semantics of ACT-R. This paves the way to analysis of ACT-R models through CHR. Therefore, to the best of our knowledge, our abstract semantics is the first formulation of ACT-R suitable for both analysis and execution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
