Solving Quantitative Equations
Georg Ehling, Temur Kutsia · Lecture notes in computer science · 2024
Abstract Quantitative equational reasoning provides a framework that extends equality to an abstract notion of proximity by endowing equations with an element of a quantale. In this paper, we discuss the unification problem for a special class of shallow subterm-collapse-free quantitative equational theories. We outline rule-based algorithms for solving such equational unification problems over generic as well as idempotent Lawvereian quantales and study their properties.