Prolog Representation for Parallel Line Theorem Reasoning

Question

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?

You need to learn about [freeze/2](https://www.swi-prolog.org/pldoc/man?predicate=freeze/2) then realize that [constraints](https://www.swi-prolog.org/pldoc/man?section=clp) bundles up most the details for you. — Guy Coder, Mar 31 '23 at 10:57
Rather than immediately counting - create a list of the parallel-to-this-segment segments, then the count is simply the list length. — brebs, Mar 31 '23 at 12:34
First, state what kind of inference rules (independently of a Prolog encoding) you intend to use. What about AB||BC & A≠C then AB||AC ? — false, Apr 01 '23 at 09:25
@false I'm not considering the common line at the moment, just three parallel lines. — ztmzzz, Apr 02 '23 at 04:36
@brebs 0 means that this is the 0th step of the derivation. parallel(seg(a,b),seg(e,f),2) means whether AB || EF can be deduced in 2 steps. — ztmzzz, Apr 03 '23 at 10:31
Putting the zero in the `parallel` rules is inappropriate. This all sounds very similar to https://www.google.com/search?q=prolog+path+edge , e.g. https://stackoverflow.com/questions/21161624/define-graph-in-prolog-edge-and-path-finding-if-there-is-a-path-between-two-ve — brebs, Apr 03 '23 at 11:01

Topological Sort · Answer 1 · 2023-04-13T20:39:35.173

0

Try this:

parallel(seg(A, B), seg(C, D)) :- 
  ((A=W,B=X);(A=X,B=W)),
  ((C=Y,D=Z);(C=Z,D=Y)),
  parallel_base(seg(W, X), seg(Y, Z)).

This uses the nonrecursive relation parallel_base, allowing the endpoints of the lines to be given in any order. I didn't use your seg/1 predicate because it's recursive and you may get endless recursion. (I recommend you comment it out, or make it nonrecursive in the same way you made parallel/2 nonrecursive by using parallel_base.)

edited Apr 13 '23 at 20:39

answered Apr 12 '23 at 13:50

Topological Sort

2,733
2
27
54

1

Thank you very much! This will solve my problem. – ztmzzz Apr 13 '23 at 05:08

score 0 · Accepted Answer · answered Apr 14 '23 at 07:04

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.

Prolog Representation for Parallel Line Theorem Reasoning

2 Answers2