Alexander Steen:

Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics

Kurzbeschreibung

Church's Simple Theory of Types (STT), also referred to as classical higher-order logik, is an elegant and expressive formal system built on top of the simply typed λ-calculus. Its mechanisms of explicit binding and quantification over arbitrary sets and functions allow the representation of complex mathematical concepts and formulae in a concise and unambiguous manner. Higher-order automated theorem proving (ATP) has recently made major progress and several sophisticated ATP systems for higher-order logic have been developed, including Satallax, Osabelle/HOL and LEO-II. Still, higher-order theorem proving is not as mature as its first-order counterpart, and robust implementation techniques for efficient data structures are scarce.

In this thesis, a higher-order term representation based upon the polymorphically typed  λ-calculus is presented. This term representation employs spine notation, explicit substitutions and perfect term sharing for efficient term traversal, fast β-normalization and reuse of already  constructed terms, respectively.  An evaluation  of the term representation is performed on the basis of a heterogeneous benchmark set. It shows that while the presented term data structure performs quite well in general, the normalization results indicate that a context dependent choice of reduction strategies is beneficial.

A term indexing data structure for  fast term retrieval based on various low-level criteria is presented and discussed. It supports symbol-based term retrieval, indexing of terms via structural properties, and subterm indexing.

Betreuer
Dr. C. Benzmüller, Prof. Dr. Marcel Kyas
Abschluss
Master of Science (M.Sc.)
Abgabedatum
17.10.2014
Homepage des Autors

Downloads