OpenMath Content Dictionary: graph1

Canonical URL:
http://www.dse.nl/~postma/graph1.ocd
CD Base:
http://www.openmath.org/cd
CD File:
graph1.ocd
CD as XML Encoded OpenMath:
graph1.omcd
Defines:
arrowset, digraph, edgeset, graph, source, target, vertexset
Date:
2004-06-01
Version:
0 (Revision 13)
Review Date:
2006-06-01
Status:
experimental

This CD defines symbols for handling directed and undirected graphs. Authored by Hans Cuypers and Erik Postma. This version is edited by amc; bugfix JHD after Robbins.

graph

Description:

This symbol represents an undirected graph. It takes two arguments: the vertex set of the graph and the edge set. The vertices can be arbitrary OpenMath objects. Each edge should be a set consisting of two vertices.

Example:
A path of length 2.
$\mathrm{graph}\left(\left\{1,2,3\right\},\left\{\left\{1,2\right\},\left\{2,3\right\}\right\}\right)$
Signatures:
sts

 [Next: vertexset] [Last: target] [Top]

vertexset

Description:

This symbol represents the vertex set of a (directed or undirected) graph. It takes one argument, the graph.

Example:
If Gamma is a graph, the following function tests whether its argument v is a vertex of Gamma.
$\lambda v.v\in \mathrm{vertexset}\left(\Gamma \right)$
Signatures:
sts

 [Next: edgeset] [Previous: graph] [Top]

edgeset

Description:

This symbol represents the set of edges of an undirected graph. It takes one argument, the undirected graph.

Example:
Given a graph Gamma and two of its vertices v and w, this predicate asserts that they are adjacent.
$\left\{v,w\right\}\in \mathrm{edgeset}\left(\Gamma \right)$
Commented Mathematical property (CMP):
Every edge in an undirected graph Gamma is a subset of the vertex set of size two.
Formal Mathematical property (FMP):
$\forall e,\Gamma .e\in \mathrm{vertexset}\left(\Gamma \right)⇒e\subset \mathrm{vertexset}\left(\Gamma \right)\wedge \mathrm{size}\left(e\right)=2$
Signatures:
sts

 [Next: digraph] [Previous: vertexset] [Top]

digraph

Description:

This symbol refers to a digraph. It has two arguments. The first is the set of vertices, the second is the set of arrows. Arrows are represented by lists of length two, where a list represents the arrow from the first element to the second.

Example:
The two-sided infinite directed path.
$\mathrm{digraph}\left(\mathbb{Z},\left\{\left(x,x+1\right)|x\in \mathbb{Z}\right\}\right)$
Signatures:
sts

 [Next: arrowset] [Previous: edgeset] [Top]

arrowset

Description:

This symbol represents the set of arrows of a directed graph. It takes one argument, the directed graph.

Example:
The arrow set of the loop consists of one loop.
$\mathrm{arrowset}\left(\mathrm{digraph}\left(\left\{1\right\},\left\{\left(1,1\right)\right\}\right)\right)=\left\{\left(1,1\right)\right\}$
Signatures:
sts

 [Next: source] [Previous: digraph] [Top]

source

Description:

Given an arrow, this symbol refers to the vertex where the arrow starts. It takes one argument, the arrow.

Example:
The arrow [a, b] starts at a.
$\mathrm{source}\left(\left(a,b\right)\right)=a$
Signatures:
sts

 [Next: target] [Previous: arrowset] [Top]

target

Description:

Given an arrow, this symbol refers to the vertex the arrow points to. It takes one argument, the arrow.

Example:
The arrow [a, b] points to b.
$\mathrm{target}\left(\left(a,b\right)\right)=b$
Signatures:
sts

 [First: graph] [Previous: source] [Top]