Available on ORBilu since
02 March 2020
Bachelor/master dissertation (Dissertations and theses)
Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics
Steen, Alexander


Full Text
Author postprint (2.51 MB)

All documents in ORBilu are protected by a user license.

Send to


Keywords :
Automated Theorem Proving; Data structures; Higher-Order Logic
Abstract :
[en] 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.
Disciplines :
Computer science
Author, co-author :
Steen, Alexander ;  University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Language :
Title :
Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics
Defense date :
22 October 2014
Number of pages :
Institution :
FU Berlin - Freie Universität Berlin, Berlin, Germany
Degree :
Master in Computer Science (M.Sc.)
Promotor :
Benzmüller, Christoph
Jury member :
Kyas, Marcel


Number of views
53 (1 by Unilu)
Number of downloads
26 (0 by Unilu)


Similar publications

Contact ORBilu