path weight fn (PathWeightFn)

A UnaryFunction that maps a GraphPath to the sum of the arcWeights on the GraphArcs in the GraphPath.

Ontology

SUMO / GRAPH-THEORY

Class(es)

Classe

inheritable relation

FunzioneUnaria

path weight fn

Coordinate term(s)

absolute value fn abstraction fn arc cosine fn arc sine fn arc tangent fn back fn begin fn begin node fn cardinality fn ceiling fn complement fn cosine fn cut set fn denominator fn end fn end node fn extension fn floor fn front fn future fn generalized intersection fn generalized union fn giga fn imaginary part fn immediate future fn immediate past fn initial node fn integer square root fn kilo fn list length fn magnitude fn mega fn micro fn milli fn minimal cut set fn nano fn numerator fn organization fn past fn pico fn power set fn predecessor fn principal host fn probability fn property fn rational number fn real number fn reciprocal fn round fn signum fn sine fn skin fn square root fn successor fn tangent fn tera fn terminal node fn wealth fn when fn year fn

Type restrictions

NumeroReale PathWeightFn(CamminoDelGrafo)

Axioms (4)

se
- "il valore di path" is uguale a sum
- subpath é un sottografo di path
- arc1 é una parte di path
- il valore diarc1 énumber1
- per ogni arc2 vale: se arc2 é una parte di path, allora arc2 é una parte di subpath o arc2 is uguale a arc1
,
allora sum is uguale a "("il valore di subpath"+number1"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (subGraph ?SUBPATH ?PATH)
            (graphPart ?ARC1 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (forall
                  (?ARC2)
                  (=>
                        (graphPart ?ARC2 ?PATH)
                        (or
                              (graphPart ?ARC2 ?SUBPATH)
                              (equal ?ARC2 ?ARC1)))))
      (equal
            ?SUM
            (AdditionFn
                  (PathWeightFn ?SUBPATH)
                  ?NUMBER1)))

se
- "il valore di path" is uguale a sum
- arc1 é una parte di path
- arc2 é una parte di path
- il valore diarc1 énumber1
- il valore diarc2 énumber2
- per ogni arc3 vale: se arc3 é una parte di path, allora arc3 is uguale a arc1 o arc3 is uguale a arc2
,
allora "il valore di path" is uguale a "(number1+number2"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (graphPart ?ARC1 ?PATH)
            (graphPart ?ARC2 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (arcWeight ?ARC2 ?NUMBER2)
            (forall
                  (?ARC3)
                  (=>
                        (graphPart ?ARC3 ?PATH)
                        (or
                              (equal ?ARC3 ?ARC1)
                              (equal ?ARC3 ?ARC2)))))
      (equal
            (PathWeightFn ?PATH)
            (AdditionFn ?NUMBER1 ?NUMBER2)))

se "il cammino col minor costo tra node1 e node2" is uguale a path e "il valore di path" is uguale a number,
allora per ogni path2 vale: se path2 é un' istanza di "l' insieme di cammini tra node1 e node2" e "il valore di path2" is uguale a number2, allora number2 é più grande di o uguale a 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))))

se "il il cammino col costo maggiore tra node1 e node2" is uguale a path e "il valore di path" is uguale a number,
allora per ogni path2 vale: se path2 é un' istanza di "l' insieme di cammini tra node1 e node2" e "il valore di path2" is uguale a number2, allora number2 é minore o uguale a 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))))