FDL > PVS > Graphs : Collection


-------------------------------------------------------------------------------

 Graph Theory

  Authors:

      Jon Sjogren       AFOSR
      Ricky W. Butler   NASA Langley

  Version 2.0           Last modified 5/21/97
                        UPDATED to PVS 2.2: 11/17/98


  Maintained by:

     Rick Butler        NASA Langley Research Center   
                        *.*.******@****.****.***

  abstract  min          -- abstract definition of min
  abstract  max          -- abstract definition of max
  circuit  deg           -- degree of circuits
  circuits              -- theory of circuits
  cycle  deg             -- theorem about degree and existence of cycle
  doubletons            -- theory of doubletons used for definition of edge
  graphs                -- fundamental definition of a graph
  graph  complected      -- unusual definition of connected graph
  graph  conn  defs       -- defs of piece, path, and structural connectedness
  graph  conn  piece      -- structural connected ==> piece connected
  graph  connected       -- all connected defs are equivalent
  graph  path  conn       -- path connected ==> structural connected
  graph  piece  path      -- piece connected ==> path connected
  graph  deg             -- definition of degree
  graph  deg  sum         -- theorem relating vertex degree and number of edges
  graph  inductions      -- vertex and edge inductions for graphs
  graph  ops             -- delete vertex and delete edge operations
  h  menger              -- hard menger 
  ind  paths             -- definition of independent paths
  max  subgraphs         -- maximal subgraphs with specified property
  max  subtrees          -- maximal subtrees with specified property
  meng  scaff            -- scaffolding for hard menger proof
  meng  scaff  defs       -- scaffolding for hard menger proof
  meng  scaff  prelude    -- scaffolding for hard menger proof
  menger                -- menger's theorem
  min  walk  reduced      -- theorem that minimum walk is reduced
  min  walks             -- minimum walk satisfying a property
  path  lems             -- some useful lemmas about paths
  path  ops              -- deleting vertex and edge operations
  paths                 -- fundamental definition and properties about paths
  ramsey  new            -- Ramsey's theorem
  reduce  walks          -- operation to reduce a walk
  sep  set  lems          -- properties of separating sets
  sep  sets              -- definition of separating sets
  subgraphs             -- generation of subgraphs from vertex sets
  subgraphs  from  walk   -- generation of subgraphs from walks
  subtrees              -- subtrees of a graph
  tree  circ             -- theorem that tree has no circuits
  tree  paths            -- theorem that tree has only one path between vertices
  trees                 -- fundamental definition of trees
  walk  inductions       -- induction on length of a walk
  walks                 -- fundamental definition and properties of walks

-------------------------------------------------------------------------------

h mengergraph path connseq pidgeon
meng scaff defsgraph piece pathpath lems
abstract maxgraph inductionswalk inductions
cycle deggraph conn pieceabstract min
tree pathsgraph connectedsep sets
sep set lemsgraph conn defspath ops
subgraphs from walksubtreespaths
meng scaffcircuit degseq def
meng scaff preludetree circwalks
ind pathstreessubgraphs
mengermin lemgraph deg sum
reduce walksmax subtreesgraph ops
min walksmax uptograph deg
min walk reducedmax subgraphsdoubletons
ramsey newcircuitsgraphs
graph complectedfslib