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

順列(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 の全体集合を表す整列されたリスト)).
*/