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.
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
-  H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Studies in logic and the foundations of mathematics. North-Holland, 1984.
-  C. E. Brown. M-Set Models. In the Festschrift in Honor of Peter B. Andrews on His 70th Birthday. (To Appear).
-  G. Dowek, T. Hardin, C. Kirchner. Higher-Order Unification via Explicit Substitutions. Proc. of the 10th Annual Symposium on Logic in Computer Science (LICS 10), pages 366-374, 1995.
-  M. Hofmann. Semantical analysis of higher-order abstract syntax.
In Proc. of the 14th Annual Symposium on Logic in Computer Science (LICS 14), pages 204-213,
IEEE Computer Society Press, Los Alamitos, California, USA, 1999.
-  C. Urban and C. Tasson. Nominal Techniques in Isabelle/HOL.
In Proc. of the 20th Conference on Automated Deduction (CADE 20),
volume 3632 of LNAI, pages 38-53. Springer-Verlag, 2005.