Techniques for First-Order Term Indexing in Isabelle/ML

Chair for Logic and Verification

Bachelor Thesis

In recent years, increasingly powerful proof automation has been introduced to interactive theorem provers such as Isabelle. This automation necessitates efficient data structures to index and query sets of terms. So-called term indices provide queries for retrieving variants, instances, generalisations and unifiables of a given term. Two indexing techniques, path indexing and discrimination tree indexing are reviewed. We implement path indexing for first-order terms in Isabelle/ML and adapt it to the more general term indexing interface defined in Isabelle/ML. We further define a unified interface for the path index and the previously implemented discrimination tree index, thereby clearing the way for the implementation of additional term indices in the future. Lastly, we evaluate the performance of path indexing in relation to discrimination tree indexing.

PDF Download

Student: Sebastian Willenbrink

Supervisor: Kevin Kappelmann

Professor: Prof. Tobias Nipkow