ABSTRACT. We recall a connection made in a recent conference paper between the optimal repair property in knowledge engineering and the unification types unitary and finitary in unification theory. This connection is revealed when looking at repairs and unifiers from an order-theoretic point of view. The paper gives order-theoretic characterizations of the optimal repair property (and thus of unification types unitary or finitary), but also generalizes the optimal repair property to the notion of repair types, in analogy with the definition of unification types. Finally, it shows that (a generalization of) unification can actually be seen as a repair problem.

ABSTRACT. We address the quantitative generalization problem in the variadic nominal language. The language combines variadic (i.e., flexible arity) functions with binding structures and freshness constraints. The quantitative generalization problem is concerned with discovering structural similarities of two input expressions, where proximity of function symbols is specified by a given fuzzy relation. We introduce a novel algorithm to compute quantitative generalizations of two variadic nominal input expressions. It combines techniques for handling variable binding with support for variadic expressions and fuzzy proximity.

ABSTRACT. The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. Most of the results on the unification type of equational theories were shown for the restricted setting. In this extended abstract, we recall our recent results on how the unification type may change when going from the restricted to the unrestricted setting.

ABSTRACT. This paper discusses the proof of completeness of an inference-rule-based procedure for absorptive anti-unification. The procedure transforms an input configuration encoding a problem into a set of configurations from which an abstraction grammar produces generalizers. The completeness statement asserts that the procedure generates a complete set of least general generalizers regarding the class of relevant generalizers, which are generalizers restricted to the language of the input problem.

ABSTRACT. We present a framework for computing special constant-preserving (scp) generalizations in anti-unification (or generalization) modulo equations. Our approach is motivated by interaction composition in distributed systems, where preserving designated constants is crucial for consistent synchronization between partial behaviors. To address this, we extend a rule-based scp generalization algorithm with a variant-based mechanism, enabling reasoning modulo equational theories while enforcing constant-preservation constraints.

ABSTRACT. We present an E-unification procedure for a set of non-ground (dis)equations, along with a dynamic set of ground (dis)equations, and prove its completeness. The ground part is dynamic in the sense that it continually changes. The algorithm saturates the non-ground equations using Superposition modulo the ground theory. We also have an Instantiation rule that matches the left hand side of non-ground (dis)equations with ground terms, creating new ground (dis)equations, which changes the ground theory. This algorithm can be used in quantified SMT problems, where the dynamic ground theory represents the evolving model. We develop an ordering to compare terms modulo a ground theory, which is used to orient non-ground equations. We prove properties of this ordering, using a weak form of monotonicity and subterm property. We finally present a set of inference rules for our ordering, which allows us to properly orient equations in theories of some finite data structures, such as a theory of finite lists with length and append.

ABSTRACT. It is well-known that Boolean unification is unitary with constants, but only finitary with function terms. However, any discriminator theory may be expanded with function terms without loss of unification type provided that they satisfy a certain compatibility condition. We construct an isomorphism between compatibly expanded and nonexpanded Boolean rings, allowing us to reason about compatibly expanded Boolean rings via correspondence. Additionally, we show that the result generalizes to $p$-rings expanded with compatible unary function terms. This additionally shows that the compatible function terms are not injective, even when restricted to terms generated without ring connectives, which renders them unhelpful for many of the applications of general Boolean unification.

ABSTRACT. Matching and unification have been introduced in Description Logic as non-standard reasoning problems with applications in ontology engineering. For the DL EL, it was shown that both problems are NP-complete, but some special cases of matching are tractable. Surprisingly, it turned out that for unification the complexity increases to PSpace if one disallows the use of the top concept to build concept descriptions. However, the effect of disallowing the top concept has not been investigated for matching. We show that a similar increase in complexity applies to matching when the top concept is not allowed.

ABSTRACT. Given a set of equations E, one is often interested in proving (or disproving) E-*validity* of equations s=t, i.e., whether s and t are *equivalent* with respect to E, written s =_E t. Assume that E can be turned into a Term Rewriting System R which is *confluent* and such that the equational theory of E_R, obtained by replacing `->' by `=' in all rules of R, coincides with that of E. Then, s =_E t and R-*joinability* of s and t, i.e., checking whether s ->*_R u and t ->*_R u holds for some term u, coincide. Termination of R is useful to check such joinability: just rewrite s and t until no further reduction is possible to obtain s' and t'; then compare them for syntactic equality. Using term rewriting for proving E-validity with *non-terminating* systems R, though, is underexplored to date. In this paper we show how to use *Context-Sensitive Rewriting* (where only selected arguments of function symbols can be rewritten) to prove and disprove E-validity, even if R is *not* terminating.