path length (pathLength)

A BinaryPredicate that specifies the length (in number of GraphNodes) of a GraphPath. (pathLength path number) means that there are number nodes in the GraphPath path.

Ontology

SUMO / GRAPH-THEORY

Class(es)

class

inheritable relation

binary predicate
is instance of

asymmetric relation
is instance of

irreflexive relation
is instance of

path length

Coordinate term(s)

back fn cardinality fn front fn principal host fn probability fn skin fn arc weight attribute authors before before or equal causes causes subclass citizen closed on completely fills connected connected engineering components contains information cooccur copy crosses date decreases likelihood developmental form disjoint distributes documentation duration during earlier editor element employs equal equivalence relation on exploits expressed in language faces family relation fills finishes frequency graph part greater than greater than or equal to has purpose has skill holds during holds obligation holds right hole identity element immediate instance immediate subclass in list in scope of interest increases likelihood independent probability inhabits inhibits initial list instance interior part inverse irreflexive on larger less than less than or equal to manner material measure meets spatially meets temporally member modal attribute overlaps partially overlaps temporally parent partial ordering on partially fills partly located penetrates possesses precondition prevents proper part properly fills property publishes range range subclass realization refers reflexive on related internal concept sibling smaller starts sub attribute sub collection sub graph sub list sub organizations sub plan sub process sub proposition subclass subrelation subsumes content class subsumes content instance successor attribute successor attribute closure superficial part surface temporal part time total ordering on trichotomizing on uses valence version

Type restrictions

pathLength(graph path, positive integer)

Axioms (2)

if "the set of minimal paths that partition graph into two separate graphs" is equal to pathclass,
then there exists number so that for all path holds: if path is an instance of pathclass, then the length of path is number

(=>
      (equal
            (MinimalCutSetFn ?GRAPH)
            ?PATHCLASS)
      (exists
            (?NUMBER)
            (forall
                  (?PATH)
                  (=>
                        (instance ?PATH ?PATHCLASS)
                        (pathLength ?PATH ?NUMBER)))))

There don't exist the set of paths that partition graph into two separate graphs path1,the set of minimal paths that partition graph into two separate graphs path2 so that the length of path1 is number1 and the length of path2 is number2 and number1 is less than number2.

(not
      (exists
            (?PATH1 ?PATH2)
            (and
                  (instance
                        ?PATH1
                        (CutSetFn ?GRAPH))
                  (instance
                        ?PATH2
                        (MinimalCutSetFn ?GRAPH))
                  (pathLength ?PATH1 ?NUMBER1)
                  (pathLength ?PATH2 ?NUMBER2)
                  (lessThan ?NUMBER1 ?NUMBER2))))