environ 
        == This is where the premises of the argument are placed
        == each of these sentences is assumed to be true. 

        == First we introduce the names of the objects involved
        == in the argument.  These names are global constants.

    given A, B, C being PERSON;

        == Then we state the logical relationships between the objects.

    P0: Knight[A];
    P1: Knight[A] implies Knave[B];
    P2: Knave[B]  implies Knight[C];

        == Now we start the reasoning part of the argument.
begin 

    S1: Knave[B] by P0, P1; 
    S2: Knight[C] by S1, P2;