TY  - UNPD
A1  - Schmidt-Schauß, Manfred
A1  - Kutsia, Temur
A1  - Levy, Jordi
A1  - Villaret, Mateu
A1  - Kutz, Yunus
T1  - Nominal unification of higher order expressions with recursive let
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 62
N2  - A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. As extension a nominal unification algorithm for higher-order expressions with recursive let and atom-variables is constructed, where we show that it also runs in non-deterministic polynomial time.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 62 
Y1  - 2019
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/62000
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-620007
UR  - https://www2.ki.informatik.uni-frankfurt.de/papers/frank/frank-62.pdf
IS  - October 23, 2019
SP  - 1
EP  - 24
PB  - Research group for Artificial Intelligence and Software Technology Institut für Informatik, Fachbereich Informatik und Mathematik, Johann Wolfgang Goethe-Universität
CY  - Frankfurt am Main
ER  -