标题： 基于相似关系的高阶模式合一 显示英文标题

标题： Higher-Order Pattern Unification Modulo Similarity Relations

摘要： 高阶理论和模糊逻辑的结合在涉及抽象函数和谓词推理的决策任务中可能很有用，其中精确匹配通常很少或不必要的。 为这种组合形式开发高效的推理和计算技术是一个重大挑战。 在本文中，我们采用了一种更直接的方法，旨在整合两个已建立且计算行为良好的组件：一方面是有高阶模式，另一方面是通过基于最小T范数的相似关系表达的模糊等价关系。 我们提出了一个针对这些相似关系的高阶模式统一算法，并证明了其终止性、正确性和完备性。 这个统一问题，像它的清晰对应问题一样，是唯一的。 当给定的项可以统一时，该算法会计算出一个最一般的统一项，具有最高的近似程度。 显示英文摘要

摘要： The combination of higher-order theories and fuzzy logic can be useful in decision-making tasks that involve reasoning across abstract functions and predicates, where exact matches are often rare or unnecessary. Developing efficient reasoning and computational techniques for such a combined formalism presents a significant challenge. In this paper, we adopt a more straightforward approach aiming at integrating two well-established and computationally well-behaved components: higher-order patterns on one side and fuzzy equivalences expressed through similarity relations based on minimum T-norm on the other. We propose a unification algorithm for higher-order patterns modulo these similarity relations and prove its termination, soundness, and completeness. This unification problem, like its crisp counterpart, is unitary. The algorithm computes a most general unifier with the highest degree of approximation when the given terms are unifiable.