TY  - UNPD
A1  - Kutz, Yunus
A1  - Schmidt-Schauß, Manfred
T1  - Rewriting with generalized nominal unification
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 63
N2  - We consider matching, rewriting, critical pairs and the Knuth-Bendix confluence test on rewrite rules in a nominal setting extended by atom-variables. Computing critical pairs is done using nominal unification, and rewriting using nominal matching. We utilise atom-variables to formulate rewrite rules, which is an improvement over previous approaches, using usual nominal unification, nominal matching and nominal equivalence of expressions coupled with a freshness constraint. We determine the complexity of several problems in a quantified freshness logic. In particular we show that nominal matching is Πp2-complete. We prove that the adapted Knuth-Bendix confluence test is applicable to a nominal rewrite system with atom-variabes and thus, that there is a decidable test whether confluence of the ground instance of the abstract rewrite system holds. We apply the nominal Knuth Bendix confluence criterion to the theory of monads, and compute a convergent nominal rewrite system modulo alpha-equivalence.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 63 
Y1  - 2019
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/62736
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-627366
UR  - https://www2.ki.informatik.uni-frankfurt.de/papers/frank/frank-63.pdf
IS  - October 23, 2019
SP  - 1
EP  - 21
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  -