Symbolic Techniques for Quantitative Extensions of Equality [SQUEE]

@techreport{RISC7245,
author = {Besik Dundua and Georg Ehling and Santiago Escobar and Maribel Fernández and Temur Kutsia},
title = {{Quantitative Equational Rewriting}},
language = {english},
abstract = {Rewriting logic is a logical framework for expressing both concurrent computation and logical deduction using equations and re-write 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.},
number = {26-09},
year = {2026},
month = {June},
keywords = {Quantitative rewriting, quantitative equational reasoning, quantitative matching},
length = {39},
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)}
}

@techreport{RISC7248,
author = {Silvio Ghilardi and Cleo Pau (Editors)},
title = {{Proceedings of the 40th International Workshop on Unification, UNIF 2026}},
language = {english},
abstract = {This volume contains the extended abstract presented at the 40th edition of the annual international workshop on Unification (UNIF 2026), held on July 24th, 2026. The workshop was a part of the Federated Logic Conference (FLoC 2026), that unites the ten leading international conferences focused on mathematical logic and its applications in computer science, as well as over 30 satellite workshops. FLoC 2026 took place in Lisbon.},
number = {26-10},
year = {2026},
month = {July},
keywords = {unification},
length = {80},
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)}
}

@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)}
}

@techreport{RISC7056,
author = {G. Ehling and T. Kutsia},
title = {{Solving Quantitative Equations}},
language = {english},
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.},
number = {24-03},
year = {2024},
month = {April},
keywords = {quantitative equational reasoning, Lawvereian quantales, equational unification},
length = {23},
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)}
}