SWISH Pathfinder on the directed graph

Help! Predicate
, ,
1

Screenshot 1

Hello everyone.
I need your help, I’m a beginner in prolog.

Based on the directed graph,

  1. how to write a program which searches for paths in the graph, declaring the edges in order I, II and III?
    Should be like edge(a,b).?
  2. check in SWISH the query Δ ⊨ Ǝx path(a,x) where the predicate path/2 searches for paths as for ‘a’?

If you don’t understand the question, I can also give details.
Thank you.

2

Hi rustamPy!

It is easier to help if you give a code sample of what you have tried so far.

Cheers/JCR

3 
node(a).
node(b).
node(c).
node(d).

edge(a,b).
edge(b,d).
edge(a,c).


path(Stop,Stop,Path,Path).
path(Start,Stop,CurrPath,Path):- Start\=Stop, edge(Start,Next),\+member(Next,CurrPath),append(CurrPath,[Next],L),path(Next,Stop,L,Path).
findPath(Start,Stop):- node(Start),node(Stop),forall(path(Start,Stop,[Start],P), writeln(P)).

showNodes:- forall(node(X), writeln(X)).
showEdges:- forall(edge(X,Y), writeln(X-Y)).
showEdges(X):- forall(edge(X,Y), writeln(X-Y)).
4

But how to check for the query Δ ⊨ Ǝx path(a,x) ?

5

I am not sure what Δ ⊨ Ǝx path(a,x) means (its not Prolog), but i am interpreting it as “there exists an x such that there is a path from a to x”. In this case you have path(a, X).

6

In Prolog (as in inductive proofs in math) you tend to write definitions in terms of themselves … can you see how this could look like when translated to two (or more) Prolog rules?

Edit:

Δ ⊨ Ǝx path(a,x)

I guess this literally means from delta (Δ) it is possible to semantically proof that there exists an x such that path(a,x) is true.

I guess Δ stands for the Prolog program that defines what a path is within the structure given.

But, i am wondering – does semantic proof (double turnstile) really apply to Prolog queries, or should it be a single turn stile (syntactic proof) – since in prolog one simply computes one example – one can also repeatendly show all x for which there is a path from a to x – but its also merely examples rather than a symbol proof.