17 citations · 46 across the 16 of their papers we have counts for
10 papers · 1 filter
Anti-Unification Completeness Analysis in PVS
Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima +2
In syntactic anti-unification, one is concerned with finding the commonalities between terms, while (uniformly) abstracting their differences. The original goal of anti-unification…
Generalization of Variadic Structures with Binders: A Tool for Structural Code Comparison
Alexander Baumgartner, Temur Kutsia
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…
Graded Quantitative Narrowing
Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Georg Ehling +1
The recently introduced framework of Graded Quantitative Rewriting is an innovative extension of traditional rewriting systems, in which rules are annotated with degrees drawn from…
Nominal anti-unification
Alexander Baumgartner, Temur Kutsia, Jordi Levy +1
We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general…
Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories
Daniele Nantes-Sobrinho, Manfred Schmidt-Schauss, Alexander Baumgartner +1
Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints…
Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
Temur Kutsia, Daniel Ventura, David Monniaux +1
This volume contains * The post-proceedings of the Eighteenth Logical and Semantic Frameworks with Applications (LSFA 2023). The meeting was held on July 1-2, 2023, organised by th…
Equational Anti-Unification over Absorption Theories
Mauricio Ayala-Rincon, David M. Cerna, Andres Felipe Gonzalez Barragan +1
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-unifica…
Anti-unification and Generalization: A Survey
David M. Cerna, Temur Kutsia
Anti-unification (AU) is a fundamental operation for generalization computation used for inductive inference. It is the dual operation to unification, an operation at the foundatio…
Nominal Unification and Matching of Higher Order Expressions with Recursive Let
Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy +2
A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also…
Higher-Order Equational Pattern Anti-Unification [Preprint]
David M. Cerna, Temur Kutsia
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…