The performance of a theorem prover crucially depends on the speed of the basic retrieval operations, such as finding terms that are unifiable with (instances of, or more general than) a given query term.

The first part of this talk describes an indexing method that allows to represent a set of substitutions in the form of a compact tree data structure.

The second part of this talk discusses theoretical foundations and implementing for several operations to work with this data structure such as retrieval, merge, insertion and deletion.

Supplementary materials:

Peter Graf. Substitution tree indexing // International Conference on Rewriting Techniques and Applications, 1995.

Presenter: Petr Lozov

Date: April 8, 2019

Time: 17:15

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28