Higher-Order Pattern Unification Modulo Similarity Relations
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Decision MakingSimilar Papers 제목 키워드 기반
Implementing Anti-Unification Modulo Equational Theory
We present an implementation of E-anti-unification as defined in Heinz (1995), where tree-grammar descriptions of equivalence classes of terms are used to compute generalizations modulo equational theories. We discuss se…
LEMMAHigher order PCA-like rotation-invariant features for detailed shape descriptors modulo rotation
PCA can be used for rotation invariant features, describing a shape with its $p_{ab}=E[(x_i-E[x_a])(x_b-E[x_b])]$ covariance matrix approximating shape by ellipsoid, allowing for rotation invariants like its traces of po…
Scene UnderstandingObject RecognitionThe IFF Foundation for Ontological Knowledge Organization
This paper discusses an axiomatic approach for the integration of ontologies, an approach that extends to first order logic a previous approach (Kent 2000) based on information flow. This axiomatic approach is represente…
Nominal Unification and Matching of Higher Order Expressions with Recursive Let
A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal let…
Superposition with Delayed Unification
Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferenc…