Saarland University
Programming Systems
Xin Zhang

Bachelor's thesis task description

Using LEO-II to Prove Properties of an Explicit Substitution M-set Model

Context. LEO-II is an extensional higher-order theorem prover based on resolution. In principle one should be able to formulate mathematical results in higher-order logic and have LEO help find proofs of the results. In this project, we consider a particular mathematical domain: an M-set model of elementary type theory. The lambda sigma-calculus of explicit substitutions induces a monoid M of explicit substitutions and an M-set of terms. This can be used to construct a model of elementary type theory in which one can interpret higher-order abstract syntax. Within this domain, we explore the effectiveness of using LEO to help find proofs. For example, we will attempt to use LEO to prove soundness of axioms for higher-order abstract syntax in the M-set model.

Task description. In this project we will experiment with using the higher-order theorem prover LEO-II to verify properties of the M-set model. The concrete tasks will include the following:

  • Several constants, definitions, axioms, and theorems have already been formulated in hotptp (higher-order TPTP) syntax. Some of these are theorems that we would like to prove using LEO. Each of the theorems can either be proven assuming every fact that has already been given (a ``global'' theorem) or using only some of the (human-selected) facts that have been given (a ``local'' theorem). Part of the project involves selecting the appropriate facts for a local version of each theorem.
  • Some of the theorems will likely require intermediate lemmas to be formulated before the theorem can be proven automatically. These lemmas should also be automatically proven. We can evaluate LEO based on how many intermediate lemmas are required in each case.
  • Thesis
    Slides for Final Talk (October 27, 2008)
    gzipped tar file of directory of problems for LEO

    Time frame. May 12, 2008 - October 27, 2008

    Supervisor. Dr. Chad E Brown

    Responsible Professor. Professor Dr. Gert Smolka