TY  - UNPD
A1  - Schmidt-Schauß, Manfred
A1  - Sabel, David
T1  - Nominal unification with atom and context variables
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 59
N2  - Automated deduction in higher-order program calculi, where properties of transformation rules are demanded, or confluence or other equational properties are requested, can often be done by syntactically computing overlaps (critical pairs) of reduction rules and transformation rules. Since higher-order calculi have alpha-equivalence as fundamental equivalence, the reasoning procedure must deal with it. We define ASD1-unification problems, which are higher-order equational unification problems employing variables for atoms, expressions and contexts, with additional distinct-variable constraints, and which have to be solved w.r.t. alpha-equivalence. Our proposal is to extend nominal unification to solve these unification problems. We succeeded in constructing the nominal unification algorithm NomUnifyASC. We show that NomUnifyASC is sound and complete for these problem class, and outputs a set of unifiers with constraints in nondeterministic polynomial time if the final constraints are satisfiable. We also show that solvability of the output constraints can be decided in NEXPTIME, and for a fixed number of context-variables in NP time. For terms without context-variables and atom-variables, NomUnifyASC runs in polynomial time, is unitary, and extends the classical problem by permitting distinct-variable constraints.
1998 ACM Subject Classification F.4.1 Mathematical Logic
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 59 
KW  - automated deduction
KW  - nominal unification
KW  - lambda calculus
KW  - functional programming
Y1  - 2018
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/45276
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-452767
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/frank/
PB  - Institut für Informatik, Fachbereich Mathematik und Informatik Goethe-Universität Frankfurt am Main, Germany
CY  - Frankfurt am Main
ER  -