RE: SUO: Graph Theory Redux
Chris,
Thanks for your comments. See my replies below.
-Ian
> -----Original Message-----
> From: Christopher A. Welty [mailto:weltyc@cs.vassar.edu]
> Sent: Thursday, December 20, 2001 7:32 PM
> To: Ian Niles; 'standard-upper-ontology@ieee.org'
> Subject: Re: SUO: Graph Theory Redux
>
>
>
> THis theory seems to have a number of problems. I have some of them
> here, but there are a lot more I didn't have time to document. Did
> you go over this with someone who knows some graph theory?
No, I figured I'd do my best, and then let members of the list critique the
result. Unfortunately, you've been the only one to take the bait.
>
> At 1:43 PM -0800 12/18/01, Ian Niles wrote:
> >============
> >Graph Theory
> >============
>
> suggest: theory for graphs. Graph Theory already means something
> that this is not.
Um, okay, but what is the distinction between "Graph Theory" and "theory for
graphs"?
>
> >(subclass Graph Abstract)
> >(documentation Graph "The &%Class of graphs, where a graph
> is understood
> >to be a set of &%GraphNodes and a set of &%GraphArcs. Note that this
> >&%Class includes only connected graphs, i.e. graphs in which
> all &%GraphNodes are connected. The set of &%GraphNodes or the set
> of &%GraphArcs can be empty. However, the set of &%GraphArcs cannot be
> empty if the set of &%GraphNodes is empty.")
>
> What was the rationale for this? A graph is usually defined as two
> sets: a set of nodes and a set of edges. Either can be empty,
> however the set of edges can not be empty if the set of nodes is. A
> connected graph is one in which all the nodes are connected. A
> single node is a graph.
OK, I've revised the documentation string above. Is this what you are
suggesting? However, I don't see why a set of edges cannot be empty if the
set of nodes in a graph is empty. In fact, I would think that an empty set
of nodes would require that there be no edges, since edges just connect
nodes. Maybe I just need to do some more reading...
>
> The problem with this axiomatization is that you would like to say
> that every sub-graph of a graph is a graph in and of itself, however
> you can't decompose this down to a single-node graph.
I don't follow you here. According to the axiomatization, there are two
types of graph components: &%GraphElements (arcs and nodes) and &%subgraphs
(where a &%subGraph was assumed to contain at least two arcs and three
nodes). I don't see that there was anything in the axiomatization that
required that every component of a graph itself be a graph.
>
> The normal vocabulary for an undirected "link" between two nodes is a
> "connection".
OK, thanks. I'll make this distinction in the axiomatization.
>
> I think that since the usual definition of a graph is in terms of two
> sets, nodes and edges, that there should be a relation between a
> graph and all its nodes, and another one between a graph and all its
> edges, rather than relying on a single "graphPart" relation.
OK, we can make this distinction in the formalization.
>
> >(=>
> > (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)))))))
>
> Why the functions?
Well, since I was assuming that a &%GraphPath is a &%DirectedGraph, every
&%GraphArc of a &%GraphPath would have a single beginning node and a single
ending node. Since the two relations are single valued, it seemed like a
good idea to make them functions. Do you see problems with this way of
doing things?
>
> >(=>
> > (instance ?GRAPH Graph)
> > (exists (?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
> > (and
> > (instance ?NODE1 GraphNode)
> > (instance ?NODE2 GraphNode)
> > (instance ?NODE3 GraphNode)
> > (instance ?ARC1 GraphArc)
> > (instance ?ARC2 GraphArc)
> > (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 ?ARC1 ?ARC2)))))
>
> While I don't agree with this axiom at all, unless it is for a
> "Three-Node-Graph", I wonder if you are intentionally allowing Node3
> to equal Node1, and since links requires nodes and arcs do you need
> the first five terms in the conjunction?
I agree with you here. We need the clause '(not (equal ?NODE1 ?NODE3))',
and we can eliminate the first five clauses in the conjunction (they are
indeed superfluous given the type restrictions on the predicate 'links').
>
> >(subclass DirectedGraph Graph)
> >(documentation DirectedGraph "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).")
> >
> >(=>
> > (and
> > (instance ?GRAPH DirectedGraph)
> > (instance ?ARC GraphArc)
> > (graphPart ?ARC ?GRAPH))
> > (exists (?NODE1 ?NODE2)
> > (and
> > (equal (InitialNodeFn ?ARC) ?NODE1)
> > (equal (TerminalNodeFn ?ARC) ?NODE2))))
>
> This function stuff seems an odd way to go about this.
OK, but why do you find it odd? Because you don't think the relations are
single-valued?
>
> >(subclass Tree Graph)
> >(documentation Tree "A Tree is a &%DirectedGraph that has no
> >&%GraphLoops.")
> >
> >(=>
> > (instance ?GRAPH Tree)
> > (not (exists (?LOOP)
> > (and
> > (instance ?LOOP GraphLoop)
> > (graphPart ?LOOP ?GRAPH)))))
> >
> >(subclass GraphPath DirectedGraph)
> >(documentation GraphPath "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).")
> >
> >(=>
> > (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)))))))
> >
> >(subclass GraphCircuit GraphPath)
> >(documentation GraphCircuit "A &%GraphPath that begins (see
> >&%BeginNodeFn) and ends (see &%EndNodeFn) at the same
> >&%GraphNode.")
> >
> >(<=>
> > (instance ?GRAPH GraphCircuit)
> > (exists (?NODE)
> > (and
> > (equal (BeginNodeFn ?GRAPH) ?NODE)
> > (equal (EndNodeFn ?GRAPH) ?NODE))))
> >
> >(subclass MultiGraph Graph)
> >(documentation MultiGraph "The &%Class of multigraphs. A multigraph
> >is a &%Graph containing at least one pair of &%GraphNodes that are
> >connected by more than one &%GraphArc.")
> >
> >(<=>
> > (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)))))
> >
> >(subclass PseudoGraph Graph)
> >(documentation PseudoGraph "The &%Class of pseudographs. A
> pseudograph
> >is a &%Graph containing at least one &%GraphLoop.")
> >
> >(<=>
> > (instance ?GRAPH PseudoGraph)
> > (exists (?LOOP)
> > (and
> > (instance ?LOOP GraphLoop)
> > (graphPart ?LOOP ?GRAPH))))
> >
> >(subclass GraphElement Abstract)
> >(disjoint GraphElement Graph)
> >(partition GraphElement GraphNode GraphArc)
> >(documentation GraphElement "Noncompositional parts of &%Graphs.
> >These parts are restricted to &%GraphNodes and &%GraphArcs.")
> >
> >(=>
> > (instance ?PART GraphElement)
> > (exists (?GRAPH)
> > (and
> > (instance ?GRAPH Graph)
> > (graphPart ?PART ?GRAPH))))
> >
> >(subclass GraphNode GraphElement)
> >(documentation GraphNode "&%Graphs are comprised of &%GraphNodes
> >and &%GraphArcs. Every &%GraphNode is linked by a &%GraphArc.")
> >
> >(=>
> > (instance ?NODE GraphNode)
> > (exists (?OTHER ?ARC)
> > (links ?NODE ?OTHER ?ARC)))
> >
> >(subclass GraphArc GraphElement)
> >(documentation GraphArc "&%Graphs are comprised of &%GraphNodes
> >and &%GraphArcs. Every &%GraphArc links two &%GraphNodes.")
> >
> >(=>
> > (instance ?ARC GraphArc)
> > (exists (?NODE1 ?NODE2)
> > (links ?NODE1 ?NODE2 ?ARC)))
> >
> >(subclass GraphLoop GraphArc)
> >(documentation GraphLoop "A &%GraphArc in which a &%GraphNode is
> >linked to itself.")
> >
> >(<=>
> > (instance ?LOOP GraphLoop)
> > (exists (?NODE)
> > (links ?NODE ?NODE ?LOOP)))
> >
> >(=>
> > (and
> > (equal (InitialNodeFn ?ARC) ?NODE)
> > (equal (TerminalNodeFn ?ARC) ?NODE))
> > (instance ?ARC GraphLoop))
> >
> >(instance links TernaryPredicate)
> >(domain links 1 GraphNode)
> >(domain links 2 GraphNode)
> >(domain links 3 GraphArc)
> >(documentation links "a &%TernaryPredicate that specifies the
> >&%GraphArc connecting two &%GraphNodes.")
> >
> >(=>
> > (links ?NODE1 ?NODE2 ?ARC)
> > (links ?NODE2 ?NODE1 ?ARC))
> >
> >(instance graphPart BinaryPredicate)
> >(instance graphPart AsymmetricRelation)
> >(instance graphPart IrreflexiveRelation)
> >(domain graphPart 1 GraphElement)
> >(domain graphPart 2 Graph)
> >(documentation graphPart "A basic relation for &%Graphs and their
> >parts. (&%graphPart ?PART ?GRAPH) means that ?PART is a &%GraphArc
> >or &%GraphNode of the &%Graph ?GRAPH.")
> >
> >(instance subGraph BinaryPredicate)
> >(instance subGraph ReflexiveRelation)
> >(instance subGraph TransitiveRelation)
> >(domain subGraph 1 Graph)
> >(domain subGraph 2 Graph)
> >(documentation subGraph "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.")
> >
> >(=>
> > (and
> > (subGraph ?GRAPH1 ?GRAPH2)
> > (graphPart ?ELEMENT ?GRAPH1))
> > (graphPart ?ELEMENT ?GRAPH2))
> >
> >(instance pathLength BinaryPredicate)
> >(instance pathLength AsymmetricRelation)
> >(instance pathLength IrreflexiveRelation)
> >(domain pathLength 1 GraphPath)
> >(domain pathLength 2 PositiveInteger)
> >(documentation 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.")
> >
> >(instance InitialNodeFn UnaryFunction)
> >(domain InitialNodeFn 1 GraphArc)
> >(range InitialNodeFn GraphNode)
> >(documentation InitialNodeFn "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.")
> >
> >(instance TerminalNodeFn UnaryFunction)
> >(domain TerminalNodeFn 1 GraphArc)
> >(range TerminalNodeFn GraphNode)
> >(documentation TerminalNodeFn "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.")
> >
> >(instance BeginNodeFn UnaryFunction)
> >(domain BeginNodeFn 1 GraphPath)
> >(range BeginNodeFn GraphNode)
> >(relatedInternalConcept BeginNodeFn InitialNodeFn)
> >(documentation BeginNodeFn "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.")
> >
> >(instance EndNodeFn UnaryFunction)
> >(domain EndNodeFn 1 GraphPath)
> >(range EndNodeFn GraphNode)
> >(relatedInternalConcept EndNodeFn TerminalNodeFn)
> >(documentation EndNodeFn "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.")
> >
> >(instance arcWeight BinaryPredicate)
> >(domain arcWeight 1 GraphArc)
> >(domain arcWeight 2 RealNumber)
> >(documentation arcWeight "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.")
> >
> >(instance PathWeightFn UnaryFunction)
> >(domain PathWeightFn 1 GraphPath)
> >(range PathWeightFn RealNumber)
> >(documentation PathWeightFn "A &%UnaryFunction that maps a
> >&%GraphPath to the sum of the &%arcWeights on the &%GraphArcs in
> >the &%GraphPath.")
> >
> >(=>
> > (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)))
> >
> >(instance MinimalWeightedPathFn BinaryFunction)
> >(domain MinimalWeightedPathFn 1 GraphNode)
> >(domain MinimalWeightedPathFn 2 GraphNode)
> >(range MinimalWeightedPathFn GraphPath)
> >(documentation MinimalWeightedPathFn "This &%BinaryFunction
> assigns two
> >&%GraphNodes to the &%GraphPath with the smallest sum of
> weighted arcs
> >between the two &%GraphNodes.")
> >
> >(=>
> > (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))))
> >
> >(instance MaximalWeightedPathFn BinaryFunction)
> >(domain MaximalWeightedPathFn 1 GraphNode)
> >(domain MaximalWeightedPathFn 2 GraphNode)
> >(range MaximalWeightedPathFn GraphPath)
> >(documentation MaximalWeightedPathFn "This &%BinaryFunction
> assigns two
> >&%GraphNodes to the &%GraphPath with the largest sum of weighted arcs
> >between the two &%GraphNodes.")
> >
> >(=>
> > (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))))
> >
> >(instance GraphPathFn BinaryFunction)
> >(domain GraphPathFn 1 GraphNode)
> >(domain GraphPathFn 2 GraphNode)
> >(rangeSubclass GraphPathFn GraphPath)
> >(documentation 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.")
> >
> >(=>
> > (and
> > (graphPart ?PATH ?GRAPH)
> > (not (instance ?GRAPH DirectedGraph)))
> >(<=>
> > (equal (GraphPathFn ?NODE1 ?NODE2) ?PATH)
> > (equal (GraphPathFn ?NODE2 ?NODE1) ?PATH)))
> >
> >(instance CutSetFn UnaryFunction)
> >(domain CutSetFn 1 Graph)
> >(rangeSubclass CutSetFn GraphPath)
> >(documentation cutset "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.")
> >
> >(instance MinimalCutSetFn UnaryFunction)
> >(domain MinimalCutSetFn 1 Graph)
> >(rangeSubclass MinimalCutSetFn GraphPath)
> >(internalRelatedConcept MinimalCutSetFn CutSetFn)
> >(documentation minimalCutset "A &%UnaryFunction that assigns
> a &%Graph
> >the &%Class of &%GraphPaths which comprise cutsets for the
> &%Graph and
> >which have the least number of &%GraphArcs.")
> >
> >(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))))
>
>
> --
>
> Christopher A. Welty http://www.cs.vassar.edu/faculty/welty/
> Vassar College Computer Science Dept. Voice: (845) 437-5992
> Poughkeepsie, NY 12604-0462 Fax: (845) 437-7498
>