AI 中文总结
研究针对 Prolog 传统无类型的问题，用 Maude 实现类型化合一算法并构建 MaudeTypedLog 解释器，其遵循特定操作语义，能动态检测程序和查询中的类型错误。
AI 中文摘要
传统上，Prolog 被视为无类型逻辑编程语言，尽管存在导致类型错误的查询。已有若干在 Prolog 中静态引入类型规则的尝试，但未被广泛采用。我们用 Maude 实现了一个类型化合一算法，并将其作为名为 MaudeTypedLog 的 Prolog 解释器的基础。该解释器遵循逻辑编程的类型化 SLD 消解操作语义，能够动态检测程序和查询中的类型错误。
英文摘要
Prolog is traditionally thought of as an untyped logic programming language, although there are queries that result in a type error. Several attempts of statically introducing a type discipline in Prolog have been made but they have not been widely adopted. We use Maude to implement a typed unification algorithm and use it as the basis for an interpreter for Prolog called MaudeTypedLog. This interpreter follows the Typed SLD-resolution operational semantics for logic programming, that makes it possible to detect type errors in both programs and queries dynamically.
CommentsIn Proceedings LSFA 2026, arXiv:2607.15904
Journal refEPTCS 449, 2026, pp. 107-122
