Extending approximate reasoning to unranked term structures : unification, matching and anti-unification

This thesis introduces new procedures for solving unranked unification, matching and antiunification problems with fuzzy similarity and proximity relations. We extend existing algorithms for unranked terms in such a way that, instead of requiring syntactic equality between symbols, they can also handle both similarity and proximity relations. This allows for the computation of approximate solutions annotated with quantitative degrees reflecting their similarity or closeness. We prove soundness, completeness, and, whenever applicable, termination, showing that the proposed algorithms and procedures behave correctly and exhaustively under the intended semantics. Each procedure is accompanied by small examples that demonstrate its application. Overall, the thesis provides a unified framework for fundamental techniques for reasoning about unranked term structures that goes beyond strict syntactic equality, allowing terms to be related by more general notions such as similarity or proximity.