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*/