JetBrains Research unites scientists working in challenging new disciplines

Source-Tracking Unification via Context-Free Path Querying

The unification problem is to find a substitution which, being applied to terms, makes them equal. Unification is an integral part of logic programming, type checking and automated theorem provers. Syntactic unification can be expressed as a context-free path querying problem. A path in the graph can serve as a proof that terms can be unified. In the talk we will discuss how to construct a graph for a unification problem, what language can be used as constraints and how to prove that terms can be unified.

Speaker: Ekaterina Verbitskaia


Choppella, Venkatesh, and Christopher T. Haynes. "Source-tracking unification." Information and Computation 201, no. 2 (2005): 121-159.

The seminar will be held in google meet on Monday, November 16, at 17:30 (google meet room: