The Syntakker Project

This will be the web page of the Syntakker project. Aim of the project is the research and implementation of an efficient data structure to represent higher order logic. Key features of the system to be implemented will be Term Sharing and Term indexing.

Our main interest is the adaption of structural term indexing techniques (such as path indexing) to representations of higher order logic. While these techniques are well understood for first order logic, there are few comparable approaches for higher order logic. Our aim is to understand the impact of higher order features to those techniques and find ways to adapt them.

Term Indexing for the LEO-II Prover
F. Theiß, C. Benzmüller
6th International Workshop on the Implementation of Logics, 2006

Have a look at:

or mail me: