Rewriting logic is a logical framework for expressing both concurrent computation and logical deduction using equations and rewrite rules. Quantitative equational reasoning enriches equations with quantitative measures, expressing concepts such as similarity or proximity rather than mere equality of terms. In this article, we bring these two approaches together and propose a quantitative extension of rewriting logic as a flexible formalism for quantitative deduction and computation.

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.