A unitpath is simply a single arc followed in the forward or the reverse direction. A path can be a sequence of unitpaths, or a more complicated way of getting from one node to another. Keep in mind the distinctions between relation, unitpath, and path, since there are places where it matters.
unitpath
::= relation
Any single arc relation is also a unitpath.
unitpath
::= relation-
If R is a relation from node x to node y, then R- is a unitpath from y
to x.
path
::= unitpath
Any single arc, either forward or backward, is a path.
path
::= (converse path)
If P is a path from node x to node y, then (converse P)
is a path from y to x.
path
::= (compose {path | !}
)
If
are nodes and
is a path from
to
, then (compose
) is a path from
to
. Note: If the symbol ! appears between
and
, then
must be asserted in the current
context. Examples: 1) After doing (build member socrates class
man), the path (compose member- class) goes from socrates
to man, but the path (compose member- ! class) doesn't.
However, after doing (assert member socrates class man), both
paths exist. 2) (find (compose !) *nodes) is a way to find all
nodes that are asserted in the current context.
path
::= (kstar path)
If path P composed with itself zero or more times is a path from node x to
node y, then
(kstar P) is a path from x to y.
path
::= (kplus path)
If path P composed with itself one or more times is a path from node x to
node y, then (kplus P) is a path from x to y.
path
::= (or {path}
)
If
is a path from node x to node y or
is a path from
x to y or ...or
is a path from x to y, then
(or
...
) is a path from x to y.
path
::= (and {path}
)
If
is a path from node x to node y and
is a path from
x to y and ...and
is a path from x to y, then
(and
...
) is a path from x to y.
path
::= (not path)
If there is no path P from node x to node y, then (not
P) is a path from x to y. Warning: Belief revision
will not work for nodes that were inferred via path-based inference
that used not arcs.
path
::= (relative-complement path path)
If P is a path from node x to node y and there is no path Q from x to
y, then
(relative-complement P Q) is a path
from x to y. Warning: Belief revision
will not work for nodes that were inferred via path-based inference
that used relative-complement arcs.
path
::= (irreflexive-restrict
path)
If P is a path from node x to
node y, and
, then (irreflexive-restrict P) is a path from x to y.
path
::= (exception path
path)
If P is a path from node x to node y and there is
no path Q from x to y with length less than or equal
to the length of P, then (exception P Q) is a path
from x to y.
path
::= (domain-restrict (path node) path)
If P is a path from node x to node y and Q
is a path from x to node z, then
(domain-restrict (Q z) P)
is a path from x to y.
path
::= (range-restrict path (path node))
If P is a path from node x to node y and Q
is a path from y to node z, then
(range-restrict P (Q z))
is a path from x to y.
path
::= (path
)
If
is not
one of the symbols and, converse, compose, exception, kstar,
kplus, not, or, relative-complement,
irreflexive-restrict, domain-restrict, or
range-restrict, then
(
) is equivalent to
(compose
).