%------------------------------------------------------------------------------ % Directed 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 % R.W.Butler@larc.nasa.gov % % abstract_min -- abstract definition of min % abstract_max -- abstract definition of max % circuits -- theory of circuits % pairs -- theory of pairs used for definition of edge % digraphs -- fundamental definition of a digraph % digraph_conn_defs -- defs of piece, path, and structural connectedness % digraph_deg -- definition of degree % digraph_inductions -- vertex and edge inductions for digraphs % digraph_ops -- delete vertex and delete edge operations % dags, -- directed acyclic graphs % ind_paths -- definition of independent paths % max_di_subgraphs -- maximal di_subgraphs with specified property % max_subtrees -- maximal subtrees with specified property % 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 % reduce_walks -- operation to reduce a walk % sep_sets -- definition of separating sets % di_subgraphs -- generation of di_subgraphs from vertex sets % di_subgraphs_from_walk -- generation of di_subgraphs from walks % subtrees -- subtrees of a digraph % trees -- fundamental definition of trees % walk_inductions -- induction on length of a walk % walks -- fundamental definition and properties of walks % %------------------------------------------------------------------------------ top: THEORY BEGIN IMPORTING digraphs, digraph_deg, walks, paths, path_ops, dags, path_lems, circuits, di_subgraphs, di_subgraphs_from_walk, digraph_ops, max_di_subgraphs, max_subtrees, trees, subtrees, walk_inductions, min_walk_reduced, reduce_walks, abstract_min , abstract_max , pairs , digraph_conn_defs , digraph_inductions , ind_paths , min_walks, sep_sets % digraph_deg_sum -- theorem relating vertex degree and number of edges % tree_circ -- theorem that tree has no circuits % digraph_connected -- all connected defs are equivalent % ramsey_new -- Ramsey's theorem % menger -- menger's theorem % tree_paths -- theorem that tree has only one path between vertices % circuit_deg -- degree of circuits % cycle_deg -- theorem about degree and existence of cycle % digraph_complected -- unusual definition of connected digraph % digraph_conn_piece -- structural connected ==> piece connected % digraph_path_conn -- path connected ==> structural connected % digraph_piece_path -- piece connected ==> path connected % h_menger -- hard menger % meng_scaff -- scaffolding for hard menger proof % meng_scaff_defs -- scaffolding for hard menger proof % meng_scaff_prelude -- scaffolding for hard menger proof % sep_set_lems -- properties of separating sets % digraph_deg_sum, % tree_circ, % digraph_connected, % ramsey_new, % menger, % tree_paths, % Proof incorrect % circuit_deg, % cycle_deg, % not attempted yet % digraph_complected , % digraph_conn_piece , % digraph_connected , % digraph_path_conn , % digraph_piece_path , % h_menger , % meng_scaff , % meng_scaff_defs , % meng_scaff_prelude, % menger , % sep_set_lems , END top