Unificati on is concerned with the problem of identifying gi ven (first- or higher-order) terms, either syntact ically or modulo a theory. It is a fundamental tec hnique that is employed in various areas of Comput er Science and Mathematics. In particular, unifica tion algorithms are key components in completion o f term rewriting systems, resolution-based theorem proving, and logic programming. But unification i s, for example, also investigated in the context o f natural language processing, program analysis, t ypes, modal logics, and in knowledge representatio n.
\n\nUNIF 2021 is the 35th in a series o f annual workshops on unification and related topi cs. Just as it predecessors', the purpose of UNIF 2021 is to bring together researchers interested i n unification theory and its applications, as well as closely related topics, such as matching (i.e. , one-sided unification), anti-unification (i.e., the dual problem to unification), disunification ( i.e., solving equations and inequations) and the a dmissibility problem (which generalizes unificatio n in modal logics). It will provide a forum for pr esenting recent (even unfinished) work, and discus s new ideas and trends in this and related fields. UNIF 2021 is associated with FSCD 2021 and will b e a purely virtual event.
\nF ollowing the tradition of UNIF, we call for submis sions of extended abstracts (5 pages) in EasyChair style. Topics of interest of the workshop include syntactic and equational unification algorithms, matching and constraint solving, unification in mo dal, temporal, and description logics, higher-orde r unification, narrowing, disunification, anti-uni fication, complexity issues, combination methods, implementation techniques, and applications. We al so allow submission of work presented/submitted in /to another conference.
\n