A question came up on StackExchange Proof Assistants and noted Prolog and Latin squares.
OEIS A274806 states that for a square of size 4 with a diagonal and anti-diagonal there should be 48 Latin squares.
Since I could not find a listing of all 48 Latin squares of size 4 with a diagonal and anti-diagonal, created some Prolog code to generate them.
This is not optimized code and could probably be done using constraints. This was done to quickly get a listing of the 48 squares.
Click triangle to expand section.
Prolog source code
Note: The directory can be changed but the user must have write access to the directory.
Name: example.pl
Directory: C:/Users/Groot
:- module(example,
[
latin_square/2,
is_normal/1
]).
% Sxy x - column, y - row from top to bottom (think over and down)
% 11 21 31 41
% 12 22 32 42
% 13 23 33 43
% 14 24 34 44
latin_square(N,Latin_square) :-
N == 4,
!,
sequence(N,Values),
main_diagonal(Values,MD),
anti_diagonal(MD,AD),
finish(Values,MD,AD,Latin_square).
sequence(N,L) :-
numlist(1,N,L).
main_diagonal(L,P) :-
permutation(L,P).
% Given main diagonal, generate valid antidiagonal
anti_diagonal(L,P) :-
permutation(L,P),
anti_diagonal_row_diff(L,P),
anti_diagonal_col_diff(L,P).
anti_diagonal_row_diff(A,B) :-
seq_diff(A,B).
anti_diagonal_col_diff(A,B) :-
reverse(B,C),
seq_diff(A,C).
seq_diff([],[]) :- !.
seq_diff([H|_],[H|_]) :-
!,
fail.
seq_diff([_|T0],[_|T1]) :-
seq_diff(T0,T1).
% Given diagonal and anti-diagonal finish Latin square.
finish(S,[S11,S22,S33,S44],[S41,S32,S23,S14],[[S11,S21,S31,S41],[S12,S22,S32,S42],[S13,S23,S33,S43],[S14,S24,S34,S44]]) :-
member(S21,S),
S21 \= S11, true, var(S31), S21 \= S41,
S21 \= S22,
S21 \= S23,
var(S24),
member(S31,S),
S31 \= S11, S31 \= S21, true, S31 \= S41,
S31 \= S32,
S31 \= S33,
var(S34),
member(S12,S),
S12 \= S11,
true, S12 \= S22, S12 \= S32, var(S42),
var(S13),
S12 \= S14,
member(S42,S),
S42 \= S41,
S42 \= S12, S42 \= S22, S42 \= S32, true,
var(S43),
S42 \= S44,
member(S13,S),
S13 \= S11,
S13 \= S12,
true, S13 \= S23, S13 \= S33, var(S43),
S13 \= S14,
member(S43,S),
S43 \= S41,
S43 \= S42,
S43 \= S13, S43 \= S23, S43 \= S33, true,
S43 \= S44,
member(S24,S),
S24 \= S21,
S24 \= S22,
S24 \= S23,
S24 \= S14, true, var(S34), S24 \= S44,
member(S34,S),
S34 \= S31,
S34 \= S32,
S34 \= S33,
S34 \= S14, S34 \= S24, true, S34 \= S44,
true.
:- multifile
user:portray/1.
user:portray([[S11,S21,S31,S41],[S12,S22,S32,S42],[S13,S23,S33,S43],[S14,S24,S34,S44]]) :-
nl,
format('~d ~d ~d ~d~n',[S11,S21,S31,S41]),
format('~d ~d ~d ~d~n',[S12,S22,S32,S42]),
format('~d ~d ~d ~d~n',[S13,S23,S33,S43]),
format('~d ~d ~d ~d~n',[S14,S24,S34,S44]).
check_uniqueness :-
findall(LS,latin_square(4,LS),List),
length(List,LL),
list_to_set(List,Set),
length(Set,LL).
is_normal([H|_]) :-
length(H,N),
numlist(1,N,H).
Example run
Welcome to SWI-Prolog (threaded, 64 bits, version 8.5.5)
?- working_directory(_,'C:/Users/Groot').
true.
?- [example].
true.
?- tell('Latin Squares.txt'),findall(_,(latin_square(4,LS),print(LS)),S),length(S,N),told.
S = [_, _, _, _, _, _, _, _, _|...],
N = 48.
?- example:check_uniqueness.
true.
?- latin_square(4,LS),is_normal(LS).
LS =
1 2 3 4
4 3 2 1
2 1 4 3
3 4 1 2
;
LS =
1 2 3 4
3 4 1 2
4 3 2 1
2 1 4 3
;
false.
File: Latin Squares.txt
1 3 4 2
4 2 1 3
2 4 3 1
3 1 2 4
1 4 2 3
3 2 4 1
4 1 3 2
2 3 1 4
1 4 3 2
3 2 1 4
2 3 4 1
4 1 2 3
1 3 2 4
4 2 3 1
3 1 4 2
2 4 1 3
1 2 4 3
4 3 1 2
3 4 2 1
2 1 3 4
1 4 3 2
2 3 4 1
4 1 2 3
3 2 1 4
1 4 2 3
2 3 1 4
3 2 4 1
4 1 3 2
1 2 3 4
4 3 2 1
2 1 4 3
3 4 1 2
1 2 3 4
3 4 1 2
4 3 2 1
2 1 4 3
1 3 4 2
2 4 3 1
3 1 2 4
4 2 1 3
1 3 2 4
2 4 1 3
4 2 3 1
3 1 4 2
1 2 4 3
3 4 2 1
2 1 3 4
4 3 1 2
2 3 4 1
4 1 2 3
1 4 3 2
3 2 1 4
2 4 1 3
3 1 4 2
4 2 3 1
1 3 2 4
2 4 3 1
3 1 2 4
1 3 4 2
4 2 1 3
2 3 1 4
4 1 3 2
3 2 4 1
1 4 2 3
2 1 4 3
4 3 2 1
3 4 1 2
1 2 3 4
2 4 3 1
1 3 4 2
4 2 1 3
3 1 2 4
2 4 1 3
1 3 2 4
3 1 4 2
4 2 3 1
2 1 3 4
4 3 1 2
1 2 4 3
3 4 2 1
2 1 3 4
3 4 2 1
4 3 1 2
1 2 4 3
2 3 4 1
1 4 3 2
3 2 1 4
4 1 2 3
2 3 1 4
1 4 2 3
4 1 3 2
3 2 4 1
2 1 4 3
3 4 1 2
1 2 3 4
4 3 2 1
3 2 4 1
4 1 3 2
1 4 2 3
2 3 1 4
3 4 1 2
2 1 4 3
4 3 2 1
1 2 3 4
3 4 2 1
2 1 3 4
1 2 4 3
4 3 1 2
3 2 1 4
4 1 2 3
2 3 4 1
1 4 3 2
3 1 4 2
4 2 3 1
2 4 1 3
1 3 2 4
3 4 2 1
1 2 4 3
4 3 1 2
2 1 3 4
3 4 1 2
1 2 3 4
2 1 4 3
4 3 2 1
3 1 2 4
4 2 1 3
1 3 4 2
2 4 3 1
3 1 2 4
2 4 3 1
4 2 1 3
1 3 4 2
3 2 4 1
1 4 2 3
2 3 1 4
4 1 3 2
3 2 1 4
1 4 3 2
4 1 2 3
2 3 4 1
3 1 4 2
2 4 1 3
1 3 2 4
4 2 3 1
4 2 3 1
3 1 4 2
1 3 2 4
2 4 1 3
4 3 1 2
2 1 3 4
3 4 2 1
1 2 4 3
4 3 2 1
2 1 4 3
1 2 3 4
3 4 1 2
4 2 1 3
3 1 2 4
2 4 3 1
1 3 4 2
4 1 3 2
3 2 4 1
2 3 1 4
1 4 2 3
4 3 2 1
1 2 3 4
3 4 1 2
2 1 4 3
4 3 1 2
1 2 4 3
2 1 3 4
3 4 2 1
4 1 2 3
3 2 1 4
1 4 3 2
2 3 4 1
4 1 2 3
2 3 4 1
3 2 1 4
1 4 3 2
4 2 3 1
1 3 2 4
2 4 1 3
3 1 4 2
4 2 1 3
1 3 4 2
3 1 2 4
2 4 3 1
4 1 3 2
2 3 1 4
1 4 2 3
3 2 4 1
EDIT
In the original question on StackExchange Proof Assistants is
Iām interested in automating that part of some discrete problems which reduces the search space āwithout loss of generalityā by exploiting various symmetries.
In reading
āGraph Rewriting for Natural Deduction and the Proper Treatment of Variablesā by Willem Heijltjes (pdf)
is
There are three kinds of transformations: contractions, permutations and simplifications.
- Contractions are used to remove a consecutive introduction and elimination of the same connective.
- Simplifications remove parts of a proof that are unused, which occurs when a closed assumption class of an āE- or āØE-application is empty.
- Permutations are used to shift āØE- and āE applications down over elimination rules to expose other contractions.
ā¦ the formal descriptions of the normalization rules can be found in Appendix A.
While the use of contractions, permutations and simplifications is common in Prolog (think term rewriting among other predicates), formal descriptions of the (natural deduction) normalization rules found in Appendix A is not so easily found.