SUO: Graph Theory Redux
Hi All,
Adam Pease and I have been working on extending and revising the
SUMO-compliant formalization of basic graph theory that I distributed last
week. The result is enclosed. Note that most of the changes are below the
definition of 'EndNodeFn'. If there are no objections, I'll go ahead and
include these definitions and axioms in the next version of the SUMO.
Thanks,
Ian
============
Graph Theory
============
(subclass Graph Abstract)
(documentation Graph "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.")
(=>
(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
(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)))))
(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))))
(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))))