We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules, where both kinds of rules are defined using the type-theoretic concept of object-invertible rules. We also give sufficient syntactic criteria for recognizing such rules, as well as a simple pattern-matching algorithm for applying them. A third component of the algorithm is a suitable notion of principal arguments, which determines a notion of normal form. By varying these, we obtain known notions, such as weak head-normal and strong normal forms. We prove that our algorithm is sound. We implemented it in the Andromeda 2 proof assistant, which supports user-definable type theories. The user need only provide the equality rules they wish to use, which the algorithm automatically classifies as computation or extensionality rules, and select appropriate principal arguments.

翻译：我们提出了一个适用于大类理论的通用和用户可扩展的平等检查算法。算法有一个适用于大类理论的通用和用户扩展的平等检查算法。算法有一个用于应用扩展规则和基于计算规则的正常化阶段,其中两种规则都使用物体不可翻转规则的类型理论概念来定义。我们还提供了承认这些规则的充分综合标准,以及应用这些规则的简单模式匹配算法。算法的第三个组成部分是一个合适的主要参数概念,它决定着一种正常形式的概念。我们通过这些不同的概念获得已知的概念,例如弱头常态和强势的正常形式。我们证明我们的算法是健全的。我们在支持用户可定义型号理论的安卓美达2号验证助手中执行了它。用户只需要提供他们希望使用的平等规则,而算法则自动归类为计算规则或扩展规则,并选择适当的主要参数。