[Dundua]
Higher-Order Pattern Unification Modulo Similarity Relations
Besik Dundua, Temur Kutsia
Technical report no. 25-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). February 2025. Licensed under CC BY 4.0 International. [doi] [pdf]@techreport{RISC7141,
author = {Besik Dundua and Temur Kutsia},
title = {{Higher-Order Pattern Unification Modulo Similarity Relations}},
language = {english},
abstract = {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-behaving 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 the most general unifier with the highest degree of approximation when the given terms are unifiable.},
number = {25-03},
year = {2025},
month = {February},
keywords = {Unification, higher-order patterns, fuzzy similarity relations},
length = {20},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
author = {Besik Dundua and Temur Kutsia},
title = {{Higher-Order Pattern Unification Modulo Similarity Relations}},
language = {english},
abstract = {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-behaving 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 the most general unifier with the highest degree of approximation when the given terms are unifiable.},
number = {25-03},
year = {2025},
month = {February},
keywords = {Unification, higher-order patterns, fuzzy similarity relations},
length = {20},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}