Unification is concerned with the problem of making two given terms equal, either syntactically or modulo an equational theory. It is a fundamental process used in various areas of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, knowledge representation, types, etc.
The International Workshop on Unification (UNIF) is a forum for researchers in unification theory and related fields to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for students, young researchers and scientists working in related areas to get an overview of the current state of the art in unification theory.
Topics of interest of the workshop include, but are not limited to:
- Syntactic and equational unification algorithms
- Matching and constraint solving
- Higher-order unification
- Unification in modal, temporal, and description logics
- Admissibility of inference rules
- Complexity issues
- Combination methods
- Implementation techniques