Symbolic constraints and quantitative extensions of equality

by Temur Kutsia, Johannes Kepler University, Austria


Symbolic constraint solving is ubiquitous in many areas of mathematics and computer science. Unification, matching, anti-unification, disunification, and ordering constraints are some prominent examples that play an important role in automated reasoning, term rewriting, declarative programming, and their applications. In this talk, we present recent advances in solving unification and anti-unification constraints in theories where equality is replaced by its quantitative approximation. Such problems arise in working with imprecise information requiring results “within tolerance”. Examples include fuzzy proximity and similarity relations, multi-valued logics, quantitative algebras.
Our algorithms solve unification and anti-unification problems modulo crisp and fuzzy tolerance (i.e., reflexive and symmetric) relations where mismatches between symbol names/arities are permitted, as well as modulo multiple similarity relations. We will discuss general principles behind these techniques, show examples, present some of the algorithms, and characterize their properties.