A small directed graph, a search that remembers where it has been, and three questions: two routes that exist and one that does not. The negative answer is as much a result as the positive ones, and the proof says what it rests on.
Run it in the playground · Source
Is f reachable from a? Is g reachable from c? Is e reachable from
b?
Answering “no” is harder than answering “yes”. A “yes” needs one route; a “no” needs a search that is guaranteed to finish and then finds nothing.
edge(a, b).
edge(a, c).
edge(b, d).
edge(c, e).
edge(d, f).
edge(e, f).
edge(f, g).
reachable_via(Node, Node, _visited).
reachable_via(Start, Goal, Visited) :-
edge(Start, Next),
\+ member(Next, Visited),
reachable_via(Next, Goal, [Next|Visited]).
The Visited list records every node on the current route, and
\+ member(Next, Visited) refuses to step onto one twice. That keeps every
route finite, even on a graph with cycles.
reachable(reachability_case, path(a, f)) :-
is_reachable(a, f).
not_reachable(reachability_case, path(b, e)) :-
\+ is_reachable(b, e).
not_reachable/2 uses negation as failure: it succeeds when the finite search
for a route from b to e comes back empty.
eyeprolog examples/graph-reachability.pl
reachable(reachability_case, path(a, f)).
reachable(reachability_case, path(c, g)).
not_reachable(reachability_case, path(b, e)).
step(reachable_via(f, f, "fdba"), fact(8), ['Node' = f], []).
step(not_reachable(reachability_case, path(b, e)), rule(13), [], [\+ is_reachable(b, e)]).
step(\+ is_reachable(b, e), absent, [], []).
The route from a ends when it reaches f with the visited list "fdba"
(the list [f, d, b, a], printed in compact text form): the route was
a → b → d → f. The negative answer rests on an absent step, the record that
the search for a route from b to e finished without one.
condition('C1', resolution, ok, 19).
condition('C5', re_decision, ok, 6).
obligation(absent, theory_scoped, \+ is_reachable(b, e)).
trusted(1).
verdict(checked_with_obligations).
All 19 rule and fact steps replay. The six “not visited yet” tests are about
lists written out in their steps, so the checker decides them again itself.
The one unreachable pair, \+ is_reachable(b, e), is different: it says the
whole program has no path, which no single step can show. It is the one
obligation, and it holds as long as the program’s edge/2 facts are complete.
edge(b, e). The not_reachable/2 answer disappears, while the two
reachable/2 answers stay.edge(g, a). The search still finishes thanks to the visited
list, and not_reachable/2 disappears: b now reaches e by way of g
and a.reachable(reachability_case, path(a, g)) :- is_reachable(a, g). and
read its proof route.Learn more in The Art of EyeProlog, Chapters 4 and 7.