I am using prolog for reasoning about theorems for parallel lines.
That is, AB || EF and CD || EF, which leads to AB || CD.
The current code ensures that AB || CD is true, but BA || CD is false. Is there any way to make BA || CD is also true?
M and N are to control the number of executions, which I guess is not related to the problem.
Here is my code:
seg(A,B):-seg(B,A).
parallel(seg(A,B),seg(C,D),N):-M is N - 1,M >= 0,parallel(seg(A,B),seg(E,F),M),parallel(seg(C,D),seg(E,F),M).
parallel(A,B,N):-M is N - 1,M >= 0,parallel(B,A,M).
parallel(A,B,N):-M is N - 1,M >= 0,parallel(A,B,M).
parallel(seg(a,b),seg(e,f),0).
parallel(seg(c,d),seg(e,f),0).
The query I executed:
parallel(seg(a,b),seg(c,d),2). ------true
parallel(seg(b,a),seg(c,d),2). ------false,should be true
I know I can use this method to solve the problem, but the number of rules needed is 2^N.
parallel(seg(A, B), seg(C, D)) :- parallel_base(seg(A, B), seg(C, D)).
parallel(seg(A, B), seg(D, C)) :- parallel_base(seg(A, B), seg(C, D)).
parallel(seg(B, A), seg(C, D)) :- parallel_base(seg(A, B), seg(C, D)).
parallel(seg(B, A), seg(D, C)) :- parallel_base(seg(A, B), seg(C, D)).
Is there a more elegant way to solve this problem?
I just wanted to mention - rather than:
((A=W,B=X);(A=X,B=W)),
((C=Y,D=Z);(C=Z,D=Y)),
... a neater alternative is to enforce the convention of the lower (or equal) value being first, using e.g.:
lower_upper(X, Y, L, U) :-
( X @< Y
-> L = X, U = Y
; L = Y, U = X
).
This will help to reduce the amount of unwanted choicepoints, and improve code clarity.