Evaluation of Systems for Higher-order Logic (ESHOL)

Abstract

The ESHOL sessions of the PAAR workshop focussed on the use of higher-order reasoning systems. A particular focus was on means to evaluate higher-order reasoning systems. The notion of higher-order included, but was not limited to, rami ed type theory, simple type theory, intuitionistic and constructive type theory, and logical frameworks. The notion of reasoning systems included automated and semi-automated provers, model generators, as well as proof and model checkers. There were two parts to the ESHOL sessions: (i) higher-order system demonstrations, and (ii) a panel discussion. Additionally, one of the PAAR invited speakers, Rob Arthan, gave a talk in the ESHOL topic area.

Introduction

Demonstrations

The following higher-order systems were demonstrated in the system demonstration sessions. Each presenter gave a 10 minute \talk" slot to present the system to the audience in the traditional laptop+projector mode (giving a brief overview of the system and a demonstration of it running and solving some of the problems in Appendix A). Following the 10 minute presentations there was an open forum during which presenters were all available to give individual and more detailed information and demonstrations.

Panel Discussion

The ESHOL panelists were Rob Arthan, Lucas Dixon, and Joe Hurd. The panel discussed ideas, suggestions, and potential problems related to: { The buildup of an higher-order TPTP infrastructure. { The development of automated reasoning systems for higher-order logic (or fragments of it). { Promising application areas for automated higher-order reasoning systems. { The planned organization of a higher-order CASC at CADE-22 in 2009.

Sample Problems for System Demonstrations The two rst problems should be simple enough for every system, to provide a starting point for comparisons and discussion. The third example is Cantor's Theorem, which might be more di cult. The problems are presented in the TPTP \THF" language for simple type theory, which was recently developed by the organizers [ 1 ]. The language is based on Church's simple type theory, and is a syntactically conservative extension of the untyped rst-order TPTP language. A.1 Puzzle Example %----------------------------------------------------------------------%----Signatures for basic set theory predicates and functions. thf(const_in,type,(

in: $i > ( $i > $o ) > $o )). thf(const_intersection,type,(

intersection: ( $i > $o ) > ( $i > $o ) > ( $i > $o ) )). thf(const_union,type,(

union: ( $i > $o ) > ( $i > $o ) > ( $i > $o ) )). %----Some axioms for basic set theory. thf(ax_in,axiom,( ( in = ( ^ [X: $i,S: ( $i > $o )] :

( S @ X ) ) ) )). %-----------------------------------------------------------------------thf(surjectiveCantorThm,conjecture,( ~ ( ? [G: $i > $i > $o] : ! [F: $i > $o] : ? [X: $i] : ( ( G @ X ) = F ) ) )). %-----------------------------------------------------------------------

References

1. C. Benzmuller, F. Rabe , and G. Sutcli e. THF0 - The Core TPTP Language for Classical Higher-Order Logic . In P. Baumgartner, A. Armando , and D. Gilles, editors, Proceedings of the 4th International Joint Conference on Automated Reasoning, Lecture Notes in Arti cial Intelligence , page Accepted, 2008 .