2:- module(counting,[countingAxioms/2]).    3
    4/*========================================================================
    5    Load Modules
    6========================================================================*/
    7
    8:- use_module(semlib(options),[option/2]).    9
   10
   11/* =======================================================================
   12   Get Background Knowledge (Counting)
   13========================================================================*/
   14
   15countingAxioms(F,F):-
   16   option('--plural',false), !.
   17
   18countingAxioms(F,BK):-
   19   option('--plural',true), !,
   20
   21   BK = [A0,A1,A2,A3,A4,A5,A6,A7,A8|F],
   22
   23   A0 = all(X,all(Y,imp(subset(X,Y),all(Z,imp(member(Z,X),member(Z,Y)))))),
   24
   25   A1 = all(X,all(Y,imp(member(X,Y),and(singular(X),collection(Y))))),
   26    
   27   A2 = all(X,all(Y,imp(subset(X,Y),and(collection(X),collection(Y))))),
   28
   29   A3 = all(X,all(Y,all(Z,imp(and(subset(X,Y),subset(Y,Z)),subset(X,Z))))),
   30
   31   A4 = all(X,imp(singular(X),not(collection(X)))),
   32
   33   A5 = all(X,imp(one(X),not(two(X)))),
   34
   35   A6 = all(X,imp(collection(X),or(one(X),two(X)))),
   36
   37   A7 = all(X,imp(singular(X),some(Z,and(collection(Z),member(X,Z))))),
   38
   39   A8 = all(X,all(Y,imp(and(and(collection(X),one(X)),
   40                            and(and(collection(Y),one(Y)),
   41                                and(not(eq(X,Y)),
   42                                    and(not(subset(X,Y)),not(subset(Y,X)))))),
   43                        some(Z,and(collection(Z),
   44                                   and(subset(X,Z),
   45                                       and(two(Z),
   46                                           and(subset(Y,Z),
   47                                               all(U,imp(member(U,Z),or(member(U,X),member(U,Y)))))))))))).
   48
   49/*
   50
   51   A6 = all(X,imp(two(X),some(Y1,some(Y2,and(member(Y1,X),and(member(Y2,X),and(not(eq(Y1,Y2)),all(Z,imp(member(Z,X),or(eq(Z,Y1),eq(Z,Y2))))))))))).
   52
   53   A2 = all(X,imp(at_least_2(X),
   54                  some(Y1,and(member(Y1,X),
   55                              some(Y2,and(member(Y2,X),not(eq(Y1,Y2)))))))),
   56
   57   A3 = all(X,imp(at_least_3(X),
   58                  some(Y,and(and(at_least_2(Y),subset(Y,X)),
   59                             some(Z,and(member(Z,X),not(member(Z,Y)))))))),
   60
   61   A4 = all(X,imp(at_least_4(X),
   62                  some(Y,and(and(at_least_3(Y),subset(Y,X)),
   63                             some(Z,and(member(Z,X),not(member(Z,Y)))))))),
   64
   65   A5 = all(X,imp(at_least_5(X),
   66                  some(Y,and(and(at_least_4(Y),subset(Y,X)),
   67                             some(Z,and(member(Z,X),not(member(Z,Y)))))))),
   68
   69   A6 = all(X,imp(at_least_6(X),
   70                  some(Y,and(and(at_least_5(Y),subset(Y,X)),
   71                             some(Z,and(member(Z,X),not(member(Z,Y)))))))),
   72
   73   A7 = all(X,imp(at_least_7(X),
   74                  some(Y,and(and(at_least_6(Y),subset(Y,X)),
   75                             some(Z,and(member(Z,X),not(member(Z,Y)))))))).
   76*/