Higher-Order Pattern Unification Modulo Similarity Relations
This addresses the challenge of decision-making tasks involving abstract functions and predicates where exact matches are rare, though it is incremental as it integrates existing components.
The paper tackled the problem of efficiently reasoning with higher-order theories and fuzzy logic by proposing a unification algorithm for higher-order patterns modulo similarity relations based on minimum T-norm, proving its termination, soundness, and completeness, and showing it computes a most general unifier with the highest degree of approximation.
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.