| Reference : Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics |
| Dissertations and theses : Bachelor/master dissertation | |||
| Engineering, computing & technology : Computer science | |||
| http://hdl.handle.net/10993/42694 | |||
| Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics | |
| English | |
Steen, Alexander  [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >] | |
| 22-Oct-2014 | |
| Freie Universität Berlin, Berlin, Germany | |
| Master in Computer Science (M.Sc.) | |
| 82 | |
| Benzmüller, Christoph | |
| Kyas, Marcel | |
| [en] Automated Theorem Proving ; Data structures ; Higher-Order Logic | |
| [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. | |
| Researchers | |
| http://hdl.handle.net/10993/42694 | |
| http://www.mi.fu-berlin.de/inf/groups/ag-ki/Theses/Completed-theses/Master_Diploma-theses/2014/Steen/index.html |
| File(s) associated to this reference | ||||||||||||||
|
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.
