将高阶模式与模糊等价关系结合，实现更灵活的逻辑推理。
Higher-Order Pattern Unification Modulo Similarity Relations
- 基于最小T-范数的相似关系，设计高阶模式统一算法
- 证明算法终止、正确且完备，可求出最通用近似解
- 适合处理抽象函数推理中的模糊匹配问题
高阶理论与模糊逻辑的结合在涉及抽象函数和谓词推理的决策任务中具有应用价值，其中精确匹配往往罕见或非必需。本文提出一种融合两个成熟计算框架的方法：一侧为高阶模式，另一侧为基于最小T-范数的相似关系表达的模糊等价。我们设计了在该相似关系下高阶模式的统一算法，并证明其终止性、正确性和完备性。该统一问题如其精确版本一样具有唯一性，当给定项可统一时，算法能计算出具有最高逼近度的最通用统一式。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。