Logo der Freien Universität BerlinFreie Universität Berlin

Fachbereich Mathematik und Informatik


Service-Navigation

  • Startseite
  • Personen
  • Kontakt
Hinweise zur Datenübertragung bei der Google™ Suche
Fachbereich Mathematik und Informatik/Informatik/

Dahlem Center for Machine Learning and Robotics

Menü
  • Members

    loading...

  • Open Positions

    loading...

  • Publications

    loading...

  • Teaching

    loading...

  • Theses

    loading...

  • Projects

    loading...

  • News

    loading...

  • Videos

    loading...

  • FAQs

    loading...

Mikronavigation

  • Startseite
  • Informatik
  • Arbeitsgruppen
  • Dahlem Center for Machine Learning and Robotics
  • Theses
  • Completed theses
  • Master-/Diploma-theses
  • 2014
  • Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics

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
  • Homepage A. Steen

Downloads

  • pdf-Datei
be-digital Pressekonferenz am 07.12.15Mexico Oktober 2015MiG Mexico 2015Finalisten German Open 2014Simulator-Erfinder: Professor Raul Rojas (l.) und David Dormagen von der AG Intelligente Systeme und RobotikMadeInGermany in MexicoThe Tony Sale Award winners 2014: Robert B Garner (L) and  Raul Rojas (R), Nov. 2014Able und BakerCarolo-Cup-Team2014Formalisierung und Automatisierung von Gödels GottesbeweisAutoNOMOS-Team 2011Besuch Senatorin Yzer am 22.03.13Die autonomen Fahrzeuge der AG Intelligente Systeme und RobotikArchaeocopterMulticopterEntwicklung einer Roboterbiene

Dates

spinner

News

spinner

Service-Navigation

  • Startseite
  • Personen
  • Kontakt

Diese Seite

  • Drucken
  • RSS-Feed abonnieren