Shared term data structures represent repeated instances of the same subterm in the proof state only once. In theorem proving, they can contribute to a considerable reduction of matching operations required, and allow furthermore for completely new techniques for certain operations in the proving procedure, such as non-local shared rewriting.

In contrast to naive implementations, terms are not considered as values of a data structure, but as objects, and their syntactical structure is represented by relations over these objects. The resulting data structure is a directed acyclic graph (DAG), which can be implemented, e.g., by a relational database. Some interesting problems in this context are:

• the development of normal forms that allow for unique representations of equivalent terms, especially with respect to βη-equality and α-equivariance
• treatment of free and bound variables, anonymous variables, scope management
• suitable strategies for term indexing