graph path fn (GraphPathFn)

A BinaryFunction that maps two GraphNodes to the Class of GraphPaths between those two nodes. Note that the two GraphNodes must belong to the same Graph.

Ontology

SUMO / GRAPH-THEORY

Class(es)

class

inheritable relation

binary function

graph path fn

Coordinate term(s)

addition fn day fn density fn division fn edition fn exponentiation fn hour fn intersection fn interval fn kappa fn list concatenate fn list order fn log fn max fn maximal weighted path fn measure fn mereological difference fn mereological product fn mereological sum fn min fn minimal weighted path fn minute fn month fn multiplication fn periodical issue fn recurrent time interval fn relative complement fn relative time fn remainder fn second fn series volume fn speed fn subtraction fn temporal composition fn time interval fn union fn where fn

Type restrictions

subclass graph path GraphPathFn(graph node, graph node)

Axioms (5)

If "the lowest cost path between node1 and node2" is equal to path, then path is an instance of "the set of paths between node1 and node2".

(=>
      (equal
            (MinimalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

if "the lowest cost path between node1 and node2" is equal to path and "the value of path" is equal to number,
then for all path2 holds: if path2 is an instance of "the set of paths between node1 and node2" and "the value of path2" is equal to number2, then number2 is greater than or equal to number1

(=>
      (and
            (equal
                  (MinimalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (greaterThanOrEqualTo ?NUMBER2 ?NUMBER1))))

If "the highest cost path between node1 and node2" is equal to path, then path is an instance of "the set of paths between node1 and node2".

(=>
      (equal
            (MaximalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

if "the highest cost path between node1 and node2" is equal to path and "the value of path" is equal to number,
then for all path2 holds: if path2 is an instance of "the set of paths between node1 and node2" and "the value of path2" is equal to number2, then number2 is less than or equal to number1

(=>
      (and
            (equal
                  (MaximalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

If path is a part of graph and graph is not an instance of directed graph, then "the set of paths between node1 and node2" is equal to path if and only if "the set of paths between node2 and node1" is equal to path.

(=>
      (and
            (graphPart ?PATH ?GRAPH)
            (not
                  (instance ?GRAPH DirectedGraph)))
      (<=>
            (equal
                  (GraphPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (GraphPathFn ?NODE2 ?NODE1)
                  ?PATH)))