English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/159866
logo share SHARE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:


Nominal Anti-Unification

AuthorsBaumgartner, Alexander; Kutsia, Temur; Levy, Jordi ; Villaret, Mateu
Nominal anti-unification
Issue Date29-Jun-2015
PublisherDagstuhl Publishing
Citation26th International Conference on Rewriting Techniques and Applications, RTA 2015. Leibniz International Proceedings in Informatics, LIPIcs V36 (2015): 57-73
AbstractWe 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 solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and α-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems were generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved. © Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret.
Identifiersdoi: 10.4230/LIPIcs.RTA.2015.57
issn: 18688969
isbn: 978-393989785-9
Appears in Collections:(IIIA) Comunicaciones congresos
Files in This Item:
File Description SizeFormat 
LIPIcsV36(2015)_57-73.pdf538,05 kBUnknownView/Open
Show full item record
Review this work

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.