% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
%                                                                           %
% File:            boolean3.dtr                                             %
% Purpose:         infix notation for boolean operators                     %
% Author:          Eric Kafe, 18th August 1994                              %
% Email:           kafe@cphling.dk                                          %
% Version:         1.01                                                     %
% Related files:   boolean1.dtr, boolean2.dtr                               %
%                                                                           %
%   Copyright (c) University of Copenhagen 1994.  All rights reserved.      %
%                                                                           %
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

# vars $X $Y: true false. 

Not:
    <false> == true
    <true> == false
    <$X and $Y> == True:<Not:<$X> or Not:<$Y>>
    <$X or $Y> == True:<Not:<$X> or Not:<$Y>>
    <$X implies $Y> == True:<$X and Not:<$Y>>
    <$X if $Y> == <$Y implies $X>.

True:
    <$X and> == false
    <true and true> == true
    <$X or> == true
    <false or false>== false
    <$X implies $Y> == <$Y or Not:<$X>>
    <$X if $Y> == <$Y implies $X>.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

Claimant:
    <> == false
    <over_60> == "<over_65>"
    <male> == Not:<"<female>">
    <pensioner> == True:<"<over_65>" or <"<over_60>" and "<female>">>.

Irene:
    <> == Claimant
    <female> == true
    <over_60> == true.

Gladys:
    <> == Claimant
    <female> == true
    <over_65> == true.

Ernest:
    <> == Claimant
    <over_60> == true.

Arthur:
    <> == Claimant
    <over_65> == true.


% Four theorems:
%
% Irene:  <pensioner> = true.
% Gladys: <pensioner> = true.
% Ernest: <pensioner> = false.
% Arthur: <pensioner> = true.


% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

# hide Not True Claimant.
    
# show
    <male>
    <female>
    <over_60>
    <over_65>
    <pensioner>.

% The next line is the Revision Control System Id: do not delete it.
% $Id: archive.dtr,v 1.1 1997/04/09 20:40:33 root Exp $