The EPSRC Project EP/D070511/1

The development of LEO-II has been initiated by the EPSRC grant EP/D070511/1 at Cambridge University, UK. Christoph Benzmüller visited Cambridge University for one year (from October 2006 to October 2007) to undertake the research together with Larry Paulson and to develop prototype of the LEO-II prover. He has been supported by Frank Theiss and Arnaud Fietzke from Saarland University, Germany.

Project Report

We report on the different activities in the project.

Basic Research and System Development

The main focus of the project has been on the developemnt of a first prototype of LEO-II. It can be download here. The architecture of LEO-II is described in [LEO-C3,LEO-C2]. LEO-II is more than a simple reimplementation of its predecessor LEO as it incorporates several novel research results:

  • Higher Order Termindexing and Termsharing

    LEO-II has strongly gained in efficiency due to the development and exploitation of termindexing and termsharing techniques (see [LEO-C1]).

  • Calculus with Primitive Equality

    LEO-II supports reasoning with primitive equality in order to overcome the cut-simulation challenge imposed by Leibniz equality.

  • Improved Cooperation with FO-ATPs

    LEO-II's search procedure has been modified so that it now more quickly generates first-order refutable clause subsets. LEO-II can cooperate with the first-order provers E and Spass (and Vampire).

  • Improved Higher Order to First Order Mappings

    LEO-II's supports different higher-order to first-order mappings known from the literature. Amongst them is a fully typed mapping which has been further improved to enable limited extensionality reasoning in the first-order provers.

Workshop on the Implementation of Logics

Christoph Benzmüller organised together with Bernd Fisher and Geoff Sutcliffe the 6th International Workshop on the Implementation of Logics as part of LPAR'06 in Phnom Penh, Cambodia, November 2006. He presented ideas on the datastructures of LEO-II and discussed them with the participants. Here are the proceedings of the event.

Case Studies

The performance of LEO-II has been compared with LEO on examples in basic set theory, about relations and functions (see [LEO-P4]). LEO-II has furthermore been successfully applied to examples in modal logics (see [LEO-B1])

Higher Order TPTP Language

In a cooperation with Geoff Sutcliffe, Florian Rabe, Allen van Gelder and Chad Brown a syntax higher-order TPTP syntax has been developed. For more information visit this website. A conference submission is in preparation (see [LEO-C4]).

Library of Test Problems

In the course of the LEO-II project meanwhile more than 200 small example problems have been formalized in the novel higher-order TPTP syntax. Some of these examples are availaible in the source distribution of LEO-II and further are available upon request. A subset will soon be selected and entered into the emerging higher-order TPTP library. Together with Geoff Sutcliffe, Christoph Benzmüller has written a project proposal to carry on with the development of the higher-order TPTP language and the development of a higher-order TPTP.

Higher Order System Competition

A first higher-order theorem prover contest (happening) will be held as part of the CASC competition at IJCAR 2008 in Sydney, Australia. The event will be organised by Christoph Benzmueller, Geoff Sutcliffe, and Florian Rabe. The emerging higher-order TPTP library will be employed for this purpose.

Research Visits, Invited Talks and Invited Courses

  • Research Visit of Christoph Benzmüller in Edinburgh and St. Andrews (5-16 February 2007).
    Invited talks:
    • Challenges for Automated Theorem Proving in Classical Higher Order Logics, The University of Edinburgh, Scotland, February 6, 2007
    • Challenges for Automated Theorem Proving in Classical Higher Order Logics, University of St. Andrews, St. Andrews, Scotland, February 8, 2007
    • Challenges for Automated Theorem Proving in Classical Higher Order Logics, Heriot-Watt University, Edinburgh, Scotland, February 6, 2007
  • Research Visit of Frank Theiss at Cambridge University (12-17 March 2007).
  • Research Visit of Christoph Weidenbach at Cambridge University (31 January - 1 February 2007).
  • Research Visit of Christoph Benzmüller at the University of Birmingham (1-4 Dezember 2006).
  • Several Research Visits of Christoph Benzmüller in Saarbrücken.
  • Research Visit of Joerg Siekmann at Cambridge University (4-7 September 2007).
  • Invited Lecture Course on Higher-Order Semantics of Christoph Benzmüller at IT University of Copenhagen, Denmark (1-5 October 2007). As an add on to this course LEO-II was discussed and demonstrated.

Awards

In 2007 Christoph Benzmüller finished his Habilitation at Saarland University, Saarbrücken. His inaugural lecture will be held in autumn 2007, after he has returned to Saarland University.

Publications

    Chapters in Books on LEO-II

    Conference and Workshop Papers on LEO-II (more to come)

    Posters on LEO-II

    Other Publications (that have been supported by the project)

    • C. Benzmüller, B. Fischer, G. Sutcliff, Proceedings of the 6th International Workshop on the Implementation of Logics. Phnom Penh, Cambodia, November 2006.
    • C. Benzmüller, C. Brown. Automation of Higher-Order Logics. In D. Gabbay, J. Woods (eds.), The Handbook of the History of Logic, Volume 9 – Logic and Computation. © Elsevier. Invited Chapter, In Preparation.
    • J. Siekmann, S. Autexier, C. Benzmüller. Herbrand's Logic. In D. Gabbay, J. Woods (eds.), The Handbook of the History of Logic, Volume 5 – Logic and Sets from Russell to Church: Logic. © Elsevier. Invited Chapter, In Preparation.
    • C. Benzmüller, V. Sorge, M. Jamnik, M. Kerber, Combined Reasoning by Automated Cooperation. Journal of Applied Logic, (2007).
    • C. Benzmüller, C. Brown. The curious inference of Boolos in MIZAR and OMEGA. In Roman Matuszewski, Anna Zalewska (eds.), From Insight to Proof – Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar, and Rhetoric, 10(23):299-388, 2007.
    • C. Benzmüller, D. Dietrich, M. Schiller, Serge Autexier, Deep Inference for Automated Proof Tutoring. KI 2007: Advances in Artificial Intelligence: 30th Annual German Conference on AI, LNAI, Osnabrück, Germany, 2007. © Springer.
    • M. Schiller, D. Dietrich, C. Benzmüller. Towards computer-assisted proof tutoring. In SCOOP Workshop: 1st Workshop on Scientific Communities of Practice, Jacobs University Bremen, Germany, 2007.
    • M. Schiller, D. Dietrich, C. Benzmueller. Proof Step Analysis for Proof Tutoring - A Learning Approach to Granularity. Submitted to a journal special issue dedicated to CADGME 2007.