Related papers: Variant-based Equational Unification under Constru…
Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. Equational unification is of special relevance to automated deduction, theorem…
We consider the problem of the unification modulo an equational theory ACh, which consists of a function symbol $h$ that is homomorphic over an associative-commutative operator $+$. Since the unification modulo ACh theory is undecidable, we…
A variety is a class of algebraic structures axiomatized by a set of equations. An equation is linear if there is at most one occurrence of an operation symbol on each side. We show that a variety axiomatized by linear equations has the…
We present a generalization of first-order unification to a term algebra where variable indexing is part of the object language. We exploit variable indexing by associating some sequences of variables ($X_0,\ X_1,\ X_2,\dots$) with a…
This paper introduces a novel anti-unification algorithm for the generalization of variadic structures with binders, designed as a flexible tool for structural code comparison. By combining nominal techniques for handling variable binding…
This paper introduces GLINTS, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including order-sorted equational…
A method for selecting solution constructors in narrowing is presented. The method is based on a sort discipline that describes regular sets of ground constructor terms as sorts. It is extended to cope with regular sets of ground…
In this work, we propose a class of equational theories for bounded binary circuits that have the finite variant property. These theories could serve as a building block to specify cryptographic primitive implementations and automatically…
This paper addresses the problem of checking invariant properties for a large class of symbolic transition systems, defined by a combination of SMT theories and quantifiers. State variables can be functions from an uninterpreted sort…
We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the…
The graph programming language GP 2 allows to apply sets of rule schemata (or "attributed" rules) non-deterministically. To analyse conflicts of programs statically, graphs labelled with expressions are overlayed to construct critical pairs…
In this paper we describe how to leverage higher-order unification to type check a dependently typed language with meta-variables. The literature usually presents the unification algorithm as a standalone component, however the need to…
This paper studies the unification problem with associative, commutative, and associative-commutative functions mainly from a viewpoint of the parameterized complexity on the number of variables. It is shown that both associative and…
Given a text and a pattern over two types of symbols called constants and variables, the parameterized pattern matching problem is to find all occurrences of substrings of the text that the pattern matches by substituting a variable in the…
We show that the question whether a term is typable is decidable for type systems combining inclusion polymorphism with parametric polymorphism provided the type constructors are at most unary. To prove this result we first reduce the…
For a polynomial with palindromic coefficients, unimodality is equivalent to having a nonnegative $g$-vector. A sufficient condition for unimodality is having a nonnegative $\gamma$-vector, though one can have negative entries in the…
Here we define a new unification algorithm for terms interpreted in semantic domains denoted by a subclass of regular types here called deterministic regular types. This reflects our intention not to handle the semantic universe as a…
We investigate unification problems related to the Cipher Block Chaining (CBC) mode of encryption. We first model chaining in terms of a simple, convergent, rewrite system over a signature with two disjoint sorts: list and element. By…
Bounded model finding is a key technique for validating software designs, usually obtained by translating high-level specifications into SAT/SMT problems. Although effective, such translations introduce a semantic gap and a dependency on…
Interest in anti-unification, the dual problem of unification, is on the rise due to applications within the field of software analysis and related areas. For example, anti-unification-based techniques have found uses within clone detection…