---------------------------------------------------------
-- sumo-4

[= type entityfile]
[= contents <sumo-4 subset element UnionFn IntersectionFn RelativeComplementFn ComplementFn GeneralizedUnionFn GeneralizedIntersectionFn CardinalityFn NullSet NonNullSet FiniteSet PairwiseDisjointClass MutuallyDisjointClass KappaFn Graph DirectedGraph Tree GraphPath GraphCircuit MultiGraph PseudoGraph GraphElement GraphNode GraphArc GraphLoop links graphPart subGraph pathLength InitialNodeFn TerminalNodeFn BeginNodeFn EndNodeFn arcWeight PathWeightFn MinimalWeightedPathFn MaximalWeightedPathFn GraphPathFn CutSetFn MinimalCutSetFn>]

---------------------------------------------------------
-- subset

[= type ontoc]
[= domain <Set Set Set Set>]
[= subrelation {subclass subclass}]

@Comment
(subset ?SET1 ?SET2) is true just in case the 
&%elements of the &%Set ?SET1 are also &%elements of the &%Set ?SET2.
 
@Axioms
(=> (subset ?SUBSET ?SET)
 (forall (?ELEMENT)
  (=> (element ?ELEMENT ?SUBSET) (element ?ELEMENT ?SET))))
     
(=> (subset ?SUBSET ?SET)
 (forall (?ELEMENT)
  (=> (element ?ELEMENT ?SUBSET) (element ?ELEMENT ?SET))))
     

 
---------------------------------------------------------
-- element

[= type ontoc]
[= instance {BinaryPredicate AsymmetricRelation IntransitiveRelation BinaryPredicate AsymmetricRelation IntransitiveRelation}]
[= domain <Entity Set Entity Set>]
[= subrelation {instance instance}]

@Comment
(element ?ENTITY ?SET) is true just in case 
?ENTITY is contained in the &%Set ?SET.  An &%Entity can be an &%element 
of another &%Entity only if the latter is a &%Set.
 
@Axioms
(=>
 (forall (?ELEMENT)
  (<=> (element ?ELEMENT ?SET1) (element ?ELEMENT ?SET2)))
 (equal ?SET1 ?SET2))
     
(=>
 (forall (?ELEMENT)
  (<=> (element ?ELEMENT ?SET1) (element ?ELEMENT ?SET2)))
 (equal ?SET1 ?SET2))
     

 
---------------------------------------------------------
-- UnionFn

[= type ontoc]
[= instance {BinaryFunction TotalValuedRelation BinaryFunction TotalValuedRelation}]
[= domain <SetOrClass SetOrClass SetOrClass SetOrClass>]
[= range {SetOrClass SetOrClass}]

@Comment
A &%BinaryFunction that maps two &%SetOrClasses to 
the union of these &%SetOrClasses.  An object is an &%element of the union 
of two &%SetOrClasses just in case it is an &%instance of either &%SetOrClass.
 
---------------------------------------------------------
-- IntersectionFn

[= type ontoc]
[= instance {BinaryFunction TotalValuedRelation BinaryFunction TotalValuedRelation}]
[= domain <SetOrClass SetOrClass SetOrClass SetOrClass>]
[= range {SetOrClass SetOrClass}]

@Comment
A &%BinaryFunction that maps two 
&%SetOrClasses to the intersection of these &%SetOrClasses.  An object is 
an instance of the intersection of two &%SetOrClasses just in case it is 
an instance of both of those &%SetOrClasses.
 
---------------------------------------------------------
-- RelativeComplementFn

[= type ontoc]
[= instance {BinaryFunction TotalValuedRelation BinaryFunction TotalValuedRelation}]
[= domain <SetOrClass SetOrClass SetOrClass SetOrClass>]
[= range {SetOrClass SetOrClass}]

@Comment
A &%BinaryFunction that maps two 
&%SetOrClasses to the difference between these &%SetOrClasses.  More 
precisely, (&%RelativeComplementFn ?CLASS1 ?CLASS2) denotes the instances 
of ?CLASS1 that are not also instances of ?CLASS2.
 
---------------------------------------------------------
-- ComplementFn

[= type ontoc]
[= instance {UnaryFunction TotalValuedRelation UnaryFunction TotalValuedRelation}]
[= domain <SetOrClass SetOrClass>]
[= range {SetOrClass SetOrClass}]

@Comment
The complement of a given &%SetOrClass C is the 
&%SetOrClass of all things that are not instances of C.  In other words, an 
object is an instance of the complement of a &%SetOrClass C just in case it 
is not an instance of C.
 
---------------------------------------------------------
-- GeneralizedUnionFn

[= type ontoc]
[= instance {UnaryFunction TotalValuedRelation UnaryFunction TotalValuedRelation}]
[= range {SetOrClass SetOrClass}]
[= domainSubclass <SetOrClass SetOrClass>]

@Comment
A &%UnaryFunction that takes a &%SetOrClass 
of &%Classes as its single argument and returns a &%SetOrClass which is the 
merge of all of the &%Classes in the original &%SetOrClass, i.e. the &%SetOrClass 
containing just those instances which are instances of an instance of the 
original &%SetOrClass.
 
---------------------------------------------------------
-- GeneralizedIntersectionFn

[= type ontoc]
[= instance {UnaryFunction TotalValuedRelation UnaryFunction TotalValuedRelation}]
[= range {SetOrClass SetOrClass}]
[= domainSubclass <SetOrClass SetOrClass>]

@Comment
A &%UnaryFunction that takes a 
&%SetOrClass of &%Classes as its single argument and returns a &%SetOrClass which 
is the intersection of all of the &%Classes in the original &%SetOrClass, i.e. 
the &%SetOrClass containing just those instances which are instances of all 
instances of the original &%SetOrClass.
 
---------------------------------------------------------
-- CardinalityFn

[= type ontoc]
[= instance {UnaryFunction TotalValuedRelation AsymmetricRelation UnaryFunction TotalValuedRelation AsymmetricRelation}]
[= domain < 
     >]
[= range {Number Number}]

@Comment
(CardinalityFn ?CLASS) returns the 
number of instances in the &%SetOrClass ?CLASS or the number of 
members in the ?CLASS &%Collection.
 
---------------------------------------------------------
-- NullSet

[= type ontoc]
[= subclass {SetOrClass SetOrClass}]

@Comment
Any &%SetOrClass that contains no instances.
 
@Axioms
(=> (instance ?SET NullSet)
 (not (exists (?INST) (instance ?INST ?SET))))
     
(=> (instance ?SET NullSet)
 (not (exists (?INST) (instance ?INST ?SET))))
     

 
---------------------------------------------------------
-- NonNullSet

[= type ontoc]
[= subclass {SetOrClass SetOrClass}]

@Comment
Any &%SetOrClass that contains at least one 
instance.
 
@Axioms
(=> (instance ?SET NonNullSet) (exists (?INST) (instance ?INST ?SET)))
     
(=> (instance ?SET NonNullSet) (exists (?INST) (instance ?INST ?SET)))
     

 
---------------------------------------------------------
-- FiniteSet

[= type ontoc]
[= subclass {Set Set}]

@Comment
A &%Set containing a finite number of elements.
 
@Axioms
(=> (instance ?SET FiniteSet)
 (exists (?NUMBER)
  (and (instance ?NUMBER NonnegativeInteger)
       (equal ?NUMBER (CardinalityFn ?SET)))))
     
(=> (instance ?SET FiniteSet)
 (exists (?NUMBER)
  (and (instance ?NUMBER NonnegativeInteger)
       (equal ?NUMBER (CardinalityFn ?SET)))))
     

 
---------------------------------------------------------
-- PairwiseDisjointClass

[= type ontoc]
[= subclass {SetOrClass SetOrClass}]

@Comment
A &%SetOrClass is a &%PairwiseDisjointClass 
just in case every instance of the &%SetOrClass is either &%equal to or &%disjoint 
from every other instance of the &%SetOrClass.
 
@Axioms
(=> (instance ?SUPERCLASS PairwiseDisjointClass)
 (forall (?CLASS1 ?CLASS2)
  (=>
   (and (instance ?CLASS1 ?SUPERCLASS) (instance ?CLASS2 ?SUPERCLASS))
   (or (equal ?CLASS1 ?CLASS2) (disjoint ?CLASS1 ?CLASS2)))))
     
(=> (instance ?SUPERCLASS PairwiseDisjointClass)
 (forall (?CLASS1 ?CLASS2)
  (=>
   (and (instance ?CLASS1 ?SUPERCLASS) (instance ?CLASS2 ?SUPERCLASS))
   (or (equal ?CLASS1 ?CLASS2) (disjoint ?CLASS1 ?CLASS2)))))
     

 
---------------------------------------------------------
-- MutuallyDisjointClass

[= type ontoc]
[= subclass {SetOrClass SetOrClass}]

@Comment
A &%SetOrClass is a &%MutuallyDisjointClass 
just in case there exists nothing which is an instance of all of the instances of 
the original &%SetOrClass.
 
@Axioms
(=> (instance ?CLASS MutuallyDisjointClass)
 (forall (?INST1 ?INST2)
  (=> (and (instance ?INST1 ?CLASS) (instance ?INST2 ?INST1))
   (exists (?INST3)
    (and (instance ?INST3 ?CLASS) (not (instance ?INST2 ?INST3)))))))
     
(=> (instance ?CLASS MutuallyDisjointClass)
 (forall (?INST1 ?INST2)
  (=> (and (instance ?INST1 ?CLASS) (instance ?INST2 ?INST1))
   (exists (?INST3)
    (and (instance ?INST3 ?CLASS) (not (instance ?INST2 ?INST3)))))))
     

 
---------------------------------------------------------
-- KappaFn

[= type ontoc]
[= instance {BinaryFunction BinaryFunction}]
[= domain <SymbolicString Formula SymbolicString Formula>]
[= range {Class Class}]

@Comment
A class-forming operator that takes two 
arguments:  a variable and a formula containing at least one unbound 
occurrence of the variable.  The result of applying &%KappaFn to a 
variable and a formula is the &%SetOrClass of things that satisfy the formula.  
For example, we can denote the &%SetOrClass of prime numbers that are less 
than 100 with the following expression:  (KappaFn ?NUMBER 
(and (instance ?NUMBER PrimeNumber) (lessThan ?NUMBER 100))).  Note that 
the use of this function is discouraged, since there is currently no 
axiomatic support for it.
 
---------------------------------------------------------
-- Graph

[= type ontoc]
[= subclass {Abstract Abstract}]

@Comment
The &%Class of graphs, where a graph is understood 
to be a set of &%GraphNodes connected by &%GraphArcs.  Note that this 
&%Class includes only connected graphs, i.e. graphs in which there is a 
&%GraphPath between any two &%GraphNodes.  Note too that every &%Graph 
is assumed to contain at least two &%GraphArcs and three &%GraphNodes.
 
@Axioms
(=>
 (and (instance ?GRAPH Graph) (instance ?NODE1 GraphNode)
      (instance ?NODE2 GraphNode) (graphPart ?NODE1 ?GRAPH)
      (graphPart ?NODE2 ?GRAPH) (not (equal ?NODE1 ?NODE2)))
 (exists (?ARC ?PATH)
  (or (links ?NODE1 ?NODE2 ?ARC)
      (and (subGraph ?PATH ?GRAPH) (instance ?PATH GraphPath)
           (or (and (equal (BeginNodeFn ?PATH) ?NODE1)
                    (equal (EndNodeFn ?PATH) ?NODE2))
               (and (equal (BeginNodeFn ?PATH) ?NODE2)
                    (equal (EndNodeFn ?PATH) ?NODE1)))))))
     
(=> (instance ?GRAPH Graph)
 (exists (?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
  (and (graphPart ?NODE1 ?GRAPH) (graphPart ?NODE2 ?GRAPH)
       (graphPart ?NODE3 ?GRAPH) (graphPart ?ARC1 ?GRAPH)
       (graphPart ?ARC2 ?GRAPH) (links ?ARC1 ?NODE1 ?NODE2)
       (links ?ARC2 ?NODE2 ?NODE3) (not (equal ?NODE1 ?NODE2))
       (not (equal ?NODE2 ?NODE3)) (not (equal ?NODE1 ?NODE3))
       (not (equal ?ARC1 ?ARC2)))))
     
(=>
 (and (instance ?GRAPH Graph) (instance ?NODE1 GraphNode)
      (instance ?NODE2 GraphNode) (graphPart ?NODE1 ?GRAPH)
      (graphPart ?NODE2 ?GRAPH) (not (equal ?NODE1 ?NODE2)))
 (exists (?ARC ?PATH)
  (or (links ?NODE1 ?NODE2 ?ARC)
      (and (subGraph ?PATH ?GRAPH) (instance ?PATH GraphPath)
           (or (and (equal (BeginNodeFn ?PATH) ?NODE1)
                    (equal (EndNodeFn ?PATH) ?NODE2))
               (and (equal (BeginNodeFn ?PATH) ?NODE2)
                    (equal (EndNodeFn ?PATH) ?NODE1)))))))
     
(=> (instance ?GRAPH Graph)
 (exists (?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
  (and (graphPart ?NODE1 ?GRAPH) (graphPart ?NODE2 ?GRAPH)
       (graphPart ?NODE3 ?GRAPH) (graphPart ?ARC1 ?GRAPH)
       (graphPart ?ARC2 ?GRAPH) (links ?ARC1 ?NODE1 ?NODE2)
       (links ?ARC2 ?NODE2 ?NODE3) (not (equal ?NODE1 ?NODE2))
       (not (equal ?NODE2 ?NODE3)) (not (equal ?NODE1 ?NODE3))
       (not (equal ?ARC1 ?ARC2)))))
     

 
---------------------------------------------------------
-- DirectedGraph

[= type ontoc]
[= subclass {Graph Graph}]

@Comment
The &%Class of directed graphs.  A 
directed graph is a &%Graph in which all &%GraphArcs
have direction, i.e. every &%GraphArc has an initial node (see 
&%InitialNodeFn) and a terminal node (see &%TerminalNodeFn).
 
@Axioms
(=>
 (and (instance ?GRAPH DirectedGraph) (instance ?ARC GraphArc)
      (graphPart ?ARC ?GRAPH))
 (exists (?NODE1 ?NODE2)
  (and (equal (InitialNodeFn ?ARC) ?NODE1)
       (equal (TerminalNodeFn ?ARC) ?NODE2))))
     
(=>
 (and (instance ?GRAPH DirectedGraph) (instance ?ARC GraphArc)
      (graphPart ?ARC ?GRAPH))
 (exists (?NODE1 ?NODE2)
  (and (equal (InitialNodeFn ?ARC) ?NODE1)
       (equal (TerminalNodeFn ?ARC) ?NODE2))))
     

 
---------------------------------------------------------
-- Tree

[= type ontoc]
[= subclass {Graph Graph}]

@Comment
A Tree is a &%DirectedGraph that has no 
&%GraphLoops.
 
@Axioms
(=> (instance ?GRAPH Tree)
 (not (exists (?LOOP)
       (and (instance ?LOOP GraphLoop) (graphPart ?LOOP ?GRAPH)))))
     
(=> (instance ?GRAPH Tree)
 (not (exists (?LOOP)
       (and (instance ?LOOP GraphLoop) (graphPart ?LOOP ?GRAPH)))))
     

 
---------------------------------------------------------
-- GraphPath

[= type ontoc]
[= subclass {DirectedGraph DirectedGraph}]

@Comment
Informally, a single, directed route between 
two &%GraphNodes in a &%Graph.  Formally, a &%DirectedGraph that is a 
&%subGraph of the original &%Graph and such that no two &%GraphArcs in 
the &%DirectedGraph have the same intial node (see &%InitialNodeFn) or 
the same terminal node (see &%TerminalNodeFn).
 
@Axioms
(=>
 (and (instance ?GRAPH GraphPath) (instance ?ARC GraphArc)
      (graphPart ?ARC ?GRAPH))
 (=> (equal (InitialNodeFn ?ARC) ?NODE)
  (not (exists (?OTHER)
        (and (equal (InitialNodeFn ?OTHER) ?NODE)
             (not (equal ?OTHER ?ARC)))))))
     
(=>
 (and (instance ?GRAPH GraphPath) (instance ?ARC GraphArc)
      (graphPart ?ARC ?GRAPH))
 (=> (equal (TerminalNodeFn ?ARC) ?NODE)
  (not (exists (?OTHER)
        (and (equal (TerminalNodeFn ?OTHER) ?NODE)
             (not (equal ?OTHER ?ARC)))))))
     
(=>
 (and (instance ?GRAPH GraphPath) (instance ?ARC GraphArc)
      (graphPart ?ARC ?GRAPH))
 (=> (equal (InitialNodeFn ?ARC) ?NODE)
  (not (exists (?OTHER)
        (and (equal (InitialNodeFn ?OTHER) ?NODE)
             (not (equal ?OTHER ?ARC)))))))
     
(=>
 (and (instance ?GRAPH GraphPath) (instance ?ARC GraphArc)
      (graphPart ?ARC ?GRAPH))
 (=> (equal (TerminalNodeFn ?ARC) ?NODE)
  (not (exists (?OTHER)
        (and (equal (TerminalNodeFn ?OTHER) ?NODE)
             (not (equal ?OTHER ?ARC)))))))
     

 
---------------------------------------------------------
-- GraphCircuit

[= type ontoc]
[= subclass {GraphPath GraphPath}]

@Comment
A &%GraphPath that begins (see 
&%BeginNodeFn) and ends (see &%EndNodeFn) at the same 
&%GraphNode.
 
@Axioms
(<=> (instance ?GRAPH GraphCircuit)
 (exists (?NODE)
  (and (equal (BeginNodeFn ?GRAPH) ?NODE)
       (equal (EndNodeFn ?GRAPH) ?NODE))))
     
(<=> (instance ?GRAPH GraphCircuit)
 (exists (?NODE)
  (and (equal (BeginNodeFn ?GRAPH) ?NODE)
       (equal (EndNodeFn ?GRAPH) ?NODE))))
     

 
---------------------------------------------------------
-- MultiGraph

[= type ontoc]
[= subclass {Graph Graph}]

@Comment
The &%Class of multigraphs.  A multigraph 
is a &%Graph containing at least one pair of &%GraphNodes that are 
connected by more than one &%GraphArc.
 
@Axioms
(<=> (instance ?GRAPH MultiGraph)
 (exists (?ARC1 ?ARC2 ?NODE1 ?NODE2)
  (and (graphPart ?ARC1 ?GRAPH) (graphPart ?ARC2 ?GRAPH)
       (graphPart ?NODE1 ?GRAPH) (graphPart ?NODE2 ?GRAPH)
       (links ?NODE1 ?NODE2 ?ARC1) (links ?NODE1 ?NODE2 ?ARC2)
       (not (equal ?ARC1 ?ARC2)))))
     
(<=> (instance ?GRAPH MultiGraph)
 (exists (?ARC1 ?ARC2 ?NODE1 ?NODE2)
  (and (graphPart ?ARC1 ?GRAPH) (graphPart ?ARC2 ?GRAPH)
       (graphPart ?NODE1 ?GRAPH) (graphPart ?NODE2 ?GRAPH)
       (links ?NODE1 ?NODE2 ?ARC1) (links ?NODE1 ?NODE2 ?ARC2)
       (not (equal ?ARC1 ?ARC2)))))
     

 
---------------------------------------------------------
-- PseudoGraph

[= type ontoc]
[= subclass {Graph Graph}]

@Comment
The &%Class of pseudographs.  A pseudograph 
is a &%Graph containing at least one &%GraphLoop.
 
@Axioms
(<=> (instance ?GRAPH PseudoGraph)
 (exists (?LOOP)
  (and (instance ?LOOP GraphLoop) (graphPart ?LOOP ?GRAPH))))
     
(<=> (instance ?GRAPH PseudoGraph)
 (exists (?LOOP)
  (and (instance ?LOOP GraphLoop) (graphPart ?LOOP ?GRAPH))))
     

 
---------------------------------------------------------
-- GraphElement

[= type ontoc]
[= subclass {Abstract Abstract}]
[= partition {GraphNode GraphArc}]

@Comment
Noncompositional parts of &%Graphs.  
These parts are restricted to &%GraphNodes and &%GraphArcs.
 
@Axioms
(=> (instance ?PART GraphElement)
 (exists (?GRAPH)
  (and (instance ?GRAPH Graph) (graphPart ?PART ?GRAPH))))
     
(=> (instance ?PART GraphElement)
 (exists (?GRAPH)
  (and (instance ?GRAPH Graph) (graphPart ?PART ?GRAPH))))
     

 
---------------------------------------------------------
-- GraphNode

[= type ontoc]
[= subclass {GraphElement GraphElement}]

@Comment
&%Graphs are comprised of &%GraphNodes 
and &%GraphArcs.  Every &%GraphNode is linked by a &%GraphArc.
 
@Axioms
(=> (instance ?NODE GraphNode)
 (exists (?OTHER ?ARC) (links ?NODE ?OTHER ?ARC)))
     
(=> (instance ?NODE GraphNode)
 (exists (?OTHER ?ARC) (links ?NODE ?OTHER ?ARC)))
     

 
---------------------------------------------------------
-- GraphArc

[= type ontoc]
[= subclass {GraphElement GraphElement}]

@Comment
&%Graphs are comprised of &%GraphNodes 
and &%GraphArcs.  Every &%GraphArc links two &%GraphNodes.
 
@Axioms
(=> (instance ?ARC GraphArc)
 (exists (?NODE1 ?NODE2) (links ?NODE1 ?NODE2 ?ARC)))
     
(=> (instance ?ARC GraphArc)
 (exists (?NODE1 ?NODE2) (links ?NODE1 ?NODE2 ?ARC)))
     

 
---------------------------------------------------------
-- GraphLoop

[= type ontoc]
[= subclass {GraphArc GraphArc}]

@Comment
A &%GraphArc in which a &%GraphNode is 
linked to itself.
 
@Axioms
(<=> (instance ?LOOP GraphLoop)
 (exists (?NODE) (links ?NODE ?NODE ?LOOP)))
     
(=>
 (and (equal (InitialNodeFn ?ARC) ?NODE)
      (equal (TerminalNodeFn ?ARC) ?NODE))
 (instance ?ARC GraphLoop))
     
(<=> (instance ?LOOP GraphLoop)
 (exists (?NODE) (links ?NODE ?NODE ?LOOP)))
     
(=>
 (and (equal (InitialNodeFn ?ARC) ?NODE)
      (equal (TerminalNodeFn ?ARC) ?NODE))
 (instance ?ARC GraphLoop))
     

 
---------------------------------------------------------
-- links

[= type ontoc]
[= instance {TernaryPredicate TernaryPredicate}]
[= domain <GraphNode GraphNode GraphArc GraphNode GraphNode GraphArc>]

@Comment
a &%TernaryPredicate that specifies the 
&%GraphArc connecting two &%GraphNodes.
 
@Axioms
(=> (links ?NODE1 ?NODE2 ?ARC) (links ?NODE2 ?NODE1 ?ARC))
     
(=> (links ?NODE1 ?NODE2 ?ARC) (links ?NODE2 ?NODE1 ?ARC))
     

 
---------------------------------------------------------
-- graphPart

[= type ontoc]
[= instance {BinaryPredicate AsymmetricRelation IrreflexiveRelation BinaryPredicate AsymmetricRelation IrreflexiveRelation}]
[= domain <GraphElement Graph GraphElement Graph>]

@Comment
A basic relation for &%Graphs and their 
parts.  (&%graphPart ?PART ?GRAPH) means that ?PART is a &%GraphArc 
or &%GraphNode of the &%Graph ?GRAPH.
 
---------------------------------------------------------
-- subGraph

[= type ontoc]
[= instance {BinaryPredicate ReflexiveRelation TransitiveRelation BinaryPredicate ReflexiveRelation TransitiveRelation}]
[= domain <Graph Graph Graph Graph>]

@Comment
The relation between two &%Graphs when one 
&%Graph is a part of the other.  (&%subGraph ?GRAPH1 ?GRAPH2) means 
that ?GRAPH1 is a part of ?GRAPH2.
 
@Axioms
(=> (and (subGraph ?GRAPH1 ?GRAPH2) (graphPart ?ELEMENT ?GRAPH1))
 (graphPart ?ELEMENT ?GRAPH2))
     
(=> (and (subGraph ?GRAPH1 ?GRAPH2) (graphPart ?ELEMENT ?GRAPH1))
 (graphPart ?ELEMENT ?GRAPH2))
     

 
---------------------------------------------------------
-- pathLength

[= type ontoc]
[= instance {BinaryPredicate AsymmetricRelation IrreflexiveRelation BinaryPredicate AsymmetricRelation IrreflexiveRelation}]
[= domain <GraphPath PositiveInteger GraphPath PositiveInteger>]

@Comment
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.
 
---------------------------------------------------------
-- InitialNodeFn

[= type ontoc]
[= instance {UnaryFunction PartialValuedRelation UnaryFunction PartialValuedRelation}]
[= domain <GraphArc GraphArc>]
[= range {GraphNode GraphNode}]

@Comment
A &%UnaryFunction that maps a 
&%GraphArc to the initial node of the &%GraphArc.  Note
that this is a partial function.  In particular, the function is 
undefined for &%GraphArcs that are not part of a &%DirectedGraph.
 
---------------------------------------------------------
-- TerminalNodeFn

[= type ontoc]
[= instance {UnaryFunction PartialValuedRelation UnaryFunction PartialValuedRelation}]
[= domain <GraphArc GraphArc>]
[= range {GraphNode GraphNode}]

@Comment
A &%UnaryFunction that maps a 
&%GraphArc to the terminal node of the &%GraphArc.  Note that this 
is a partial function.  In particular, the function is undefined 
for &%GraphArcs that are not part of a &%DirectedGraph.
 
---------------------------------------------------------
-- BeginNodeFn

[= type ontoc]
[= instance {UnaryFunction TotalValuedRelation UnaryFunction TotalValuedRelation}]
[= domain <GraphPath GraphPath>]
[= range {GraphNode GraphNode}]
[= relatedInternalConcept {InitialNodeFn InitialNodeFn}]

@Comment
A &%UnaryFunction that maps a &%GraphPath 
to the &%GraphNode that is the beginning of the &%GraphPath.  Note that, 
unlike &%InitialNodeFn (which relates a &%GraphArc to a &%GraphNode),  
&%BeginNodeFn is a total function - every &%GraphPath has a beginning.
 
---------------------------------------------------------
-- EndNodeFn

[= type ontoc]
[= instance {UnaryFunction TotalValuedRelation UnaryFunction TotalValuedRelation}]
[= domain <GraphPath GraphPath>]
[= range {GraphNode GraphNode}]
[= relatedInternalConcept {TerminalNodeFn TerminalNodeFn}]

@Comment
A &%UnaryFunction that maps a &%GraphPath 
to the &%GraphNode that is the end of the &%GraphPath.  Note that, unlike 
&%TerminalNodeFn (which relates a &%GraphArc to a &%GraphNode),  
&%EndNodeFn is a total function - every &%GraphPath has a end.
 
---------------------------------------------------------
-- arcWeight

[= type ontoc]
[= instance {BinaryPredicate SingleValuedRelation BinaryPredicate SingleValuedRelation}]
[= domain <GraphArc RealNumber GraphArc RealNumber>]

@Comment
This predicate indicates the value of a 
&%GraphArc in a &%Graph.  This could map to the length of a road in 
a road network or the flow rate of a pipe in a plumbing system.
 
---------------------------------------------------------
-- PathWeightFn

[= type ontoc]
[= instance {UnaryFunction UnaryFunction}]
[= domain <GraphPath GraphPath>]
[= range {RealNumber RealNumber}]

@Comment
A &%UnaryFunction that maps a 
&%GraphPath to the sum of the &%arcWeights on the &%GraphArcs in 
the &%GraphPath.
 
@Axioms
(=>
 (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)))
     
(=>
 (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)))
     
(=>
 (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)))
     
(=>
 (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)))
     

 
---------------------------------------------------------
-- MinimalWeightedPathFn

[= type ontoc]
[= instance {BinaryFunction BinaryFunction}]
[= domain <GraphNode GraphNode GraphNode GraphNode>]
[= range {GraphPath GraphPath}]

@Comment
This &%BinaryFunction assigns two 
&%GraphNodes to the &%GraphPath with the smallest sum of weighted arcs 
between the two &%GraphNodes.
 
@Axioms
(=> (equal (MinimalWeightedPathFn ?NODE1 ?NODE2) ?PATH)
 (instance ?PATH (GraphPathFn ?NODE1 ?NODE2)))
     
(=>
 (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))))
     
(=> (equal (MinimalWeightedPathFn ?NODE1 ?NODE2) ?PATH)
 (instance ?PATH (GraphPathFn ?NODE1 ?NODE2)))
     
(=>
 (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))))
     

 
---------------------------------------------------------
-- MaximalWeightedPathFn

[= type ontoc]
[= instance {BinaryFunction BinaryFunction}]
[= domain <GraphNode GraphNode GraphNode GraphNode>]
[= range {GraphPath GraphPath}]

@Comment
This &%BinaryFunction assigns two 
&%GraphNodes to the &%GraphPath with the largest sum of weighted arcs 
between the two &%GraphNodes.
 
@Axioms
(=> (equal (MaximalWeightedPathFn ?NODE1 ?NODE2) ?PATH)
 (instance ?PATH (GraphPathFn ?NODE1 ?NODE2)))
     
(=>
 (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))))
     
(=> (equal (MaximalWeightedPathFn ?NODE1 ?NODE2) ?PATH)
 (instance ?PATH (GraphPathFn ?NODE1 ?NODE2)))
     
(=>
 (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))))
     

 
---------------------------------------------------------
-- GraphPathFn

[= type ontoc]
[= instance {BinaryFunction TotalValuedRelation BinaryFunction TotalValuedRelation}]
[= domain <GraphNode GraphNode GraphNode GraphNode>]
[= rangeSubclass {GraphPath GraphPath}]

@Comment
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.
 
@Axioms
(=>
 (and (graphPart ?PATH ?GRAPH) (not (instance ?GRAPH DirectedGraph)))
 (<=> (equal (GraphPathFn ?NODE1 ?NODE2) ?PATH)
  (equal (GraphPathFn ?NODE2 ?NODE1) ?PATH)))
     
(=>
 (and (graphPart ?PATH ?GRAPH) (not (instance ?GRAPH DirectedGraph)))
 (<=> (equal (GraphPathFn ?NODE1 ?NODE2) ?PATH)
  (equal (GraphPathFn ?NODE2 ?NODE1) ?PATH)))
     

 
---------------------------------------------------------
-- CutSetFn

[= type ontoc]
[= instance {UnaryFunction UnaryFunction}]
[= domain <Graph Graph>]
[= rangeSubclass {GraphPath GraphPath}]

@Comment
A &%UnaryFunction that assigns a &%Graph the 
&%Class of &%GraphPaths that partition the graph into two separate 
graphs if cut.  There may be more than one cutset for a given graph.
 
---------------------------------------------------------
-- MinimalCutSetFn

[= type ontoc]
[= instance {UnaryFunction UnaryFunction}]
[= domain <Graph Graph>]
[= relatedInternalConcept {CutSetFn CutSetFn}]
[= rangeSubclass {GraphPath GraphPath}]

@Comment
A &%UnaryFunction that assigns a &%Graph 
the &%Class of &%GraphPaths which comprise cutsets for the &%Graph and 
which have the least number of &%GraphArcs.
 
@Axioms
(=> (instance ?GRAPH Graph)
 (subclass (MinimalCutSetFn ?GRAPH) (CutSetFn ?GRAPH)))
     
(=> (equal (MinimalCutSetFn ?GRAPH) ?PATHCLASS)
 (exists (?NUMBER)
  (forall (?PATH)
   (=> (instance ?PATH ?PATHCLASS) (pathLength ?PATH ?NUMBER)))))
     
(=> (instance ?GRAPH Graph)
 (subclass (MinimalCutSetFn ?GRAPH) (CutSetFn ?GRAPH)))
     
(=> (equal (MinimalCutSetFn ?GRAPH) ?PATHCLASS)
 (exists (?NUMBER)
  (forall (?PATH)
   (=> (instance ?PATH ?PATHCLASS) (pathLength ?PATH ?NUMBER)))))
     
(not (exists (?PATH1 ?PATH2)
      (and (instance ?PATH1 (CutSetFn ?GRAPH))
           (instance ?PATH2 (MinimalCutSetFn ?GRAPH))
           (pathLength ?PATH1 ?NUMBER1) (pathLength ?PATH2 ?NUMBER2)
           (lessThan ?NUMBER1 ?NUMBER2))))
     

 
ooooooooooooooooooooooooooooooooooooooooooooooooooooooooo