Each presenter will have a 10 minute "talk" slot to present the system to the audience in the traditional laptop+projector mode (we envisage a brief overview of the system and a demonstration of it running and solving one or both of the simple problems below). Following the 10 minute presentations there will be an open forum during which presenters will all be available to give individual and more detailed information and demonstrations. We also plan to have a panel session to discuss how to have a CASC-inspired system competition for higher-order logic.
The two first examples are hoped to 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 difficult.
%-----------------------------------------------------------------------
%----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. These axioms define the set
%----operators as lambda-terms. The general idea is that sets are
%----represented by their characteristic functions.
thf(ax_in,axiom,(
( in
= ( ^ [X: $i,S: ( $i > $o )] :
( S @ X ) ) ) )).
thf(ax_intersection,axiom,(
( intersection
= ( ^ [S1: ( $i > $o ),S2: ( $i > $o ),U: $i] :
( ( in @ U @ S1 )
& ( in @ U @ S2 ) ) ) ) )).
thf(ax_union,axiom,(
( union
= ( ^ [S1: ( $i > $o ),S2: ( $i > $o ),U: $i] :
( ( in @ U @ S1 )
| ( in @ U @ S2 ) ) ) ) )).
%----The distributivity of union over intersection.
thf(thm_distr,conjecture,(
! [A: ( $i > $o ),B: ( $i > $o ),C: ( $i > $o )] :
( ( union @ A @ ( intersection @ B @ C ) )
= ( intersection @ ( union @ A @ B ) @ ( union @ A @ C ) ) ) )).
%------------------------------------------------------------------------
%------------------------------------------------------------------------------
%----Type declarations
thf(islander,type,(
islander: $i )).
thf(knight,type,(
knight: $i )).
thf(knave,type,(
knave: $i )).
thf(says,type,(
says: $i > $o > $o )).
thf(zoey,type,(
zoey: $i )).
thf(mel,type,(
mel: $i )).
thf(is_a,type,(
is_a: $i > $i > $o )).
%----A very special island is inhabited only by knights and knaves.
thf(kk_6_1,axiom,(
! [X: $i] :
( ( is_a @ X @ islander )
=> ( ( is_a @ X @ knight )
| ( is_a @ X @ knave ) ) ) )).
%----Knights tell the truth
thf(kk_6_2,axiom,(
! [X: $i] :
( ( is_a @ X @ knight )
=> ! [A: $o] :
( ( says @ X @ A )
=> A ) ) )).
%----Knaves lie
thf(kk_6_3,axiom,
! [X: $i] :
( ( is_a @ X @ knave )
=> ! [A: $o] :
( ( says @ X @ A )
=> ~ ( A ) ) )).
%----Zoey and Mel are islanders
thf(kk_6_4,axiom,
( ( is_a @ zoey @ islander )
& ( is_a @ mel @ islander ) )).
%----Zoey says Mel is a knave
thf(kk_6_5,axiom,
( says @ zoey @ ( is_a @ mel @ knave ) )).
%----Mel says `Neither Zoey nor I are knaves.'
thf(kk_6_6,axiom,
( says @ mel
@ ~ ( ( is_a @ zoey @ knave )
| ( is_a @ mel @ knave ) ) )).
%----Who is a knight and who is a knave?
thf(query,conjecture,(
? [Y: $i,Z: $i] :
( ( ( Y = knight )
<~> ( Y = knave ) )
& ( ( Z = knight )
<~> ( Z = knave ) )
& ( is_a @ mel @ Y )
& ( is_a @ zoey @ Z ) ) )).
%------------------------------------------------------------------------------
thf(surjectiveCantorThm,conjecture,(
~ ( ? [G: $i > $i > $o] :
! [F: $i > $o] :
? [X: $i] :
( ( G @ X )
= F ) ) )).
%------------------------------------------------------------------------------