Abstract
The combination of higher-order theories and fuzzy logic can be useful indecision-making tasks that involve reasoning across abstract functions andpredicates, where exact matches are often rare or unnecessary. Developingefficient reasoning and computational techniques for such a combined formalismpresents a significant challenge. In this paper, we adopt a morestraightforward approach aiming at integrating two well-established andcomputationally well-behaved components: higher-order patterns on one side andfuzzy equivalences expressed through similarity relations based on minimumT-norm on the other. We propose a unification algorithm for higher-orderpatterns modulo these similarity relations and prove its termination,soundness, and completeness. This unification problem, like its crispcounterpart, is unitary. The algorithm computes a most general unifier with thehighest degree of approximation when the given terms are unifiable.