21世紀における0～3の数字を2個ずつ使ってできる年月日の個数 (「禁則」によって表現するバージョン) | Codetter（こーどったー）

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
順列(Y,0,[]).
順列(Y,N,[A|X]) :- del(A,Y,Z), M is N - 1, 順列(Z,M,X).
del(A,[A|X],X).
del(A,[B|X],[B|Y]) :- del(A,X,Y).
小の月(2).
小の月(4).
小の月(6).
小の月(9).
小の月(11).
% 小の月(M) :- 月の日数(M, Days), Days < 31.
'「禁則」の簡略化のために利用する諸命題' :-
    '閏年か否かは考慮しなくてよい',
    '2月以外の小の月の存在は考慮しなくてよい',
    '0月、14～19月および40月以上の年月日ならびは発生しない',
    '0日および34日以上の年月日ならびは発生しない'.
    
'閏年か否かは考慮しなくてよい' :-
%      ∀ L [ L : '順列と21世紀の条件'を満たす ⇒ L : 2月29日を表す年月日並びではない ]
% ⇔ ￢∃ L [ L : '順列と21世紀の条件'を満たす ∧ L : 2月29日を表す年月日並びである ]
    \+ 順列と21世紀の条件([_,_,_,_, 0,2, 2,9]).
    
'2月以外の小の月の存在は考慮しなくてよい' :-
    % 小の月：31日の存在しない月
    \+ (
        順列と21世紀の条件([_,_,_,_, M1,M2, 3,1]),
        M is (M1 * 10 + M2), '2月以外の小の月'(M)
    ).
    
'2月以外の小の月'(M) :- M \== 2, 小の月(M).
'0月、14～19月および40月以上の年月日ならびは発生しない' :-
    % 0月が発生しないのは、21世紀だから、年が0を少なくとも1つ使うため
    \+ (
        順列と21世紀の条件([_,_,_,_, M1,M2, _,_]),
        M is (M1 * 10 + M2),
        ( M == 0 ; (14 =< M, M =< 19) ; M >= 40 )  % まとめた
    ).
    
'0日および34日以上の年月日ならびは発生しない' :-
    \+ (
        順列と21世紀の条件([_,_,_,_, _,_, D1,D2]),
        D is D1 * 10 + D2,
        ( D == 0 ; D >= 34 )
    ).
    
順列と21世紀の条件(L) :-
    順列([0,0,1,1,2,2,3,3], 8, L),   % 「0～3の数字を2個ずつ使ってできる」こと
    [2,0,0,1, 0,1, 0,1] @=< L,      % 「21世紀」であること
    L @=< [2,1,0,0, 1,2, 3,1].
禁則([_,_,_,_, 0,2, 3,_]) :- !.
禁則([_,_,_,_, 1,3, _,_]) :- !.
禁則([_,_,_,_, 2,_, _,_]) :- !.
禁則([_,_,_,_, 3,_, _,_]) :- !.
禁則([_,_,_,_, _,_, 3,2]) :- !.
禁則([_,_,_,_, _,_, 3,3]) :- !.
条件(L) :-
%   L = [Y1,Y2,Y3,Y4, M1,M2, D1,D2],
    順列と21世紀の条件(L),
    \+ 禁則(L).             % 「年月日ならび」であるための条件 ('順列と21世紀の条件'と併せて)
    
?- '「禁則」の簡略化のために利用する諸命題',
    setof(L, 条件(L), Ls), length(Ls, N).
% N = 48
/*
備考：全称命題の証明は面倒くさいので、二重否定を使って“存在の否定”命題に変形した。
    '∀x p(x)' :- setof(x, p(x), (x の全体集合を表す整列されたリスト)).
%   :- setof(x, x ∈ 全体集合, (x の全体集合を表す整列されたリスト)).
*/
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX