Saarland University
Informatics
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

References

[1] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Studies in logic and the foundations of mathematics. North-Holland, 1984.
[2] C. E. Brown. M-Set Models. In the Festschrift in Honor of Peter B. Andrews on His 70th Birthday. (To Appear).
[3] 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.
[4] 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.
[5] 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.