Details About PVS Graph Theory Library

  circuit_deg           -- degree of circuits 
  circuits              -- theory of circuits 
  cycle_deg             -- theorem about degree and existence of cycle 
  graphs                -- fundamental definitiion of a graph 
  graph_conn_defs       -- defs of piece, path, and structural connectedness 
  graph_connected_ax    -- all connected defs are equivalent 
  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 
  menger_ax             -- 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            -- 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