1



    
    
    
    
    
    
    
    
                           D. Cvetkovic, L. Kraus
    
    
    
    
    
    
    
        "GRAPH" AN EXPERT SYSTEM FOR THE CLASSIFICATION AND EXTENSION
    
                OF THE KNOWLEDGE IN THE FIELD OF GRAPH THEORY
    
    
    
    
    
                              - User's manual -
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
          University of Belgrade, Faculty of Electrical Engineering
    
                         Belgrade,  November 1, 1986

1








    TABLE OF CONTENTS     





    1     INTRODUCTION  1.1 



    2     GENERAL CONSIDERATIONS   2.1 

    2.1   The Graph Theoretic Computer Language   2.1 

    2.2   Syntax Notation   2.2 

    2.3   Data Types   2.3 

    2.4   Wildcard Characters in the Variable Names   2.4 

    2.5   The Working Area (the Memory)   2.5 

    2.6   The Use of Files   2.6 



    3     USING THE SYSTEM   3.1 

    3.1   Getting Started   3.1 

    3.2   The Help Facility   3.2 
    3.2.1 Mode HELPHELP - for the Beginners   3.2 
    3.2.2 Mode HELP - for the Medium Trained Users   3.2 
    3.2.3 Mode NOHELP - for the Advanced Users   3.3 
    3.2.4 Changing the Mode of Work   3.3 

    3.3   Skipping Data   3.3 

    3.4   Cancelling a Command   3.4 

    3.5   Error Detection   3.4 
    3.5.1 Syntactical Errors   3.4 
    3.5.2 Semantical Errors   3.4 

    3.6   The Loop Facility   3.5 



    4     BIBLIOGRAPHIC DATA PROCESSING   4.1 

    4.1   Kinds of Publications   4.1 

    4.2   Storing Bibliographical Data (STORE, DELETE, MODIFY, SHOW)   4.2 

    4.3   Finding Publications (FIND, TYPE, ENUMERATE, FORGET, SORT)   4.5 

1
                                   - 4.3 -



    5     GRAPH PROCESSING   5.1 

    5.1   Introduction   5.1 

    5.2   Manipulative Tasks   5.1 
    5.2.1 Setting Values (SET)   5.2 
    5.2.2 Typing Values (TYPE)   5.2 
    5.2.3 Interactive Drawning of Graphs (SET, MODIFY)   5.3 
    5.2.4 Drawing Graphs (DRAW)   5.7 
    5.2.5 Forgetting Coordinates (FORGET)   5.7 
    5.2.6 Splitting Families (MODIFY)   5.8 
    5.2.7 Sorting Objects (SORT)   5.8 

    5.3   Creating Graphs of Common Structure (CREATE)   5.8 

    5.4   Creating Graphs by Graph Theoretic Operations (FORM)   5.9 
    5.4.1 Unary Operations   5.9 
    5.4.2 Unary Operations With a Parameter   5.10 
    5.4.3 Binary Operations   5.10 
    5.4.4 Operations Defined by a Point Set or Line Set   5.10 
    5.4.5 Operations Defined by a Point   5.11 
    5.4.6 Operations Defined by a Line   5.12 

    5.5   Relabelling Graphs (RELABEL)   5.12 

    5.6   Determining Integer Invariants (DETERMINE)   5.13 
    5.6.1 Invariants of the Graph   5.13 
    5.6.2 Invariants of a Point   5.13 
    5.6.3 Invariants of a Given Size   5.14 
    5.6.4 Invariants of Two Points   5.14 

    5.7   Determining Real Graph Invariants (CALCULATE)   5.15 

    5.8   Checking Graph Properties (CHECK)   5.15 
    5.8.1 Checking Global Graph Properties   5.15 
    5.8.2 Checking Properties of a Point in the Graph   5.16 
    5.8.3 Checking Properties of Two Graphs   5.16 
    5.8.4 Setting the Mode of Checking   5.17 

    5.9   Listing Families (LIST)   5.17 
    5.9.1 Listing Families of Integers   5.17 
    5.9.2 Listing Families of Sets   5.18 

    5.10  Investigating Graphs (INVESTIGATE)   5.18 

    5.11  Final Remarks   5.18 



    6     THEOREM PROVING   6.1 

    6.1   Introduction   6.1 

    6.2   Defining a Sentence   6.1 
    6.2.1 Entering a Sentence into the System (SET, TYPE)   6.1 
    6.2.2 Manipulations with Sentences (FORM, STORE, GET, DELETE)   6.2 

    6.3   Storing Definitions (STORE)   6.4 

1
                                   - 6.4 -
    6.4   Generating Sentences Equivalent to a Given Sentence (GENERATE)  
          6.6 

    6.5   Interactive Prover   6.7 
    6.5.1 Creating a Proof Tree (CREATE, MOVE)   6.7 
    6.5.2 Finding Subgoals (FIND, MODIFY, LIST, DELETE, SET)   6.7 
    6.5.3 Displaying Proof Tree (TYPE, DRAW)   6.10 

    6.6   Automatic Prover (PROVE)   6.11 

    6.7   Finding Necessary Sentences (FIND, SHOW, SET)   6.14 

    6.8   Temporary Limitations   6.14 



    7     UTILITIES   7.1 

    7.1   Informative Operations   7.1 
    7.1.1 Giving Informations About the System (INFORM)   7.1 
    7.1.2 Showing Tables of Keywords (SHOW)   7.1 

    7.2   Manipulations with the Data in the Memory   7.2 
    7.2.1 Copying Data (SET)   7.2 
    7.2.2 Showing Variable Names and Values (SHOW)   7.2 
    7.2.3 Forgetting Variables (FORGET)   7.3 

    7.3   Manipulations with the Data in the Files   7.4 
    7.3.1 Storing Data into Files (STORE)   7.4 
    7.3.2 Getting Data from Files (GET)   7.4 
    7.3.3 Showing Variable Names and Values in Files (SHOW)   7.5 
    7.3.4 Deleting Data from Files (DELETE)   7.5 

    7.4   Manipulations with Files   7.5 
    7.4.1 Creating Files (CREATE)   7.5 
    7.4.2 Showing Names of Files (SHOW)   7.7 
    7.4.3 Deleting Files (DELETE)   7.7 

    7.5   Miscallenous Commands   7.7 
    7.5.1 Changing the Mode of Looping (SET)   7.7 
    7.5.2 Terminating the Work (FINISH)   7.8 



          REFERENCES      



          APPENDICES      

    A     A Survey of Commands of GTCL   A.1 

          CALCULATE   A.1 
          CHECK   A.1 
          CREATE   A.2 
          DELETE   A.2 
          DETERMINE   A.3 
          DRAW   A.4 
          ENUMERATE   A.4 
          FIND   A.4 
          FINISH   A.5 
          FORGET   A.5 
1
                                   - A.5 -
          FORM   A.5 
          GENERATE   A.7 
          GET   A.8 
          INFORM   A.8 
          INVESTIGATE   A.8 
          LIST   A.8 
          MODIFY   A.9 
          MOVE   A.10 
          PROVE   A.10 
          RELABEL   A.11 
          SET   A.11 
          SHOW   A.11 
          SORT   A.12 
          STORE   A.13 
          TYPE   A.13 

    B     Tables of Keywords for Commands   B.1 

          Table 1   B.1 
          Table 2   B.1 
          Table 3   B.1 
          Table 4   B.2 
          Table 5   B.2 
          Table 6   B.2 
          Table 7   B.3 
          Table 8   B.3 
          Table 9   B.4 
          Table 10   B.4 
          Table 11   B.4 
          Table 12   B.5 
          Table 13   B.5 
          Table 14   B.5 
          Table 15   B.5 
          Table 16   B.6 
          Table 17   B.6 
          Table 18   B.6 
          Table 19   B.6 
          Table 20   B.7 
          Table 21   B.7 
          Table 22   B.7 
          Table 23   B.8 

    C     Syntax of Proper GTCL   C.1 

    D     Internal Representations   D.1 

    D.1   Graph Representation   D.1 
    D.2   Sentence Representation   D.2 
    D.3   Proof Tree Representation   D.4 
    D.4   Family Representation   D.5 
    D.5   Numerical Values   D.5 

    E     Description of Graph Catalogues and some other Files   E.1 


1








    1 INTRODUCTION 



    The interactive programming system "Graph" is an expert system for the
    classification and extension  of  knowledge  in  the  field  of  graph
    theory. The purpose of the system is to support scientific research in
    graph theory and its applications. The system "Graph" can also be used
    to teach graph theory. 

    The user communicates with the system "Graph" by a  specially  devised
    language - Graph Theoretical Computer Language (GTCL).  Language  GTCL
    is a simplified and formalized subset of English (see Chapter 2). 

    "Graph" consists of the following three main blocks: 

       BIBLI - the  information  system  about  the  literature  of  graph
               theory; 
       ALGOR - the system for solving problems on particular graphs; 
       THEOR - the system for proving theorems in graph theory. 

    The user can  store  bibliographical  data  and  organize  the  search
    through the created data base giving, for example, authors' names, key
    phrases, etc. 

    Particular graphs can enter the system via a keyboard  or  light  pen,
    and they are stored under names given by the user. Several problems on
    so defined graphs can be solved (e.g. listing components  or  cliques,
    determining diameter or chromatic number, checking whether  the  graph
    is planar or hamiltonian etc.). 

    Third block manipulates sentences which represent assertions in  graph
    theory. The sentences can  be  stored  in  several  files  as  axioms,
    theorems, lemmas etc., these files can be searched by key phrases, and
    an attempt can be made to prove the validity of  an  assertion  by  an
    interactive or by a fully automatized theorem prover. 

    There are two auxilliary blocks: 

       UTIL  - block for auxilliary manipulations; 
       INFOR - block for providing the  user  by  informations  about  the
               whole system. 

    The system "Graph" is written in FORTRAN IV.  It  contains  about  800
    subroutines and 30000 instructions. The system is linked as  a  unique
    task unit and its work is supported by about 25 files. The  system  is
    portable; the use of overlays is necessary on small computers. 

    The system "Graph" has been developed at the University  of  Belgrade,
    Faculty of Electrical Engineering, during  1980-1984  by  a  group  of
    about 25 collaborators. 

    This manual contains condensed information about  the  language  GTCL,
    i.e. about commands of the system "Graph". 

    Chapters 2-3 explain how the system "Graph"  is  started  and  contain
1
                                   - 1.2 -

    general ideas of the language GTCL. 

    In chapters 4-7 commands of GTCL related to BIBLI,  ALGOR,  THEOR  and
    UTIL, respectively, are described. 

    Appendix contains a survey of commands, tables  of  some  keywords  in
    these commands, the syntax of a part of GTCL, description of  internal
    representations  of  several  objects  treated  by  "Graph",   and   a
    description of some graph catalogues. 

    The list of references contains the papers about system "Graph",  some
    of the papers in whose preparation the system was used, and some other
    references. If there are some differences concerning  the  details  of
    implementation between these papers and User's Manual  the  data  from
    User's Manual should be considered as relevant. 

    Since the system "Graph" is being  further  modified  this  manual  is
    subjected to some slight changes or additions. This is the version  of
    November 1, 1986. 


1








    2 GENERAL CONSIDERATIONS 






    2.1 THE GRAPH THEORETIC COMPUTER LANGUAGE 


    The Graph Theoretic Computer Language (GTCL) is a formalized subset of
    the everyday English language. Sentences in the GTCL  are  called  the
    commands of GTCL. Every such command expresses a user's order  to  the
    system "Graph" to execute some procedure. 

    The GTCL is an interactive language and its commands are to  be  typed
    into the computer through a terminal using only  upper  case  letters.
    The words (separate data items)  in  the  commands  of  GTCL  must  be
    separated by at least one space  character.  A  command  of  GTCL  can
    occupy any number of lines, but each command must begin in a new line. 

    Elements of the commands of GTCL are keywords and data. 

    Keywords are sequences of alphanumeric characters (not containing  any
    space characters) having just  one  permissible  value.  They  can  be
    English words or punctuation marks (dot, comma, colon, etc.). 

    Special kind of keywords are the "grammatical" words. They do not hold
    any information, but serve just to  make  the  commands  as  close  as
    possible to grammatically  correct  english  sentences.  They  can  be
    skipped when entering a command of GTCL into the computer. 

    In the GTCL it is not necessary to type in the whole keywords. Several
    begining characters (minimal prefix),  which  uniquely  determine  the
    keyword, will suffice. The number of necessary  characters  depend  on
    the context; e.g., if at a given moment  the  keywords  DETERMINE  and
    DELETE are allowed as the next word  in  a  command,  at  least  three
    letters (DET or DEL) are necessary. 

    Data are sequences of alphanumeric characters representing values from
    a given range. The allowed range is described by the type of data  and
    the minimum and maximum value. 

    Data in the commands of GTCL can be constant values or variable names.
    More details about them are given in Section 2.3. 

    A special part of GTCL is the  proper  GTCL,  and  it  is  related  to
    sentences (see Section 6.2). 








1
                                   - 2.2 -




    2.2 SYNTAX NOTATIONS 


    The detailed description of the syntax and semantics of  the  commands
    of GTCL is given in the succeeding chapters.  As  syntax  notation,  a
    slightly modified version of the inverted notation is used. 

    Keywords, as defined in Section 2.1, are represented by their  values.
    Upper case letters denote the minimal prefix of the keyword, and lover
    case letters the rest of it (e.g.: DETermine). 

    Data are represented by descriptions put between angle brackets (e.g.:
    <graph name>). 

    Parts of commands which may be skipped are put between brackets (e.g.:
    [FOR]). 

    Multiline  braces  denote  alternatives  from   which   exactly   one,
    represented with  one  of  the  lines  between  the  braces,  must  be
    selected. E.g.: 

       {GRAPH <name>}
       {<g-name>    }
    
    Multiline brackets denote alternatives from which one or none is to be
    selected, i.e. again a part of the command which may be skipped as  in
    the earlyer single line brackets. 

    Repetition of the part of the command is represented by ellipses (...)
    after the closing bracket or brace. For example,  {<integer value>}...
    denotes array of at least one integer number, and [<integer value>]...
    denotes array possibly not containing any number at all. 

    Limited number of repetitions is  denoted  by  a  number  put  between
    parentheseses after the ellipses,  denoting  the  maximum  number  the
    cited  part  may  be  used.  E.g.:   <key phrase>[,<key phrase>]...(4)
    denotes a list of at most five key phrases. 

    A special  repetition  construct  is  denoted  by  multiline  brackets
    followed by three asterisks (***) to denote parts of the command which
    can be entered in an arbitrary order. Multiple use of  a  row  between
    the brackets doesn't create an array of data, but the laterly  entered
    data replaces the previously entered ones. The next is an  example  of
    such a structure: 

       [AUthors [<author name>]...     ]***
       [TItle <text of the title>      ]
       [PUblished [BY] <publisher name>]
       [PLace <town>                   ]
       [YEar <integer>                 ]
    







1
                                   - 2.3 -




    2.3 DATA TYPES 


    The next types of data are defined in the system "Graph": 

    a) integer data:  numerical data having only integer part. 
    b) real data:     numerical data having integer and fractional parts. 
    c) complex data:  ordered pair of two  real  values  representing  the
                      real and imaginary parts of the complex value. 
    d) graph data:    graphs represented by pairs of points between  which
                      a line exists. 
    e) tree data:     hierarchycal trees represented as a chained  set  of
                      points starting at a root. 
    f) family data:   families of arrays of integer values representing  a
                      grouping of enumerated objects into groups according
                      to some criteria. 
    g) sentence data: English sentences written in the  so  called  proper
                      GTCL (see Section 6.2). 

    Data may be in the form of a constant repesented by a value or in  the
    form of a variable represented by a name. 

    The syntax of the numerical constants (integer, real and  complex)  is
    the same as defined is the standard FORTRAN programming  language.  In
    the commands of GTCL syntax notation for them are <i-value>, <r-value>
    and <c-value>, respectively. 

    A special type constants are the so called string constants. They  are
    written as  arrays  of  alphanumeric  characters  between  a  pair  of
    quotation marks (e.g.: "THIS IS A STRING CONSTANT").  Strings  can  be
    written is an arbitrary number of lines whith an arbitrary  number  of
    space characters between the  words.  System  "Graph"  will  normalize
    these strings to have exactly one space character between any pair  of
    consecutive words. 

    Special case of writting shorter string constants is without quotation
    marks,  but  typing  underscore  characters  ( )  instead   of   space
    characters between the words (e.g.: THIS IS A STRING). In  this  case,
    the entire string must lie within the same line on the terminal. 

    String constants are used for various purpose in the commands  of  the
    GTCL. The acceptable range of them (minimal and  maximal  length,  and
    the range of the first character) can  be  limited  according  to  the
    purpose. Syntax notation for a string is <string>. 

    Constants for data types graph, tree and family are not defined. There
    is just one command in GTCL for every of these data types for entering
    particular values of them (three variants of  the  command  SEt).  The
    syntax  of  their  representation  is  described  in  the  appropriate
    sections in terms of integer constants and marks of punctuation. 

    Constants for sentence data are essentially string constants described
    above. 

    Variables are represented by names. Generally, name is a string  of  1
    through 5 characters, first of them being a  letter.  Syntax  notation
    for a name is <name>. 

1
                                   - 2.4 -

    The type of data, represented by a variable, can be defined implicitly
    or explicitly. If not stated otherwise by an appropriate keyword,  the
    type of the data is defined by the first letter of the name. 

    The next selfexplanatory syntax notations defines the implicit  naming
    convertions. These notations are used in the succeeding sections, too. 

    
       <i-name> ::= {INTEGEr <name>                   }
                    {<name beginning with I,J,K,L,M,N>}
    
       <r-name> ::= {REAL <name>                }
                    {<name beginning with A,B,C>}
    
       <c-name> ::= {COMPLEx <name>           }
                    {<name beginning with D,E>}
    
       <g-name> ::= {GRAPH <name>             }
                    {<name beginning with G,H>}
    
       <t-name> ::= {TREE <name>              }
                    {<name beginning with T,U>}
    
       <f-name> ::= {FAMILY <name>          }
                    {<name beginning with F>}
    
       <s-name> ::= {SENTENce <name>              }
                    {<name beginning with P,Q,R,S>}
    
    The fact that a data in a GTCL command can be either a constant  or  a
    variable name, in the later text is  denoted  according  to  the  next
    syntax definitions: 

    
       <integer>  ::= {<i-value>}
                      {<i-name> }
    
       <real>     ::= {<r-value>}
                      {<r-name> }
    
       <complex>  ::= {<c-value>}
                      {<c-name> }
    
       <sentence> ::= {<s-name>}
                      {<string>}
    



    2.4 WILDCARD CHARACTERS IN THE VARIABLE NAMES 


    Variable names, besides  letters  and  digits,  can  contain  wildcard
    characters, too. A wildcard character on a given place of the name can
    represent any of characters from a defined set  of  characters.  There
    are three wildcard characters with the next meanings: 

    - period (.) denotes any letter or digit at the given position of  the
      name, 

    - comma (,) denotes any special character (<space>, $, %, +, -,  etc.)
1
                                   - 2.5 -

      at the given position of the name, and 

    - semicolon (;)  denotes  any  character  (letter,  digit  or  special
      character) at the given position of the name. 

                        

    A name containing wildcard character(s) represents, actually, a set of
    names stisfying the given pattern. For example: 

    - "G.A" represents any name of three  characters  having  "G"  at  the
      first position, any letter or digit at the second position  and  "A"
      at the third position. 

    - "AB;;;" represents any name of at least two characters, all of  them
      beginning with "AB" (note  that  semicolon  can  represent  a  space
      character, too). 

    - ";;;;;" represents any name of an arbitrary length from one to  five
      characters. 

                      

    From the above wildcard characters, only the semicolon (;) can be used
    at the first position of a name. 

    Variable names in almost all commands of the GTCL may contain wildcard
    characters. If not, it is explicitly stated in the succeeding chapters
    of this Manual. 

    Wildcard characters in the commands of the GTCL  are  mainly  used  to
    request a  repeated  execution  of  a  command  using  the  succeeding
    variables from the set of variables defined by the name pattern  which
    contains wildcard character(s) (see Section 3.6). 




    2.5 THE WORKING AREA (THE MEMORY) 


    The results of the execution  of  the  GTCL  commands  can  be  either
    displayed on the terminal or stored in the working area of the  system
    "Graph". The working area resides in the main memory of  the  computer
    and is in this manual often referenced simple as "the memory". 

    The data are stored into the memory under names chosen  by  the  user.
    They represent the variables which can be used as  arguments  in  GTCL
    commands. System "Graph" will prevent the user to create two variables
    with the same name and same type in the memory. 

    Besides for saving the data created by the user, the memory is used by
    the system "Graph" to store some auxilliary data, too. They are called
    "system data" and are invisible for the user. 

    In the system "Graph", several utility operations are provided to show
    the content, of the memory, to  release  not  needed  data,  etc.  The
    appropriate GTCL commands are described in details in Section 7.2. 

    The data stored in the working area are automatically saved in a  file
    on the disk when finishing the work. This ensures that at the next run
1
                                   - 2.6 -

    of the system "Graph" the memory can be restored to the state  at  the
    end of the last run. So the user can continue the work just  where  he
    finished it the previous time. 




    2.6 THE USE OF FILES 


    The working area is a relatively small place to save data  accumulated
    in a period of time. Larger quantities of data can be saved  in  files
    residing on mass storage units  of  the  computer  (e.g.  on  magnetic
    disks).  

    Data residing in the files can't be processed by operations  installed
    in the system "Graph". They must be first copied into the working area
    of the system. There are several utility operations for  the  transfer
    the data between the memory and the files (see Section 7.3). 

    In the system "Graph" there exists a standard file, called "work file"
    of moderate capacity. Besides the work file, the user can  create  own
    files of arbitrary size. These files are identified by  names  choosen
    by the user (see Section 7.4). 

    Besides the files mentioned above, system "Graph" uses a set of  files
    of dedicated purpose. They are  not  accessible  by  the  user  in  an
    explicit manner. These files  are  used  implicitly  when  doing  some
    operations belonging to subsystems "Bibli" and "Theor". 

    Data are, similarily as in the memory, stored, retrieved  and  deleted
    by names. No file can hold two data with same name  and  type  at  any
    time. But, there is no problem to have two or more data with the  same
    name and type at same time in various files. 


1








    3 USING THE SYSTEM 






    3.1 GETTING STARTED 


    The system "Graph" is an interactive  system.  The  user  communicates
    with it in form of  a  dialogue.  The  dialogue  is  conducted  via  a
    terminal having a keyboard and a video display or via a typewriter. 

    To clear the work area (the memory) from the data left  in  it  during
    the last use of the system "Graph", the next keyboard command  of  the
    computer's operating system is to be executed: 

       RUN MEMGEN
    
    If, because of a system malfunction, the memory becomes unusable,  the
    execution of this command becomes mandatory. 

    The system "Graph" is started by typing the next keyboard command: 

       RUN GRAPH
    
    The system will respond with the following message: 

       Hello, system Graph is at your disposal.
       If you do not know how to continue, type: INFORM .
    
       Type Your next command, please!
    
    
    The system "Graph" is then ready to accept any of  the  GTCL  commands
    described in the succeeding chapters. 

    After  entering  a  command,  the  system  responds  with  appropriate
    messages (results or error messages) on the terminal. The readiness to
    accept the next GTCL command is signalized by message: 

       Type Your next command, please!
    
    
    To get more information about  the  system  the  user  can  apply  the
    command "INFORM ABOUT <keyword> ." which is described in more  details
    in Section 7.1. 

    To finish the work the command "FINISH ." should be used (see  Section
    7.5.2). 





1
                                   - 3.2 -




    3.2 THE HELP FACILITY 


    The HELP facility is the capability of the system "Graph" to guide the
    user in stating his  commands  to  the  system.  The  amount  of  help
    messages is adjustable to three levels of training of the users. 



    3.2.1 Mode HELPHELP - for the Beginners 

    The highest level of the HELP facility assumes the lowest level of the
    user knowledge about the capabilities of the system  "Graph"  and  the
    syntax of the GTCL. 

    All informations in HELPHELP mode, necessary to perform  an  operation
    of the system "Graph", are collected through a  sequence  of  question
    and answers. 

    The messages of the system consist of a question implying the  meaning
    of the expected data and a description of the expected data (type  and
    allowable range of the data). 

    The user's response is to be exactly one datum representing the answer
    to the question. Superflous data in the answer will be ignored. 

    In several cases, instead of the data description, a  message  of  the
    form "consult Table #" appears (# stands for the number of table to be
    consulted). These tables contain the list of the acceptable answers to
    the question. In such cases the user can look at the appropriate table
    in appendix B and continue the dialogue, or he can cancel the  current
    command (see Section 3.4) and state the GTCL command for  showing  the
    desired table on the terminal (see Section 7.1.2). 

    The order of questions in the dialogue corresponds to the  appropriate
    GTCL commands described in  the  subsequent  chapters.  Questions  are
    stated only for the information holding components of a command,  i.e.
    the grammatical words are skipped. 



    3.2.2 Mode HELP - for the Medium Trained Users 

    The messages of the system in HELP mode consist only of the  questions
    mentioned in the previous section. It is assumed that the  user  knows
    the allowable data types and ranges. 

    In case that for some of  the  questions  the  user  doesn't  know  to
    answer, he can ask for the data description  by  entering  a  question
    mark (?) instead of the answer. The system will respond  with  a  full
    HELPHELP mode message only once. The rest of the dialogue is  held  in
    the HELP mode (only questions). 






1
                                   - 3.3 -



    3.2.3 Mode NOHELP - for the Advanced Users 

    The system "Graph" in NOHELP mode assumes that the  user  is  able  to
    state a whole GTCL command (as described in the  succeeding  chapters)
    without any assistance. There are no  automatically  stated  questions
    during the entering a command. 

    The user can, however, ask for assistance at any time  by  entering  a
    question mark (?) instead of any word of the GTCL command. The  system
    will respond with a HELP  mode  question  corresponding  to  the  word
    replaced by the question mark. The user has to answer to the  question
    and to continue the command alone (there are  no  automatic  questions
    for the succeeding words). 

    The user can answer with  a  second  question  mark  to  the  question
    mentioned in the  previous  paragraph.  The  system  responds  with  a
    HELPHELP mode message. The user again has to answer  and  to  continue
    alone. 



    3.2.4 Changing the mode of work 

    The changing the mode of work of the system "Graph"  is  requested  by
    entering one of the keywords HELP or NOHELP. 

    Answer NOHELP to a question in HELPHELP mode changes the mode of  work
    to HELP mode. 

    Answer HELP to a question in HELP mode changes the  mode  of  work  to
    HELPHELP, and answer NOHELP to mode NOHELP. 

    Keyword HELP entered in NOHELP instead of any word of a  GTCL  command
    changes the mode of work to HELP mode. 

    At the beginning of the work of the system "Graph"  (as  described  in
    Section 3.1), the mode of work is same as the mode which was in use at
    the end of the previous session with the system. 




    3.3 SKIPPING DATA 


    In some  GTCL  commands  there  are  information  holding  parts  (not
    grammatical words) which  may  be  skipped,  giving  in  this  way  an
    alternative meaning to the command. 

    During the HELPHELP and HELP mode of work, questions appear for  these
    optional parts, too. The user, if he whishes to skip such a part,  has
    to enter a slash (/) instead of the answer. In the cases when the user
    trys to skip some necessary data, the system  responsds  with  message
    "Data can't be skipped" and repeats the question.  Entering  a  second
    slash to the same questions, yields to cancelling the whole command. 

    In NOHELP mode, optional data can be skipped simply by not typing them
    at all. Skipping a necessary data will yield to syntactical error  and
    an appropriate message of the system (see Section 3.5.1). 
1
                                   - 3.4 -





    3.4 CANCELLING A COMMAND 


    Cancelling of any beginned and not yet finished  command  of  GTCL  is
    possible any time by  entering  the  keyword  CANCEL  instead  of  the
    answers to the current question in HELPHELP and HELP mode of  work  or
    instead of the next word of command in NOHELP mode of work. The system
    will respond with message "The whole command is ignored" and begin  to
    read the next command. 

    After finishing a command by entering an empty character and a  period
    (.) at the end of command, there is no means to prevent the system  to
    execute the operations requested by the command. 




    3.5 ERROR DETECTION 


    The system "Graph" applies an elaborate error detection mechanisms  to
    the GTCL commands entered by the user. Errors can be detected  in  two
    stages of work: during the entering of a command (syntactical  errors)
    and during execution (semantic errors). 



    3.5.1 Syntactical Errors 

    To syntactical errors yield any violation of  the  syntax  of  a  GTCL
    command described in the succeeding chapters. 

    In  HELPHELP  and  HELP  modes  of  work  every  answer   is   checked
    immediately. In NOHELP mode a check is done at the end of  every  line
    of a command. Detected errors are reported  by  one  of  the  messages
    "Illegal keyword: xxxx" or "Data out of  range:  xxxx",  where  "xxxx"
    represents the word of the command containing error. 

    After one of the above messages a HELPHELP mode message is  typed,  if
    the basic mode is HELPHELP or HELP, and a HELP  mode  message  if  the
    basic mode is NOHELP. Repeated errors during  the  correction  of  the
    same data will yield to one of the above messages and a HELPHELP  mode
    message, regardless of the basic mode of work. 

    In the case of NOHELP mode  of  work,  after  the  correction  of  the
    incorrect data, all words following it must be typed again. 



    3.5.2 Semantical Errors 

    A GTCL command has semantic error if it satisfies one of  the  general
    syntax forms described in the succeeding chapters,  but  it  can't  be
    executed by the system "Graph"  for  some  reason.  Examples  of  such
    situations are requests to draw a graph not existing in the memory, to
    create a data with name which already exists  in  the  memory,  or  to
    create a data when there is not enough room in the memory to store it,
1
                                   - 3.5 -

    etc. In such cases the system "Graph" refuses to execute  the  command
    (the state of the memory or of a file remains unchanged) and types  an
    appropriate and selfexplanatory message. In such cases the  user  must
    either to correct the command (e.g. by changing the name of the data),
    or to enter some another command (e.g.  to  free  some  space  in  the
    memory). 




    3.6 THE LOOP FACILITY 


    Repetitive  execution  of  almost  all  GTCL  commands,  with  various
    variables as arguments at every repetition, can be requested with  the
    use of wildcard characters (see Section 2.4). 

    In this context, variables in a given GTCL command are divided into  a
    "primary" variable and zero, one or more "secondary" variables. 

    If not stated otherwise  in  the  detailed  description  of  the  GTCL
    commands in the succeedeing chapters,  the  primary  variable  is  the
    first variable from left to right containing wildcard character(s)  in
    the name and which represents an input variable to the command. 

    All other variables, if any, containing wildcard character(s) in their
    name are called secondary variables and they can be  either  input  or
    output variable to the command. Note, if there is a  primary  variable
    in the command, the output variable, if  present  (there  is  no  GTCL
    command with two or more output variables), should  contain  at  least
    one wildcard character in its name. Again, there is no  sense  to  use
    wildcard character in the name of the output variable if there  is  no
    primary variable. 

    When encountering a wildcard character  in  a  name  in  the  command,
    system GRAPH will enter a loop. In that loop the entire  GTCL  command
    is repeated for succeeding existing primary  variables  satifying  the
    name pattern. On succeeding passes through the loop the  next  primary
    variable is searched in the memory or in a file, depending on the GTCL
    command. When the next variable is  found,  system  GRAPH  requests  a
    confirmation by: 

       Do You want to procceed with primary
       variable NNNNN of type T ?
    
    where "NNNNN" stands for  the  name  and  "T"  for  the  type  of  the
    encountered variable. The user should answer with  "Yes"  to  procced,
    "No" to skip the variable, or "Cancel" to terminate the loop  abruptly
    (actuallly, any respond not beginning with "Y" or "C"  is  treated  as
    "No"). 

    In the case of an afirmative answer, the secondary variable names,  if
    any, are generated by substituting the wildcard  character(s)  of  the
    name pattern for them  with  the  character(s)  at  the  corresponding
    positions in the name of the  current  primary  variable  (it  is  not
    necessarry the  secondary  variable  name  pattern  to  have  wildcard
    character(s) at the same position(s)  as  the  primary  variable  name
    pattern).  For  every  generated  secondary  variable  name  the  next
    informational message is displayed: 

       Secodary variable is NNNNN of type T.
1
                                   - 3.6 -

    
    Note, that the type of the secondary variable may differ from the type
    of the primary variable, depending on the actual GTCL command. 

    A care should be made in selecting a secondary variable  name  pattern
    for output variable to ensure different generated names for every pass
    of the loop. A recommended practice is to use wildcard character(s) at
    least at the same positions as in the primary variable  name  pattern.
    The secondary variable name pattern for an output variable should  not
    consist of only wildcard characters, unless the type of the  secondary
    variable differs from the type of the primary variable. 

    In the case of multiple occurences of a given  output  variable  name,
    the pass through the loop for the second, third, etc. occurence of the
    same name will be terminated with an error message  stating  that  the
    memory or the file already contains the requested variable. 

                      

    The control of whether  the  system  GRAPH  requests  confirmation  to
    procceed for every encountered primary variable or not, is established
    by the GTCL command "SET MODE OF LOOPING ..." as described in  Section
    7.5.1. 

    In the case of supressing the  confiramtions  requests,  there  is  no
    means to prevent the system GRAPH to procceed with all the encountered
    primary variables. In such  cases  the  next  informative  message  is
    displayed for every encountered primary variable: 

       Primary variable is NNNNN of type T.
    
                    


1








    4 BIBLIOGRAPHICAL DATA PROCESSING 



    In this chapter the block BIBLI, one of the three main blocks  of  the
    system "Graph", is described. It is related to processing of the  data
    about the literature of graph theory. By  the  existing  commands  the
    user can create his own data base on the publications in  an  area  of
    graph theory he is  interested  in.  The  created  data  base  can  be
    searched according to several requirements. 




    4.1 KINDS OF PUBLICATIONS 


    Any publication which is  accepted  by  the  system  gets  a  positive
    integer as an identification number. 

    A publication which enters the system must be classified into  one  of
    the following categories: PAPER, BOOK, PROCEEDINGS, REPORT,  ABSTRACT,
    MANUSCRIPT, DOCUMENT. 

    For each type of publications there is a standard description: 

    1) Paper 

       <author(s)>:<title>;<journal>;<volume number>(<year>),
          [NO.<issue number>,]<page number>-<page number>
    
    Authors' names should be separated by commas. An author name is of the
    form  

       <surname><blank><initials>
    
    where <blank> is an obligatory space character and initials  represent
    a string of letters each followed by a period. 

    If a paper is published in a book or proceedings then it has the form  

       <author(s)>:<title>;<integer value>,<page number>-<page number>
    
    Integer value is the identification number  of  the  book  or  of  the
    proceedings in which the paper is published. 

    A blank at the beginning or at the end is not allowed. However, blanks
    are  allowed  between  different  parts  of  the  description  of  the
    publication. 

    
    2) Book
    
       <author(s)>:<title>;<publisher(s)>;
          <year>,[<preface page number>+]<page number>
    
1
                                   - 4.2 -

    Preface page  number  should  be  a  Roman  numeral.  A  publisher  is
    described by his name which can  include  the  corresponding  city  or
    cities. If there is  more  than  one  publisher,  the  publishers  are
    separated by commas. 

    3) Proceedings 

       <title>;<editor(s)>;<publisher(s)>;<year>,
                [<preface page number>+]<page number>
    
    The  title  is  any  text  describing  the  proceedings.  Editors  and
    publishers are separated by commas. Editors should  be  given  in  the
    same form as authors (see above). The preface page number is  again  a
    Roman numeral. 

    4) Report                   

       <author(s)>:<title>;<description>;<year>
    
    5) Abstract                 

       <author(s)>:<title>;<description>;<year>
    
    6) Manuscript                 

       <author(s)>:<title>;<description>;<year>
    
    7) Document                      

       <description>;<year>
    



    4.2 STORING BIBLIOGRAPHICAL DATA (STORE, SET, DELETE, MODIFY, SHOW) 


    Data about a publication (a bibliographical unit) are  stored  by  the
    command  

       STORE [<language>] <publication type> [:]
    
             <description of the publication>
    
             [ ABOUT <key phrase> [[,] <key phrase>]...(4)   ]***
             [                                               ]
             [ REVIEWED [IN] <review description>            ]
             [                                               ]
             [ [WITH] THEOREMS [<i-value>]...                ]    .
             [                                               ]
             [ {REFERING [TO]} [PUBLICATIONS] [<i-value>]... ]
             [ {CONTAINING   }                               ]
             [                                               ]
             [ CITED [IN] [PUBLICATIONS] [<i-value>]...      ]
    
    
    Language is one of the following: BULGARIAN,  CHINESE,  CZECH,  DUTCH,
    ENGLISH,  FRENCH,  GERMAN,  HUNGARIAN,  ITALIAN,   JAPANESE,   POLISH,
    ROUMANIAN, RUSSIAN, SERBO CROATIAN, SPANISH. 

    Description of a publication is described in Section 4.1.  The  number
1
                                   - 4.3 -

    of key phrases is at most 5. If the system does not know some words in
    key phrases it will ask for grammatical types of new words.  

    The review description is related to the data about review journals in
    which the publication is reviewed. The  following  three  main  review
    journals are forseen:  

       Mathematical Reviewshech (MR) ,
       Zentralblatt fur Mathematik (ZB) ,
       Referativny Zurnal Matematika (RZ) .
    
    Reference to MR is of the following form  

       before 1980: MR<volume number><review number>
       since  1980: MR<volume number><issue letter><section number>
                    <review number>
    
    For other review journals we have the following descriptions:  

       before 1980: ZB<volume number><review number>
       since  1980: ZB<volume number><section number><review number>
    
              RZ <year><issue number><section letter><review number>
    
    All the data should be separated by blanks or/and commas. For example,
    the review description of a paper reads:  

       MR 43, 7356, ZB 204, 245, RZ 1971, 9 V 357
    
    Theorems  are  given  by  sequence  of  their  identification  numbers
    refering to the file of theorems in the THEOR part (see Chapter 6). 

    Refering to cited paper is done  by  means  of  the  sequence  of  the
    identification numbers of the cited paper. 

    The same holds for publications in which  the  stored  publication  is
    cited.  

    Identification numbers are typed with blanks between them. 

    The order of non-obligatory options (except for the language)  in  the
    command is arbitrary. 

    When storing the new data it is useful to  know  how  the  system  has
    memorized authors, publishers,etc., and to type  them  always  in  the
    same way. Such data can be obtained by the command 

            {AUTHORS    }
       SHOW {JOURNALS   } [BEGINNING [WITH] <string>] .
            {PUBLISHERS }
            {KEY_PHRASES}
    
    
    Authors, manuals,  publishers  and  key  phrases  obtain  an  internal
    identification number. The above command provides the user with  these
    identification  numbers  if  the   following   command   is   executed
    previously: 

1
                                   - 4.4 -

       SET MODE [OF] SHOWING [TO] 1 .
    
    
    The default value of this  mode  is  equal  to  0  in  which  case  no
    identification numbers will be displayed. 

    Identification numbers  for  authors,  journals,  publishers  and  key
    phrases may be used in  the  STORE  command  instead  of  the  textual
    description of these objects. In this case a symbol # should  be  used
    just in front of each identification number. 

    By the command 

       DELETE PUBLICATIONS [<i-value>]... .
    
    
    the publications with the  identification  numbers  from  the  integer
    sequence will be deleted from the data base. 

    By the command 

       DELETE {AUTHORS    } <string> .
              {KEY_PHRASES}
    
    
    the  given  authors  or  key  phrases  will  be   deleted   from   the
    corresponding files. They will  not  be  deleted  if  there  are  some
    publications refering to them. The authors and key phrases  should  be
    separated by commas. 

    There is a command for modifying the data 

1
                                   - 4.5 -

    MODIFY [THE] PUBLICATION <i-value> REPLACING
    
        {[;]LANGUAGE [BY] <language>                                }***
        {                                                           }
        {   {FIRST_PAGE_NUMBER}                                     }
        {   {ISSUE_NUMBER     }                                     }
        {   {LAST_PAGE_NUMBER }                                     }
        {[;]{PROCEEDING_NUMBER} [BY] <i-value>                      }
        {   {VOLUME_NUMBER    }                                     }
        {   {SIZE             }                                     }
        {   {YEAR             }                                     }
        {                                                           }
        {[;] PREFACE_SIZE {<i-value>}                               }
        {                 {<string> }                               }
        {                                                           }
        {   {DESCRIPTION       }                                    }    .
        {   {JOURNAL_NAME      }                                    }
        {[;]{REVIEW_DESCRIPTION} [BY] <string>                      }
        {   {TITLE             }                                    }
        {                                                           }
        {[;]{AUTHORS   } [<old string>] BY <new string>             }
        {   {PUBLISHERS}                                            }
        {                                                           }
        {[;]KEY_PHRASES [<old string> [,<old string>]...(4)]        }
        {                                                           }
        {               BY <new string> [,<new string>]...(4)       }
        {                                                           }
        {   {CITING_PUBLICATION     }                               }
        {[;]{REFERENCED_PUBLICATIONS}[<i-value>]... BY{<i-value>}...}
        {   {THEOREMS               }                               }
    
    
    Language my be one of the following: BULGARIAN, CHINESE, CZECH, DUTCH,
    ENGLISH,  FRENCH,  GERMAN,  HUNGARIAN,  ITALIAN,   JAPANESE,   POLISH,
    ROUMANIAN, RUSSISAN, SERBO CROATIAN, SPANISH.  




    4.3 FINDING PUBLICATIONS (FIND, TYPE, ENUMERATE, FORGET, SORT) 


    The user can force  the  system  to  find  identification  numbers  of
    previously stored publications which fullfil certain requirements.  

    The corresponding command reads  

       FIND [<language>] <publication type> [BY <authors or editors>]
    
            [ABOUT <key phrase> [, <key phrase>]...(4)
    
            [[FROM] YEARS <year> [TO [YEAR] <year>]]
    
            [[WITH] THEOREMS [<i-value>]... ] .
    
    
    Publication types can be PUBLICATIONS in general or special  kinds  of
    publications as given in 4.1. 

    Years are  given  by  one  or  two  integers.  One  integer  specifies
    particular year and two integers determine a period of time.  
1
                                   - 4.6 -


    The  order  of  non-obligatory  options,  except  for   language,   is
    arbitrary. 

    Identification numbers of publications which satisfy the  requirements
    of the last command are internally memorized by the system.  The  user
    can get these numbers by the command  

       TYPE IDENTIFICATION [NUMBERS] .
    
    
    The number of publications found will be obtained by the command 

       ENUMERATE [PUBLICATIONS] .
    
    
    The publications found will be typed by the instruction  

       TYPE PUBLICATIONS .
    
    
    If the user wants to have typed only publication  with  identification
    numbers given, he will use the command  

       TYPE PUBLICATIONS {<i-value>}... .
    
    
    There are three modes of typing publications: 0 for typing only  basic
    data about a publication, 1 basic data and  references  to  referative
    jornals are typed, 2 all the data about a publication are  typed.  The
    mode of typing can be chosen by the command 

       SET MODE [OF] TYPING PUBLICATIONS [TO] <i-value> .
    
    
    After starting the system "Graph", the mode will be set to 0. 

    After the command  

       FIND PUBLICATIONS {<i-value>}... .
    
    
    the  system  will  check   whether   there   are   publications   with
    identification numbers given. Nonexisting identification numbers  will
    be forgotten and the others internally memorized.  

    If several FIND-commands (described in this section) are performed one
    after another, the system will memorize the union of the sequences  of
    identification numbers found by particular commands. 

    If the  user  wants  to  reduce  internally  memorized  identification
    numbers, he can use the command  

       FORGET PUBLICATIONS .
    
    
    to cancel everything or the command  

1
                                   - 4.7 -

       FORGET PUBLICATIONS {<i-value>}... .
    
    
    to cancel some particular publications. 

    The publications found by the system can be sorted by the command 

       SORT PUBLICATIONS [BY] {AUTHORS} .
                              {YEARS  }
    
    
    By the command 

       FIND KEY_PHRASES [CONTAINING] <string> .
    
    
    the user can get key phrases each containing at least  one  word  from
    the string. Finally, there is an option  

       FIND [<f-name>] THEOREMS [OF] [REFERENCE] <i-value> .
    
    
    to  get  theorems  mentioned  in  the   publication   with   a   given
    identification number. 


1








    5 GRAPH PROCESSING 






    5.1 INTRODUCTION 


    In this chapter the usage of the possibilities of  the  subsystem  for
    solving problems on particular graphs ALGOR is described. 

    Objects, that are manipulated within ALGOR are graphs, values  of  the
    type integer, real and  complex,  and  families  of  sets  of  integer
    values. 

    All tasks the user can execute within graph processing can be  devided
    into the following groups: 

    a) manipulative tasks (setting and displaying values of the  mentioned
       objects), 
    b) creating common graphs (e.g. complete graphs,  circuits,  etc.)  or
       random graphs, 
    c) creating graphs by  performing  graph  theoretic  operations  (e.g.
       complement of a graph, product of two graphs, etc.), 
    d) relabelling (points or lines of) graphs (by given  permutation,  at
       random etc.), 
    e) determining integer invariants in a  graph  (e.g.  number  of  some
       subgraphs, order of some point, etc.), 
    f) determining  real  invariants  of  a   graph   (e.g.   eigenvalues,
       eigenvectors, etc), 
    g) checking properties of graph(s) (e.g. whether a  graph  is  planar,
       whether two graphs are isomorphic, etc.) and  
    h) listing families of  graph  characteristics  (e.g.  point  degrees,
       components, etc.). 

    Each group is characterized by a verb in  the  corresponding  commands
    and by the type of the output. 

    In the successive sections the GTCL commands for the above  groups  of
    tasks are described in details. 

    If some keywords or parts of commands are given in parentheses  (...),
    the corresponding subroutine has not yet been installed. 




    5.2 MANIPULATIVE TASKS 


    In this section only the manipulative tasks that are specific  to  the
    objects of ALGOR are  described.  These  are  setting  values  of  the
    objects and presnting their values to the  user.  Manipulative  tasks,
    common to all objects of the whole  system  "Graph"  (such  as  making
1
                                   - 5.2 -

    copies, deleting, etc.), are described in Chapter 7 . 



    5.2.1 Setting values (SET) 

    Next commands of GTCL allows the user to assign particular values to a
    variable of the selected type. Variable with the same name  and  type,
    as that in the command, must not exist in the memory. 

       SET <g-name> = ( <np> [,] <nl> ) [<list of pairs of points>] .
    
           <list of pairs of points> ::= <i> <j> [, <i> <j>]...
    
           <np> - number of points (integer value 1,2,...).
           <nl> - number of lines (integer value 0,1,2,...).
           <i> <j>  - pair of points which are connected by a line
                      (integer values 1,2,...,<np>).
    
    
           Example: SET G5 = ( 3 2 ) 1 2 , 2 3 .
    
    
       SET <f-name> = [<integer set> [, <integer set>]...] .
    
           <integer set> ::= [<i-value>]...
    
    
           Example: SET F15 = 1 3 7 , 4 8 , 2 5 .
    
    
       SET <i-name> = <i-value> .
    
    
           Example: SET NX = 32 .
    
    
       SET <r-name> = <r-value> .
    
    
           Example: SET ALPHA = -135.72E-4 .
    
    
       SET <c-name> = <c-value> .
    
    
           Example: SET CX1 = ( 3.5 , -1.2 ) .
    
    When setting graphs, families or sentences the system will require the
    user to type a new name of the object if the name in  the  command  is
    already used in the system. 



    5.2.2 Typing Values (TYPE) 

    Current values of graphs,  families  and  integer,  real  and  complex
    variables are presented to the user by command of GTCL: 

1
                                   - 5.3 -

       TYPE <name> .
    
    
            <name> - name of the variable whiches value is to be typed. An
                     error message will appear  if  the  variable  of  the
                     given type and name doesn't exist in the memory. 

       Examples: TYPE G13 .
                 TYPE GRAPH X .
                 TYPE F15 .
                 TYPE N .
    
    



    5.2.3 Interactive Drawing of Graphs (SET, MODIFY) 

    A special feature of the system "Graph" is creating new  graph  (SET),
    or modifying an existing graph (MODIFY) in the memory  by  interactive
    drawing the graph on the screen of the graphics display. This  feature
    requires appropiate hardware and software support. 

    For the present version of the system  GRAPH,  the  required  hardware
    support is a Tektronix  4105  graphics  terminal,  and  no  additional
    software is required. Due to the upward compatibility, greater  models
    of the Tek 4100 series can be used, too. 

    The process  of  interactive  drawing  is  initiated  by  one  of  the
    following commands of the GTCL: 

       SET <g-name> .
    
       MODIFY <g-name> .
    
    
    An error message will appear, in the case of SET, if a graph with  the
    same name already exists in the memory, or, in the case of MODIFY,  if
    the graph with the given name doesn't exist in the memory. 

    The process of the interactive drawing of the graph, which  is  beyond
    the scope of GTCL, is as follows. 

    First of all system "Graph" sets the initial picture on the screen  of
    the graphical display as shown on the Figure 5.2-1. 

1
                                   - 5.4 -

    
       ################################################################
       # name(np,nl)                                       Insert     #
       # .----------------------------------------------.  Move       #
       # |                                              |  Delete     #
       # |                                              |             #
       # |                                              |  Line       #
       # |                                              |  Point      #
       # |                                              |             #
       # |                                              |  Select     #
       # |                                              |  Go         #
       # |                                              |  Refresh    #
       # |                                              |  Finish     #
       # |            picture of the graph              |             #
       # |                                              |  [error]    #
       # |                                              |             #
       # |                                              |  .--------. #
       # |                                              |  |numeric | #
       # |                                              |  |        | #
       # |                                              |  |keypad  | #
       # |                                              |  |        | #
       # |                                              |  |template| #
       # `----------------------------------------------'  `--------' #
       # .----------------------------------------------------------. #
       # |                                                          | #
       # |                                                          | #
       # |                    dialogue on the GTCL                  | #
       # |                                                          | #
       # |                                                          | #
       # `----------------------------------------------------------' #
       ################################################################
    
                            Figure 5.2-1  

    A smaller (lower) part of the screen holds the last several  lines  of
    the dialogue on the GTCL. After terminating the  interactive  drawing,
    the succeeding lines of  the  dialogue  will  appear  here,  too,  not
    overlapping the picture of the graph. 

    The most part of the screen is used to show the picture of the  graph.
    At the beginning, in the case of SET, this area is empty. In the  case
    of MODIFY the picture of the old graph is drawn  here.  The  graph  is
    drawn exactly as it looked like last time when it was created  by  SET
    or modified by MODIFY,  unless  the  coordinates  of  the  point  were
    forgotten (see Section 5.2.5) in which case the points are placed into
    the vertices of a regular polygon. Graphs created in some another  way
    (see, for example, Sections 5.2.1, 5.3 and 5.4) are drawn in the  same
    way. 

    In the upper left corner of the screen the name of the graph  and  the
    current number of points (np) and lines (nl) is shown. 

    The keywords used during the interactive drawing are  displayed  along
    the right edge of the  screen.  These  keywords  denote  the  possible
    operations (Insert, Move, Delete), types of objects (Point, Line), and
    commands (Select, Go, Refresh, Finish). 

    One way to mark a keyword is to press the  key  of  the  alpha  keypad
    denoted by the initial letter of the keyword. Another way is to  press
    the appropriate key on the numeric keypad. The template of the numeric
    keypad keyword layout is shown on the screen by the right edge of  the
1
                                   - 5.5 -

    screen, just below the list of the keywords. 

    Marked keywords appear in different colour  from  the  colour  of  the
    unmarked keywords. The actual colour depends  on  the  set-up  of  the
    terminal, which can be done manually in the terminal's set-up mode. If
    the factory set-up is in effect, the colour of the  unmarked  keywords
    is cyan and of the marked keywords is magenta. 

    Graphical informations are entered  by  means  of  the  crossing  hair
    cursor. The crossing hair cursor is represented by a  vertical  and  a
    horizontal line accross the whole screen, the crossing point of  which
    denotes the current position  of  the  cursor.  The  position  of  the
    crossing hair cursor  can  be  moved  accross  the  screen  simply  by
    pressing the octogonal joy-disk at the appropriate edge (eg.:  at  the
    right edge for movement to the right). To speed up the movement of the
    crossing hair cursor, one has to hold down one of the  shift  keys  on
    the alpha keypad during the manipulations with the joy-disk. 

    To select any object in the graph (a point or a line), one has to move
    the crossing hair cursor over the object (to any place inside a point,
    or along a line), and mark the keyword "Select".  The  marked  objects
    change their colour signalizing that they will be acted  on  when  one
    marks the keyword "Go". 

    For the factory set-up, the  unselected  points  are  white,  and  the
    colour of the selected points is magenta.  The  unselected  lines  are
    red, and the colour of the selected lines is cyan. 

    At the beginning the keywords "Insert" and  "Point"  appear  different
    from the  others,  denoting  that  the  operation  "insert  point"  is
    selected. To change the operation  and  the  type  of  object(s),  the
    appropriate keywords must be marked. The next  events  depend  on  the
    choice made: 

    Insert/Point: Move the crossing hair cursor to the desired place. 

       Mark the keyword "Go". A point  will  appear  on  the  screen  with
       center in the denoted place. 

       Error condition occurs, if the selected place for the point is  too
       close to any existing point. 

    Insert/Line: Select two points of the graph. The  points  will  change
       their colour. 

       Mark the keyword "Go". A line  between  the  selected  points  will
       appear. 

       Error condition occurs if there is only one selected point  at  the
       moment when the "Go" is marked. 

       To insert a loop at some point mark the point twice  and  mark  the
       keyword "Go". The loop will  be  represented  by  a  vertical  line
       accross the point. 

    Move/Point: Select the point to be moved to a new place. The point and
       all coinciding lines will change their colour. 

       Move the crossing hair cursor to the desired place. 

       Mark the keyword "Go". The point and the coinciding lines  will  be
1
                                   - 5.6 -

       redrawn with the center of the point in the selected place. 

       Error condition occures if no point is selected,  or  the  selected
       new place is too close to any of the other  points  (excluding  the
       selected one) of the graph. 

    Move/Line: Not allowed. Error condition occures if one tries to select
       this combination. 

    Delete/Point: Select the point to be deleted. The selected  point  and
       all coinciding lines will change their colour. 

       Mark the keyword "Go". The selected point and all coinciding  lines
       will disappear. 

       Error condition occures if no point is selected at the  moment  the
       "Go" is marked. 

    Delete/Line: There are several possibilities to procceed. 

       a) Mark the desired line. The line will change its colour. 

          Mark the keyword "Go". The selected line will disappear from the
          screen. 

       b) Select a point. All lines cionciding to the  point  will  change
          their colour. 

          Select one of those lines, or the point at the other end of  one
          of those lines. All but the selected line will return  to  their
          original colour. 

          Mark the keyword "Go". The selected line will disappear from the
          screen. 

       c) Select a point. All lines coinciding to the  point  will  change
          their colour. 

          Mark the keyword "Go". All selected lines  will  disappear  from
          the screen. 

       Error condition occurs if there is no selected line at  the  moment
       the "Go" is marked, or if the second selected point in  b)  doesn't
       coincide with any of the selected lines. 

    At any time, if error condition occurs, a keyword "ERROR" will  appear
    under the list of keywords by the right edge of the screen.  To  reset
    the error condition, the keyword "ERROR" must be marked. 

    To cancel the selection of  object(s)  with  no  action,  any  keyword
    (except "Select", "Go", "Refresh" and "Finish") is  to  be  marked.  A
    redundant selection of a selected keyword will satisfy if no change of
    operation or object type is needed. 

    During the operations "Move" and "Delete", the lines and the points on
    the screen may  become  interrupted  with  black  gaps.  This  happens
    because deleting of an object is actually  done  by  redrawing  it  in
    black colour. Refreshing the picture without these gaps is achieved by
    marking the keyword "Refresh". Any selected  objects  in  the  picture
    remain selceted after refreshing. 

1
                                   - 5.7 -

    Termination of the interactive drawing of a graph achieved by  marking
    the keyword "Finish". The keyword "Finish" will change its colour, and
    all other objects (keywords, points, and lines) will return  to  their
    original colour. 

    To clear the picture from the screen, use the command "DRAW ." of  the
    GTCL (see the next section). 



    5.2.4 Drawing Graphs (DRAW) 

    Special feature of the system "Graph" is  drawing  the  picture  of  a
    graph, existing in the memory, on the screen of the graphics  display.
    This feature requires appropiate hardware and software support. 

    For the present version of the system  GRAPH,  the  required  hardware
    support is a Tektronix  4105  graphics  terminal,  and  no  additional
    software is required. Due to the upward compatibility, greater  models
    of the Tek 4100 series can be used, too. 

    The drawing of a graph is achieved with the command of the GTCL: 

       DRAW <g-name> .
    
    
    The screen will be arranged in the same way as shown in the  Figure 5.
    2-1, except that the keywords and the numeric  keypad  template  along
    the right edge will not be shown. 

    If the graph was created or modified interactively (see  the  previous
    section) and the coordinates of the points are not forgotten (see  the
    next section), it will be drawn in the same way  as  it  was  earlier.
    Otherwise, if the coordinates were  forgotten  or  the  graph  is  not
    handled interactively (i.e. it is created by the commands of the  GTCL
    from Sections 5.2.1, 5.3, and 5.4) the points of  the  graph  will  be
    drawn on the vertices of a regular polygon. 

    An error message will appeare if the desired graph  doesn't  exist  in
    the memory. 

    The picture of the graph remains on  the  screen  until  some  another
    graph is drawn (with DRAW, SET or MODIFY), or the picture  is  cleared
    from the screen by the command of the GTCL: 

       DRAW .
    
    
    After this command the whole screen is used to show  the  dialogue  on
    the GTCL. 




    5.2.5 Forgetting Coordinates (FORGET) 

    In the lack of space in the  memory,  some  space  can  be  freed  up,
    without the loss essential informations, by forgetting coordinates  of
    graph(s). This is achieved by the command of the GTCL: 

1
                                   - 5.8 -

       FORGET COORDINATES [OF] <g-name> .
    
    
    After forgetting the coordinates of a graph,  it  will  be,  with  the
    commands DRAW and MODIFY, drawn with the points placed on the vertices
    of a regular polygon. 



    5.2.6 Splitting Families (MODIFY) 

    A family of sets of integers can be split into several  families  each
    containing one of these sets. The corresponding command reads: 

       MODIFY [THE] <f-name> [BY] [SPLITTING] .
    
    
    The system will generate the names of the new families. 



    5.2.7 Sorting Objects (SORT) 

    Families, graphs and reals can be sorted in the memory by the command 

         {(FAMILIES [<name>])                      }
         {                                         }
         {                     {(DEGREES         )}}
    SORT { GRAPHS [<name>] [BY]{ EIGENVALUES      }} [INTO <prefix>] .
         {                     {(SPECTRAL_MOMENTS)}}
         {                                         }
         { {INTEGERS} [<name>] [BY] [VALUES]       }
         { {REALS   }                              }
    
    
    The names can contain wildcard characters and all objects of the given
    type whose names fit name mask will me sorted. If no name is given all
    objects of the given type will be treated. The objects will be  sorted
    under newly generated names with the given prefix. If  the  prefix  is
    not given,  the  old  names  will  be  used.  Graphs  will  be  sorted
    lexicographically by the selected invariants. 





    5.3 CREATING GRAPHS OF COMMON STRUCTURE (CREATE) 


    By algorithms from this group we create graphs  which  are  frequently
    used. The output is a graph and in the corresponding commands  we  are
    obliged to give a name to the created graph. The input is  an  integer
    defining the order of the graph which is created. 

    The characteristic verb in these commands is CREATE. 

    Commands have the following form: 

1
                                   - 5.9 -

       CREATE <g-name> [AS] <type of graph> [OF] [ORDER] <integer> .
    
    
    Possible types of the graph  are:  CIRCUIT,  COCTAIL PARTY,  COMPLETE,
    CUBE, MOBIUS LADDER, PATH, PRISM, RANDOM, (RANDOM TREE), STAR, WHEEL. 

       Example: CREATE G1 CIRCUIT OF ORDER 37 .
    
    



    5.4 CREATING GRAPHS BY GRAPH THEORETIC OPERATIONS (FORM) 


    The algorithms from this group create new graphs by starting from some
    previously  defined  graphs  and  performing  some   graph   theoretic
    operations  on  them.  Hence  the  output  is   always   a   graph.The
    characteristic verb in these commands is FORM. 

    There are the following subgroups: 

    a) unary operations, 
    b) unary operations with a parameter, 
    c) binary opertions, 
    d) operations defined by a point set or  line set, 
    e) operations defined by a point, and 
    f) operations defined by a line. 



    5.4.1 Unary Operations 

    In this subgroup of algorithms the input is the name of a  graph.  The
    algorithms always perform a unary graph operation so that a new  graph
    results. 

    Form of commands: 

       FORM [<g-name>] [AS] <operation> [GRAPH] [OF] <g-name> .
    
    
    Operations  are  the  following:  BASIS,  (BLOCK),  (BLOCK CUT POINT),
    (CLIQUE), CLOSED NEIGHBOURHOOD,  COMPLEMENT,  (CUT POINT),  (DIGRAPH),
    INVERSE LINE,   LINE,   LOOP,   OPEN NEIGHBOURHOOD   (PSEUDO INVERSE),
    REDUCED, SEMI TOTAL POINT, SEMI TOTAL LINE, SKELETON, SQUARE, TOTAL. 

       Examples: FORM H AS COMPLEMENT OF G .
                 FORM LINE GRAPH OF G1 .
    
    
    EXPLANATION OF NON-STANDARD TERMS. Basis  of  a  graph  is  the  graph
    obtained from this graph by deleting all loops. Skeleton  is  obtained
    by deleting loops and replacing multiple lines  with  a  single  line.
    Digraph of a graph is the digraph with the same adjacency matrix. Loop
    graph of a graph is obtained by adding a new loop to each  point.  The
    reduced graph of a graph is the smallest  homeomorphic  image  of  the
    graph. The reduced graph of a graph is the smallest homeomorphic image
    of the graph. 


1
                                   - 5.10 -



    5.4.2 Unary Operations with a Parameter 

    The input consists of a graph, given by its name, and  of  an  integer
    given by the name or value. The integer  serves  as  a  parameter  for
    defining a unary graph operation. 

    The commands have the following form: 

       FORM [<g-name>] [AS] [THE] <integer> [TH] <operation> [GRAPH]
    
            [OF] <g-name> .
    
    
    Possible  operations  are:  DISTANCE,  (PATH),   POWER,   SUBDIVISION,
    (TRAIL), (WALK). 

       Example: FORM H AS THE 4 TH SUBDIVISION GRAPH OF G .
    
    
    There are also the following commands: 

       FORM [<g-name>] [AS] [THE] <integer> [FOLD] UNION [OF] <g-name> .
    
    
       FORM [<g-name>] [BY] ADDING <integer> [ISOLATED] [POINTS]
    
            [TO] <g-name> .
    
    


    5.4.3 Binary Operations 

    Algorithms from this subgroup perform  operations  on  two  graphs  to
    create a new graph. Hence, the input consists of two graphs  (possibly
    not distinct) given by their names and the output is a graph. 

    Commands are the following form: 

       FORM [<g-name>] [AS] <operation> [OF] <g-name> [AND] <g-name> .
    
    
    Possible operations are: CORONA, JOIN, LEXICOGRAPHIC PRODUCT, PRODUCT,
    STRONG PRODUCT, SUM, UNION. 

       Examples: FORM G PRODUCT OF G1 AND G2 .
                 FORM SUM H1 H2 .
    
    


    5.4.4 Operations Defined by a Point Set or Line Set 

    The input is a graph and a set of points or lines, given by  a  family
    whose only member is a set of integers representing points  or  lines.
    Usually, we form a subgraph or supergraph in this way. 

    Commands are of the following form: 

1
                                   - 5.11 -

       FORM [<g-name>] [AS] <option> <f-name> .
    
    
    Possible options are: 

    a) SUBGRAPH [OF] <g-name> INDUCED [BY] {POINTS}
                                           {LINES }
    
    b) SUBGRAPH [OF] <g-name> [BY] CONTRACTING [POINTS]
    
    c) SUBGRAPH [OF] <g-name> [BY] DELETING {POINTS}
                                            {LINES }
    
    d) SPANNING [SUBGRAPH] [OF] <g-name> [BY] {DELETING} [LINES]
                                              {KEEPING }
    
    e) SUPERGRAPH [OF] <g-name> [BY] {ADDING [LINES]  }
                                     {JOINING [POINTS]}
    
    f) [BY] SWITCHING <g-name> [W.R.T.] [POINTS]
    
    g) {GENERALIZED_LINE} [GRAPH] [OF] <g-name> [BY]
       {PERMUTATION     }
    
       Example: FORM G SUBGRAPH OF H INDUCED BY POINTS F .
    
    


    5.4.5 Operations Defined by a Point 

    The input is a graph, given by its name, and a point  of  this  graph,
    given by an integer name or integer value. The output is a new graph. 

    Commands have the following form: 

       FORM [<g-name>] <option> <g-name> .
    
    
    Possible options are: 

    a) [BY] ADDING {LOOP} [TO] [POINT] <integer> [IN]
                   {LINE}
    
       Example: FORM H BY ADDING LOOP TO POINT 3 IN G .
    
    
    b) [BY] DELETING {PENDANT [LINE]} [AT] [POINT] <integer> FROM
                     {  LOOP        }
    
       Example: FORM H BY DELETING LOOP AT POINT K FROM G .
    
    
    c) [BY] DELETING POINT <integer> FROM
    
       Example: FORM H BY DELETING POINT 35 FROM G .
    
    
    d) [BY] ISOLATING [POINT] <integer> [BY] [SWITCHING] [IN]
    
       Example: FORM H BY ISOLATING POINT 7 BY SWITCHING IN G .
1
                                   - 5.12 -

    
    


    5.4.6 Operations Defined by a Line 

    The input is a graph, given by its name, and a  line  of  this  graph,
    given by an integer name or value. Also the line can be given  by  its
    two end points and they again can be given by integer names or values.
     Commands have the following form: 

       FORM [<g-name>] <option> <integer> [<integer>] [FROM] <g-name> .
    
    
    Possible options are [BY] CONTRACTING [LINES], BY  DELETING  LINE,  BY
    DELETING ALL LINES, SUBDIVIDING [LINES]. 

       Example: FORM H BY DELETING LINE 3 4 FROM G .
    
    



    5.5 RELABELLING GRAPHS (RELABEL) 


    The verb RELABEL is used to relabel points or lines of  a  graph.  The
    input graph, given by its name will be changed (relabelled). Therefore
    the user should copy the same graph under another name if he wants  to
    keep the old labelling (see Chapter 7). 

    The permutation which is applied on a  graph  can  be  given  under  a
    family name or described implicitly. In the first  case  we  have  the
    following options: 

                                            {PERMUTATION  }
       RELABEL {POINTS } [OF] <g-name> [BY] {C-PERMUTATION} <f-name> .
               {LINES  }                    {CYCLICALLY   }
                                            {STARTING_BY  }
    
    
    In the first option a permutation is given as a one member family.  In
    the case of C PERMUTATION the permutation is given in cyclic form with
    each cycle being a member of the family. In the third case the  family
    consists of only one member with one element - that is the step of the
    cyclic permutation. In the last option the one member  family  defines
    the objects relabelled (points or lines) which should be  permuted  so
    that they get the least possible labels. 

    In the second group we have the following possibilities 

       (RELABEL {POINTS} [OF] <g-name> [AT] <kind of permutation> .)
       (        {LINES }               [BY]                        )
    
    
    where  the  kind  of  permutation  is  determined  by  the   following
    CANNONICALLY, COLOURS, COMPONENTS, DEC-DEGREES  (decreasing  degrees),
    INC-DEGREES (increasing degrees), RANDOM. 



1
                                   - 5.13 -




    5.6 DETERMINING INTEGER GRAPH INVARIANTS (DETERMINE) 


    The output is an integer in this group  of  algorithms.  This  integer
    represents a graph invariant or an invariant of a point of the  graph.
    The characteristic verb in commands  is  DETERMINE  .  There  are  the
    following subgroups: 

    a) Invariants of the graph
    b) Invariants of a point of the graph
    c) Invariants of a given size
    d) Invariants of two points of the graph
    
    


    5.6.1 Invariants of the Graph 

    The input is a graph determined by its name. 

    The corresponding command has two forms. The first one is 

       DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] <objects>
    
                 [OF] <g-name> .
    
    
    The following objects are possible: (AUTOMORPHISM),  BLOCKS,  BRIDGES,
    CENTRAL POINTS,   (CIRCUITS),   CLIQUES,   (COCLIQUES),    COMPONENTS,
    CUTPOINTS, (INDEPENDENT LINES), LINES, LOOPS, MAX DEGREE,  MIN DEGREE,
    (ORBITS), PENDANT LINES, (PENTAGONS), POINTS, QUADRANGLES, TRIANGLES. 

    The second form reads: 

       DETERMINE [<i-name>] [AS] [THE] <invariant> [OF] <g-name> .
    
    
    Possible   invariants   are:   (CHROMATIC CLASS),   (CHROMATIC INDEX),
    CHROMATIC NUMBER,   CIRCUMFERENCE,   (CLIQUE NUMBER),    (COARSENESS),
    (COMPLEXITY),  (CROSSING NUMBER),  CYCLOMATIC NUMBER,   (DETERMINANT),
    DIAMETER, (EXTERIOR STABILITY), (GENUS), GIRTH,  (INTERIOR STABILITY),
    (LINE CONNECTIVITY), (PERMANENT), (POINT CONNECTIVITY), RADIUS,  RANK,
    (THICKNESS). 

       Examples: DETERMINE THE NUMBER OF TRIANGLES OF G .
                 DETERMINE JD DIAMETER OF H .
    
    


    5.6.2 Invariants of a Point 

    The input is a graph,  given  by  name,  and  a  point  of  the  graph
    determined by an integer name or by an integer value. 

    Commands have the following forms: 

1
                                   - 5.14 -

       DETERMINE [<i-name>] [AS] [THE] <invariant> [OF] [POINT] <integer>
    
                 [OF] <g-name> .
    
    
    Possible invariants: DEGREE, ECCENTRICITY. 

       DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] <objects>
    
                 [CONTAINING] [POINT] <integer> [OF] <g-name> .
    
    
    Integer name or value  determines  a  point  in  the  graph.  Possible
    objects: (CIRCUITS), (CLIQUES), (COCLIQUES), LOOPS, TRIANGLES. 

       DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] POINTS SIMILAR
    
                 [TO] <integer> [OF] <g-name> .
    
    
       Examples: DETERMINE DEGREE OF 7 OF G .
                 DETERMINE NC THE NUMBER OF CIRCUITS CONTAINING K OF H3 .
                 DETERMINE THE NUMBER OF POINTS SIMILAR TO 2 OF GH33 .
    
    


    5.6.3 Invariants of a Given Size 

    The input is a graph, given by name,and an integer given by a name  or
    by a value. 

       DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] <objects>
    
                      {DEGREE}
                 [OF] {LENGTH} <integer> [OF] <g-name> .
                      {SIZE  }
    
    
    Objects: CIRCUIT, (CLIQUES), (COCLIQUES),  LINES,  MATCHINGS,  (PATHS)
    POINTS, (TRAILS), (WALKS). 

       Examples: DETERMINE THE NUMBER MATCHINGS OF SIZE K OF G .
                 DETERMINE THE NUMBER OF POINTS OF DEGREE 3 OF H .
    
    


    5.6.4 Invariants of two points 

    The input is a graph given by name and two points given by integers or
    by names. 

       DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] <objects> BETWEEN
    
                 [POINTS] <integer> [AND] <integer> [OF] <g-name> .
    
    
    Possible  objects   are:   (CIRCUITS CONTAINING),   COMMON NEIGHBOURS,
    (DISJOINT PATHS),  DISTANCE,  LINE LABEL,   LINES INCIDENT,   (PATHS),
    (TRAILS), (WALKS) . 
1
                                   - 5.15 -





    5.7 DETERMINING REAL GRAPH INVARIANTS (CALCULATE) 


    The algorithms from this group determine graph  invariants  which  are
    real numbers. The input is a graph, given by its name, and the  output
    is a real number. 

    Commands have the following form: 

       CALCULATE [<r-name>] [AS] [THE] <invariant> [OF] <g-name> .
    
    
    Possible invariants are: (ADMITTANCE SPECTRUM), (ANGLES), BOND ORDERS,
    CHARGES,     DISTANCE INDEX,     (DISTANCE SPECTRUM),     EIGENVALUES,
    EIGENVECTORS, ENERGY, (MAIN ANGLES), (R-SPECTRUM), SEIDEL SPECTRUM. 

       Example: CALCULATE EIGENVALUES OF G .
    
    



    5.8 CHECKING GRAPH PROPERTIES (CHECK) 


    The algorithms of this group establish whether or not a  graph  (or  a
    point or a line) or two graphs has  (or  have)  some  properties.  The
    output is a logical variable, i.e. the system answers "yes" or "no". 

    The characteristic verb in commands is CHECK. 

    We have the following groups: 

    a) Checking global graph properties,
    b) Checking properties of a point in the graph,
    c) Checking properties of two graphs.
    
    


    5.8.1 Checking Global Graph Properties 

    The input for this subgroup of algorihms is a graph given by its name. 

    The commands have the following form: 

       CHECK [WHETHER] <g-name> [IS] [AN] <property> .
    
    
    Possible    properties     are:     ACYCLIC,     BIPARTITE,     BLOCK,
    (BLOCK CUTPOINT GRAPH),   (BLOCK GRAPH),   CIRCUIT,    (CLIQUE GRAPH),
    COMPLETE, CONNECTED, (CUTPOINT GRAPH), EULERIAN, FOREST,  HAMILTONIAN,
    HYPOHAMILTONIAN,     (INTERVAL GRAPH),      LINE GRAPH,      LOOPLESS,
    (MOORE GRAPH), (OUTERPLANAR),  (PERFECT),  PLANAR,  (PRIME),  REGULAR,
    (SELFCOMPLEMENTARY), (SELFDUAL), SEMI REGULAR, (SEMITOTAL LINE GRAPH),
    (SEMITOTAL POINT GRAPH),    STRONGLY REGULAR,     (SUBDIVISION GRAPH),
    (TOTAL GRAPH),     TOTALLY DISCONNECTED,     (TRAVERSIBLE),      TREE,
1
                                   - 5.16 -

    TRIANGLESFREE, TRIVIAL, UNICYCLIC, WHEEL, WITHOUT MULTIPLE LINES. 

       Examples: CHECK WHETHER G1 IS PLANAR .
                 CHECK WHETHER G2 IS A TREE .
    
    


    5.8.2 Checking Properties of a Point in the Graph 

    In this subgroups of algorithms the input is a graph given by its name
    and a point of this graph given by an integer name or integer value. 

    Commands have the following form: 

       CHECK [WHETHER] [THE] [POINT] <integer> [IS] [AN] <property>
    
             [IN] <g-name> .
    
    
    Possible properties are: CENTRAL, CUT POINT, END POINT, ISOLATED. 

       Example: CHECK WHETHER THE POINT 5 IS ISOLATED IN G .
    
    



    5.8.3 Checking Properties of Two Graphs 

    In this subgroup of algorithms we have  two  graphs,  given  by  their
    names, at the input. The algorithms establish some properties of these
    two graphs. 

    Commands are of the following form: 

       CHECK [WHETHER] <g-name> AND <g-name> [ARE] <property> .
    
    
    Possible properties are:  COSPECTRAL,  (HOMOMORPHIC),  (HOMEOMORPHIC),
    ISOMORPHIC, (SWITCHING EQUIVALENT). 

       Example: CHECK WHETHER G1 AND G2 ARE ISOMORPHIC .
    
    
    After the command 

       CHECK WHETHER G1 AND G2 ARE ISOMORPHIC .
    
    the system will split vertex sets in some equivalence classes. If they
    are of the same size for both graphs, the system starts  a  pedestrian
    check whether graphs are isomorphic, trying a number of  permutations.
    This process can be time consuming and there are some limitations: 

    If mode of loop is CONFIRM the system checks 720 permutations  and  if
    the decision has been not made it will ask the user  for  approval  of
    continuing the working. Each time the  user  allows  the  system  will
    check next 720 permutations. In the NOCONFIRM mode the system will not
    ask the user anything but will check at most 10000 permutations. 


1
                                   - 5.17 -



    5.8.4 Setting Mode of Checking 

    There are three modes of checking: 0 - normal mode,  1  -  the  system
    forgets the graph if it has the  checked  property,  2  -  the  system
    forgets the graph if it has not the checked property. In the  case  of
    tasks with two graphs the second one will be forgotten. 

    The mode of checking can be set by the following command 

       SET MODE [OF] CHECKING [TO] <integer> .
    
    
    After starting the system the mode will be set to 0. 




    5.9 LISTING FAMILIES (LIST) 


    In this group of algorithms, the result is a family  of  subgraphs  or
    other characteristics of a graph (or of a point in a graph etc.). 

    The characteristic verb is LIST. 

    We have the following subgroups: 

    a) Listing families of integers,
    b) Listing families of sets.
    
    


    5.9.1 Listing Families of Integers 

    The input is a graph given by its name. The output is a  family  whose
    only member consists of integers.  These  integers  represent  certain
    subgraphs or some characteristics of the graph. 

    Commands are of the following forms: 

       LIST [<f-name>] <objects> [OF] <g-name> .
    
    
    Possible objects are: BRIDGES, (CENTRE),  CUT POINTS,  LINE COLOURING,
    (LINE DEGREES),      LINES,      POINT COLOURING,       POINT DEGREES,
    POINT ECCENTRICITIES, POINT ORBITS. 

       LIST [<f-name>] [ANY] <object> [OF] <g-name> .
    
    
    Possible objects are: (CIRCUIT), (FOREST), SPANNING TREE, (1-FACTOR). 

       LIST [<f-name>] [COEFFICIENTS [OF]] <polynomial> [OF] <g-name> .
    
    
    Possible       polynomials       are:       CHARACTERISTIC POLYNOMIAL,
    (CHROMATIC POLYNOMIAL), MATCHING POLYNOMIAL, SEIDEL POLYNOMIAL. 

1
                                   - 5.18 -



    5.9.2 Listing Families of Sets 

    The input is a graph given by its name. The output is a  family  whose
    members represnt some subgraphs. 

    Commands are of the following form: 

       LIST [<f-name>] <objects> [OF] <g-name> .
    
    
    Possible  objects  are:  BLOCKS,   (CIRCUITS),   CLIQUES,   COCLIQUES,
    COMPONENTS,  (FACES),   (HAMILTONIAN CIRCUITS),   (MAXIMAL MATCHINGS),
    (HEXAGONS),     (PENTAGONS),     POINT NEIGHBOURS,      (QUADRANGLES),
    (SEMI BLOCKS),     (SPANNING TREES),     (TRIANGLES),     (1-FACTORS),
    PARALLEL LINES, SERIAL LINES . 




    5.10 INVESTIGATING GRAPHS (INVESTIGATE) 


    The only instruction in this group reads: 

       INVESTIGATE <g-name> .
    
    
    The system will give a number of data about  the  input  graph.  These
    data are based on eigenvalues, eigenvectors and point degrees. 

    Special subsets of data can be selected by the command 

       SET MODE [OF] INVESTIGATING [TO] <i-value> .
    
    Possible values of the mode are as follows: 

    0 all data are printed; 
    1 the graph, its eigenvalues, spectral moments and coefficients of the
      characteristic polynomial are printed; 
    2 the graph, its eigenvalues, angles and main angles are typed. 
    The default value of this mode is 0. 




    5.11 FINAL REMARKS 


    The part of the system "Graph" described is primarily meant as a means
    for quick checking, disproving or making conjectures in graph  theory.
    Facilities provided by the system enable to get the answer on a  great
    number of questions on graphs of a resonable size in  a  few  seconds.
    (Of cource, what does it mean a reasonable size depends on the problem
    considered.) 

    Another situation in which the system can help is the following.  Many
    proofs in graph theory begin with  an  observation  which  proves  the
    desired statement for  all  but  a  finite  number  of  graphs.  These
    exceptional graphs are, as a rule, of a small size. The  rest  of  the
1
                                   - 5.19 -

    proof consists then in checking whether the statements hold for  these
    graphs and that can be performed with the help of the system. 

    The system "Graph" provides several possibilities to define the graph.
    The user can type it at the terminal, draw it on  the  screen  by  the
    light pen or take it from a catalogue of graphs stored in the external
    memory. He can create some  simple  graphs  (say,  complete,  circuit,
    etc.) and modify them by graph operations (e.g.  complement,  product,
    etc.) or graph transformations (e.g. by adding or deleting some points
    or/and lines). Finally, the user can create a  random  graph  (say  to
    check the validity of a conjecture in this way). 


1








    6 THEOREM PROVING 






    6.1 INTRODUCTION 


    One of the three main blocks of the system "Graph" is called THEOR and
    it contains several facilities for supporting theorem proving in graph
    theory. In fact, THEOR is a subsystem for manipulating with  sentences
    which represents assertions in graph theory. The facilities include an
    interactive (natural deduction) and a  fully  automatised  (resolution
    based) theorem prover. 

    Basic objects in the THEOR part are sentences and they  are  memorized
    under some (sentence) names  (see  Section  2.3).  Other  objects  are
    proofs and they are represented  in  the  system  as  special  chained
    rooted trees and memorized under tree names. Also families of integers
    appear with family names. 

    Defining of and manipulatin with sentences is desented in Section 6.2.
    For additional general rules for manipulating objects  in  the  system
    "Graph" see Chapter 7 . In Section 6.3 we describe the storing of  new
    definitions. Section 6.4 describes a module for  generating  sentences
    equivalent  to  a  given  sentence.  Interactive  theorem  proving  is
    described in 6.5 and automatic theorem proving in  6.6  .  Search  for
    data in several files (theorems, definitions, etc. ) is  described  in
    Section 6.7 . 




    6.2 DEFINING A SENTENCE 




    6.2.1 Entering a Sentence into the System (SET, TYPE) 

    The command for defining a sentence is of the following form: 

       SET <s-name> = "<text>" .
    
    
    If the sentence is accepted it is memorized under the  name  given  in
    the command. 

    The text of the sentence should be written in  "proper  GTCL".  Proper
    GTCL is a subset of the GTCL  (Graph  Theoretical  Computer  Language)
    which is described in Section 2.1 . On the other hand, proper GTCL  is
    a simplified and formalized subset of  English.  Sentences  of  proper
    GTCL contain English words as well as terms or formulas  expressed  by
    usual mathematical symbols. Syntax of sentences  of  proper  GTCL  and
1
                                   - 6.2 -

    syntax for terms and formulas are given in Apendix C.  

    Sentences can be typed  with  any  number  of  blanks  between  words.
    However, th first and the last character should not be  a  blank.  The
    use of commas is allowed. The user can help the system  to  understand
    the sentences by using rectangle brackets [  ...  ]  to  indicate  the
    structure of subsentences. If the part of  the  sentence  immediatelly
    after a quantifier beggins with a variable, this part should be  given
    in brackets, since the system  does  not  know  whether  the  variable
    belongs to the quantifier or to the part of  the  sentence  mentioned.
    Such words as "k-connected" should  be  typed  as  "K$CONNECTED".  The
    system considers $ as a special blank symbol and accepts  this  phrase
    as consisting of two words. 

    The system accepts the sentence if it consists of words known  to  the
    system, if it is syntactically correct and if there are no  errors  in
    using brackets or other auxilliary symbols. Otherwise, a message  will
    be given which indicates the error. 

    The English text of the  accepted  sentence  is  internally  coded  by
    integers (one integer for a word) and  can  be  decoded  back  by  the
    command: 

        TYPE <s-name> .
    
    
    If the system understands the meaning of the  sentence,  according  to
    the definitions stored, it will translate the sentence into a  formula
    of a special first  order  calculus,  called  the  Arithmetical  Graph
    Theory (AGT). The obtained predicate  formula  is  memorized  together
    with identification numbers of definitions which  have  been  used  in
    translating the sentence. The user can  see  the  translation  of  the
    sentence into AGT after typing the command: 

       TYPE TRANSLATION [OF] <s-name> .
    
    
    In AGT-formulas disjunction, conjunction and negation are  denoted  by
    .OR. , .AND. , and NOT. , respectively. The  universal  quantifier  is
    denoted by ALL and the existential one by EXT. 



    6.2.2 Maniupulations with Sentences (FORM, STORE, GET, DELETE) 

    Besides the general commands for  manipulating  with  objects  in  the
    system "Graph" (see Chapter 7 ),  we  have  the  following  additional
    options for sentences. 

    One can form  new  sentences  starting  from  defined  sentences.  The
    meaning of the following commands for some unary and binary operations
    on sentences is self-evident: 

       FORM <s-name> [AS] [THE] NEGATION [OF] <s-name> .
    
    
1
                                   - 6.3 -

                                     {integer variable}
       FORM <s-name> {[FOR]  ALL   } {point   variable} <s-name> .
                     {[THERE] EXIST} {line    variable}
    
    
       FORM <s-name> [AS] [THE] <operation> [OF] <s-name> [AND] <s-name> .
    
    In the second and in the third command we have  integer-,  point-,  or
    line-variable from proper GTCL (see Apendix C). The operation  in  the
    last command could be one of the following: CONJUNCTION,  DISJUNCTION,
    EQUIVALENCE, EXLUSIVE [DISJUNCTION], IMPLICATION. 

    The sentence obtained by these commands can be further processed  like
    any other sentence. 

    Sentences can be declared as axioms, theorems and lemmas and  sent  to
    correspoding  files  in  the  external  memory.  In  these  files  the
    sentences get internal identification numbers about which the  systems
    informs the user. Axioms, theorems and lemmas  can  be  obtained  back
    from  the  files,  as  usual  sentences,  if  the   user   gives   the
    identificatin number and  a  name  under  which  wants  to  have  this
    sentence. Finally, axioms, theorems and lemmas can be deleted from the
    corresponding files. The corresponding commands are: 

             {AXIOM  }
       STORE {THEOREM} <s-name> .
             {LEMMA  }
    
    
           {AXIOM  }
       GET {THEOREM} <i-value> [AS] <s-name> .
           {LEMMA  }
    
    
              {AXIOM  }
       DELETE {THEOREM} <i-value> .
              {LEMMA  }
    
    
    After storing, the original sentence remains in the operative  memory.
    When getting a sentence from the file a copy  of  it  remains  in  the
    file. 

    The system does not accept as axioms and lemmas  the  sentences  which
    are not translated into a formula of AGT. Definitions and  lemmas  are
    used by theorem provers.  The  file  of  theorems  can  be  filled  by
    arbitrary sentences, and is not  used  directly  in  theorem  proving.
    Usually the user gives new axioms  after  telling  the  system  a  new
    definition. Axioms which are useful in theorem proving process  should
    also be sent to the file of lemmas. Lemmas are  used  to  support  the
    proving process and the file of  lemmas  can  be  changed  before  any
    attempt of theorem proving. For example, some theorems might  be  sent
    to this file. 

    The user sends sentences to the mentioned files on his own risk  since
    the system does not checks corectness of theorems and  lemmas  or  the
    consistency of axioms. Of cource, the system  will  continue  to  work
    with false theorems and lemmas but the conclusions in theorem  proving
    could then be false. 

    A definition can be deleted by the command: 
1
                                   - 6.4 -


       DELETE DEFINITION <i-value> .
    
    
    Deleting a definition may cause deleting of other definition (based on
    the first one) and therefore the system will warn the user and display
    identification numbers of other definitions which  should  be  deleted
    before.  

    Both storing and deleting definitions are serious steps and  the  user
    should carefully think over before doing them. 

    A definition with given identification number  can  become  a  regular
    sentence with a given name by the command: 

       GET DEFINITION  <i-value> AS <s-name> .
    
    




    6.3 STORING DEFINITIONS (STORE) 


    System "Graph" is able  to  learn  by  accepting  definitions  of  new
    notions. When defining a new  notion  the  user  can  introduce  words
    previously not known to the system. After accepting a  new  definition
    the system can understand sentences containing the introduced notions. 

    A new notion is introduced by the command: 

             [BASIC      ]
       STORE [FUNCTIONAL ] DEFINITION [:] "<notion>" [,] "<definition>" .
             [OPERATIONAL]
    
    
    The notion is described by a phrase of proper GTCL which  may  include
    new words. The definition is a sentence of proper GTCL in the form  of
    an equivalence: 

               <definiendum> IFF <definiens> .
    
    
    The first word IFF in the definition splits it  into  definiendum  and
    definiens. The definiens must be a sentence which is accepted  by  the
    system. Definiendum may contain new words. Free variables in definiens
    and definiendum must be the same. The number of free variables  is  at
    most four. New words occuring in the definiendum must be contained  in
    the description of the notion. 

    When the option BASIC DEFINITION is used the meaning of  definiens  is
    irrelevant since a basic notion is introduced.  The  only  requirement
    the definiens should fullfil is that its free variables are  the  same
    as in the definiendum. 

    In functional definition the definiendum is of the form 

       <notion> IS EQUAL TO <integer variable>
    
    
1
                                   - 6.5 -

    and its translation will contain a new constant or function. 

    In operational definition the definiendum is of the form 

       X AND Y ARE ADJACENT IN <unary operation>
    or
       X AND Y ARE ADJACENT IN <binary operation>
                 OF <graph variable> AND <graph variable>
    
    
    In the second case the definiens should also contain  graph  variables
    used in the definiendum. 

    Each  definition  introduces  a  new   predicate   letter   into   AGT
    (Arithmetical  Graph  Theory).  This  predicate  letter  denotes   the
    definiendum and it is internaly generated by the system. The arguments
    of this predicate  are  free  variables  occuring  in  the  definiens.
    Predicate letters are of the form LK where L depends on the number  of
    free variables n in the following way 

             n |  0  1  2  3  4
            ---+----------------
             L |  P  Q  R  S  T
    
    
    and K is an integer generated by the system. 

    Example: 

    A basic notion of graph theory is introduced in the following way: 

       STORE BASIC DEFINITION : "JOINED",
             "X AND Y ARE JOINED BY LINE U IFF X+Y=U" .
    
    
    The sentence "X AND Y ARE JOINED BY LINE U" will  be  denoted  by  the
    predicate S1(X,Y,U) which is considered  by  the  system  as  a  basic
    predicate. 

    The notion "adjacent points" can be introduced in the following way: 

       STORE DEFINITION : "ADJACENT" , "X AND Y ARE ADJACENT IFF
             THERE EXISTS U SUCH THAT X AND Y ARE JOINED BY LINE U" .
    
    
    The sentence "X AND Y  ARE  ADJACENT"  corresponds  to  the  predicate
    R1(X,Y) whose definitions reads: 

       R1(X,Y)<=>(EXT U)S1(X,Y,U) .
    
    
    During the process of accepting a new definition the system  will  ask
    the user to indicate grammatical types of the new words. In  addition,
    the system will like to know whether the new  predicate  is  symmetric
    with respect to the first  two  arguments.  Possible  errors  will  be
    indicated by the corresponding messages. The accepted definition  will
    be stored in the file of definitions under an  identification  number.
    The structure of a record in the definition file is given in  Appendix
    D. 


1
                                   - 6.6 -




    6.4 GENERATING SENTENCES EQUIVALENT TO A GIVEN SENTENCE (GENERATE) 


    By the command 

       GENERATE SENTENCES [EQUIVALENT] [TO] <s-name>
    
                [CONTAINING "<notions>"] .
    
    
    the user  can  start  a  process  of  generating  sentences  logically
    equivalent to a given sentence. The sentence is given by its name.  At
    the end of this process the system will generate a number of sentences
    which all have the same meaning as  the  original  sentence.  The  new
    senteces are in the main memory under  names  given  by  the  user  or
    generated by the system. 

    The option of the command containing notions enables to generate  only
    those sentences which contain given notions.  The  number  of  notions
    (i.e. words) is at most 3 and they should be separated by commas.  The
    system will keep all sentences containing notions related to at  least
    one of given words. 

    The module works with predicate formulas and at the end  of  the  work
    generated formulas are  translated  into  regular  sentences.  At  the
    beginning the original sentence is transformed by definitions, axioms,
    lemmas and logically valid formulas and generated sentences are stored
    into an auxiliary sentence file. Sentences from  this  file  are  then
    taken as current sentences which are transformed as mentioned and  the
    file is further filled in. From time to time the  system  reduces  the
    content of the file throwing out non-interesting  sentences.  Finally,
    the most interesting sentences from the auxiliary file are put in  the
    main memory under some names. 

    The work of the module is automatic or interactive. In both cases  the
    following blocks can be activated: 

    0) cancel; 
    1) automatic work; 
    2) interactive work; 
    3) automatic selection of the sentence which will be processed; 
    4) interactive sentence selection; 
    5) automatic auxiliary sentence file reduction; 
    6) interactive file reduction; 
    7) instantiating definitions; 
    8) replacing subformulas using definitions; 
    9) replacing subformulas using axioms; 
    10) replacing subformulas by lemmas; 
    11) replacing subformulas by logically valid formulas; 
    12) adding new lemmas; 
    13) giving notions to be contained in generated sentences; 
    14) automatic end of work; 
    15) interactive end of work; 
    16) getting information about existing blocks. 

    In interactive work blocks are selected  by  typing  the  numbers  (as
    given above) when the system asks: "How to continue?" 

1
                                   - 6.7 -

    In automatic work a special subroutine decides which of  these  blocks
    should be activated when the previous block has finished the work. 





    6.5 INTERACTIVE PROVER 




    6.5.1 Creating a Proof Tree (CREATE, MOVE) 

    The user can try to prove that a statement (sentence) is  true  by  an
    interactive theorem proving facility, described in  this  Section,  as
    well as by a fully automatic prover (see the next Section). 

    The interactive proof starts with the command 

       CREATE <t-name> [AS] [PROOF] [OF] <s-name> .
    
    
    The system creates a tree that is perhaps going to be a proof  of  the
    considered sentence. In this moment the tree consists  of  one  single
    point representing the sentence,  i.e.  the  goal  of  the  proof.  In
    further work the goal is split into  subgoals  and  they  further  are
    split into new subgoals or are replaced by other subgoals.  The  proof
    tree is a rooted tree. The root  indicates  the  currently  considered
    subgoal. The user can move the root by commands: 

                                       {     UP                   }
                                       {     DOWN                 }
       MOVE [THE] [ROOT] [OF] <t-name> {     RIGHT                } .
                                       {     LEFT                 }
                                       {[TO] [THE] POINT <i-value>}
    
    
    Moving the root up-down means the moving between "father"  and  "sons"
    and the moving "left" - "right" means the moving  between  "brothers".
    Each subgoal (i.e. each point of the proof  tree)  has  an  internally
    generated identification number which is used in the  last  option  of
    MOVE-command. These identification numbers can be obtained  by  typing
    the whole proof tree (see below). 



    6.5.2 Finding Subgoals (FIND, MODIFY, LIST, DELETE, SET) 

    By the command 

       FIND SUBGOALS [OF] [THE] [ROOT] [OF] <t-name> .
    
    
    the current subgoal is split into two subgoals according to one of the
    following four schemes: 

      A.AND.B       A<=>B       A=>B.AND.C        A.OR.B=>C
     /       \     /     \      /         \      /       \
    A         B  A=>B   B=>A  A=>B       A=>C  A=>C     B=>C
    
1
                                   - 6.8 -

    
    A subgoal will not be split in this way if it already has "sons" or if
    it is already proved. 

    By the command 

       MODIFY [THE] [ROOT] [OF] <t-name> [BY] CASE <s-name> .
    
    
    the current subgoal A will be  split  into  the  subgoals  P => A  and
    NOT.P => A , where P is a sentence given by the user (case analysis). 

    A transition subgoal may be introduced by the command 

       MODIFY [THE] [ROOT] [OF] <t-name> [BY] TRANSITION [GOAL] <s-name> .
    
    
    The current subgoal A => B will be split into A => P and P => B  where
    P is given by the user. 

    The command 

       MODIFY [THE] [ROOT] [OF] <t-name> [BY] <s-name> .
    
    
    replaces the current subgoal by the new sentence given  by  the  user.
    (The subgoal gets  only  one  "son".)  This  new  sentence  should  be
    equivalent to the subgoal or at least should imply  it.  The  user  is
    responsible the for this since the system does not check it.  However,
    the system will ask the user for a comment about this modification. 

    Similarly, we have the following commands 

                                            {DEFINITIONS   }
       MODIFY [THE] [ROOT] [OF] <t-name> BY {LEMMAS        } .
                                            {VALID_FORMULAS}
    
    
    by which the subgoal will be transformed in the manner desired. 

    By the command 

       MODIFY [THE] [ROOT] [OF] <t-name> .
    
    
    universal quantifiers acting on the whole subgoal will be  deleted  or
    the subgoal of the form A=>B will be converted into B and  A  will  be
    send to a file and will be used as a lemma in further proving process. 

    The command 

       MODIFY [THE] SUBGOAL <i-value> [OF] <t-name> .
    
    
    will cause an independent action of the system (as described below) on
    the subgoal specified. 

    The goal is proved if all leaves (i.e. subgoals  without  "sons")  are
    proved. The status of such a subgoal (proved - unproved) is  internaly
    noted, and to get a  survey  of  situation  the  user  can  apply  the
    following command: 
1
                                   - 6.9 -


       LIST SUBGOALS [OF] <t-name> .
    
    
    The system will give the identifiction numbers of both the proved  and
    the unproved leaves. 

    If the user is not satisfied with some steps in the interactive proof,
    he can reduce the proof tree to a previous state using the command 

       DELETE SUBTREE [OF] <t-name> .
    
    
    The subtree below the root will be deleted. 

    A subgoal can sometimes be declared as  true  by  the  system  itself.
    However the user can say 

       SET [THE] ROOT [OF] <t-name> [TO] [BE] [TRUE] .
    
    
    The system will ask "Tell me why you think the sentence is true ?" and
    will expect a short comment about it. This comment is memorized and is
    reproduced when typing the whole proof tree. 

    A subgoal can be separated from the proof tree and then proved by  the
    automatic prover (see Section 6.7) or an independent interactive proof
    (under another name) of it can  be  started.  The  separating  command
    reads: 

       SET <s-name> = [ROOT [OF]] <t-name> .
    
    
    However, sometimes the interactive prover sends the current subgoal to
    the automatic theorem prover. 

    The interactive theorem prover works in one  of  the  following  three
    modes: stepwise work, semiautomatic work, and automatic work. 

    In  the  first  mode  the  prover  is  quite  passive;   it   performs
    transformations of subgoals as the user wishes step by step. 

    In the semiautomatic work the prover only splits a goal into  subgoals
    or transforms the subgoal by a number of logically valid formulas  and
    some rewriting rules (always) when possible. At  most  one  definition
    instantiation or rewriting by lemmas  is  performed  on  each  of  the
    subgoals generated in this way. Again  logically  valid  formulas  and
    rewriting rules are applied. The system checks  whether  subgoals  are
    trivially true. It activates  the  automatic  theorem  prover  if  the
    subgoal is of the form of an implication  and  any  predicate  in  the
    conclusion appears also in the hypothesis.  If  the  automatic  prover
    fails, the system will ofer the user another chance if he wants to add
    some lemmas. Additional lemmas should be given in the form of  clauses
    (see next Section) and the user is responsible for the correct form of
    clauses. After performing all these actions on each  of  the  subgoals
    generated in the meantime,  the  system  will  ask  the  user  how  to
    continue. 

    In the automatic work the  number  of  definition  instantiations  and
    rewriting by lemmas is not bounded. 

1
                                   - 6.10 -

    The mode of the work can be selected by the command 

       SET MODE [OF] PROVING [TO] <i-value> .
    
    
    Setting 0 is for the stepwise work, 1 for the semiautomatic work,  and
    2 for the automatic work. 

    If the system "Graph" has just started to work, the prover  will  work
    semiautomatically. 

    When deciding about applying  a  definition  or  a  lemma  the  system
    calculates the complexity of the  current  subgoal,  as  described  in
    [12]. There are two definitions of the complexity  formula:  a  simple
    one and a more sophisticated one. The system normally uses the  latter
    but the user can choose the way of calculating the complexity  by  the
    command 

       SET MODE [OF] COMPLEXITY [TO] <i-value> .
    
    
    The values 0 and 1 of the mode correspond to  the  mentioned  ways  of
    calculating the complexity, respectively. 

    The behaviour of the prover is described with more details in [12]. 



    6.5.3 Displaying Proof Tree (TYPE, DRAW) 

    By the command 

       TYPE <t-name> .
    
    
    the part of the proof tree below the root (including the root) will be
    typed. "Sons" are typed two characters to the right  and  below  their
    "father". A subgoal is represented by its  identification  number,  by
    the predicate formula representing the subgoal and  by  a  comment  in
    case when the subgoal is proved. If the whole subtree below  the  root
    cannot be typed on one page this is indicated and the  user  can  move
    the root down and type different parts of the tree separately. 

    Example of a proof tree: 

    1      P1=>P2
      3      (ALL X)(ALL Y)(X#Y=>R1(X,Y))=>P2
        4      (ALL X)(ALL Y)(X#Y=>R1(X,Y))=>(ALL X1)(ALL Y1)R2(X1,Y1)
          5      (ALL X)(ALL Y)(X#Y=>R1(X,Y))=>(ALL Y1)R2(X1,Y1)
            6      (ALL X)(ALL Y)(X#Y=>R1(X,Y))=>R2(X1,Y1)
              7      (ALL X)(ALL Y)(X#Y=>R1(X,Y))=>(EXT K)S2(X1,Y1,K)
                8   *  (ALL X)(ALL Y)(X#Y=>S2(X,Y,1))=>(EXT K)S2(X1,Y1
                       ,K) Proved by resolution
    
    
    By the command 

       DRAW <t-name> .
    
    
    a graphical version of the proof tree is obtained on the  screen  (not
1
                                   - 6.11 -

    implemented). 

    The command 

       TYPE ROOT [OF] <t-name> .
    
    
    will give the subgoal of root of the proof tree in the formula form. 

    By the command 

       TYPE HEAD [OF] <t-name> .
    
    
    the user can get general data about the proof tree (number of  points,
    number of free points, root etc; see also the internal  representation
    of proof trees in Appendix). (Not implemented). 




    6.6 AUTOMATIC PROVER (PROVE) 


    The basic command in this Section reads 

       PROVE <s-name> .
    
    
    The system will try to prove almost fully automatically the  statement
    of the given sentence. 

    This prover basically uses linear ordered resolution as  described  in
    [35], Sections 7.4.-7.7. Another rule used is the induction rule [13]. 

    At the beginning the  system  will  display  on  the  screen  relevant
    definitions and lemmas and ask the user to select which  of  them  are
    necessary for the proof. Then the system will ask the user whether  he
    wants a proof which uses also the induction rule or a proof only  with
    resolution. The system also asks  whether  the  user  wants  symmetric
    predicates (i.e. predicates symmetric with respect to  the  first  two
    coordinates) handled automatically. 

    The negation of the closure  of  the  sentence  as  well  as  selected
    definitions and lemmas will be skolemized and represented in  form  of
    clauses. The starting set of clauses is displayed. 

    Arguments of predicates should be the terms  containing  at  most  one
    arithmetical  operation   and   neither   constants   nor   functions.
    Arithmetical  operations  and  relations  are  converted  into  prefix
    notation form. 

    If the proof is found, it is typed by the system.  Each  step  in  the
    proof consists of an application of a resolution or  of  an  induction
    rule on two clauses. Both clauses and the corresponding resolvent  are
    typed. The first (central) clause is a clause coming from the negation
    of the original sentence or is a resolvent from  previous  steps.  The
    second (auxilliary) clause belongs to the starting set of clauses,  or
    is a clause generated by the induction rule. 

    If the proof is not found within the room in the memory given for this
1
                                   - 6.12 -

    sentence, the user will get the corresponding message. 

    If the system fails in proving  a  sentence  the  user  could  try  to
    permute the starting set of clauses and this can lead to a proof.  The
    permutation can be performed by  setting  the  mode  of  proving  (see
    command SET MODE OF PROVING . in the previous  Section)  for  stepwise
    work. Applying again the command PROVE the user can type  the  clauses
    in order he wants. (Here the user is responsible for the  correcteness
    of clauses). This way of entering clauses is convenient  if  the  user
    wants to prove a sentence which  is  not  regularly  accepted  by  the
    system "Graph" (say, a sentence beyond graph theory). In this case the
    form of terms is not limited, but the prefix form should be  used  for
    all relations and operations. 

    The effectivness of the prover  depends  also  on  several  parameters
    which are set in the file  GRAPH.PAR  .  This  file  can  be  modifyed
    outside the system "Graph" using a text editor. 

    Parameters related to the resolution theorem prover are the  following
    ones: 

        JMAX   maximal number of clauses in the starting set 
        LMAX   maximal number of resolvents in a level 
        IDMAX  maximal number of symbols in a clause or in a substitution 
        LITMAX maximal number of symbols in a literal 
        KRMAX  maximal number of symbols in all central clauses in a level 
        IAKSMX maximal number of symbols in all clauses from axioms 
        IRNVMX maximal number of clauses generated for a starting clause 
        IDUBMX maximal number of levels 
        IDMAXR maximal number of symbols in a resolvent 

        The parameters are placed in file GRAPH.PAR as follows: 

        JMAX__   100,  LMAX__   100,  IDMAX_   100,  LITMAX    50,
        KRMAX_ 10000,  IAKSMX 10000,  IRNVMX  2525,  IDUBMX    25,
        IDMAXR   100,
    
    The depth of the search is regulated by IDUBMX and the breadth of  the
    search by LMAX. A good heuristic is to bound the length of  resolvents
    by IDMAXR. In that case the space on each level will be used for short
    resolvents which might lead to a proof. 

    The system generates resolvents  from  a  central  clause  C1  and  an
    auxilliary clause C2 using the following rules: 

    1. Variables in C1 and C2 are renamed so that the clauses do not  have
    common variables. 

    2. Finding resolution substitution (the most general  unifier)  T  for
    the last literal L1 in C1 and the k-th (k=1,2,...) literal L2 in C2. 

    3. A clause R is now obtained in the following way. In the clause  C1T
    the literal L1T is marked  by  a  slesh  in  front  of  L1T.  This  is
    concatenated with C2T and then L2T is deleted. 

    4. Non-marked literals are deleted from R if  they  are  identical  to
    some other non-marked literals standing in the left of them in R. If R
    is a tautology, the resolvent is not generated. 

    5. Marked literals followed by no non-marked literals are deleted. 

1
                                   - 6.13 -

    6. The last (non-marked) literal in R is deleted if it can be  unified
    by a unifier U with a complementary (in the sence of negation)  marked
    literal in R, thus yealding clause RU. 

    7. If the last literal in RU is marked we again apply 5. and 6. If  it
    is not marked or if the clause is empty we have the final form of  the
    resolvent which is going to be a central clause in the next level. 

    If the mode of proving is set to 2 then the system  will  display  all
    the resolvent generated in each level. Otherwise only  the  number  of
    resolvents in each level will be noted. 

    An example of the resolution proof: 

        R1(X,Y)<=>R1(Y,X)
    
        Clauses :
        R1(O501,O502)R1(O502,O501)&
        NOT.R1(O502,O501)NOT.R1(O501,O502)&
    
        The refutation proof is given by the following sequence
        of clauses:
        Central clause:
        R1(O501,O502)R1(O501,O502)&
        Auxilliary clause:
        NOT.R1(O502,O501)NOT.R1(O501,O502)&
        Resolution substitution:
        &
        Central clause:
        R1(O501,O502)/R1(O501,O502)NOT.R1(O502,O501)&
        Auxilliary clause:
        R1(O501,O502)R1(O502,O501)&
        Resolution substitution:
        &
        Central clause:
        R1(O501,O502)&
        Auxilliary clause:
        NOT.R1(O502,O501)NOT.R1(O501,O502)&
        Resolution substitution:
        &
        Central clause:
        /R1(O501,O502)NOT.R1(O502,O501)&
        Auxilliary clause:
        R1(O501,O502)R1(O502,O501)&
        Resolution substitution:
        &
        Central clause:
        /R1(O501,O502)/NOT.R1(O502,O501)R1(O502,O501)&
        Auxilliary clause:
        NOT.R1(O502,O501)NOT.R1(O501,O502)&
        Resolution substitution:
        &
        Empty clause:
    
    The command 

       PROVE [SUBGOAL <i-value>] [OF] <t-name> .
    
    
    will activate the automatic theorem prover and direct it to a  subgoal
    of the proof tree generated  previously  by  the  interactive  theorem
1
                                   - 6.14 -

    prover (see Section 6.5). If the subgoal is not specified, the root of
    the tree will be treated. 




    6.7 FINDING NECESSARY SENTENCES (FIND, SHOW, SET) 


    Axioms, lemmas and theorems containing given phrases can be  found  by
    the command 

                       { AXIOMS }
       FIND [<f-name>] { LEMAS  } [ABOUT] {<key phrase>}...(3) .
                       {THEOREMS}
    
    
    The resulting  family  will  contain  the  identification  numbers  of
    sentences (axioms, lemmas or theorems) containing all the key  phrases
    given. The key phrases should  consist  of  the  words  known  to  the
    system. 

    After the command 

       FIND DEFINITION [OF] <phrase> .
    
    
    the system will display all notions containing the  given  phrase  and
    will give the identification numbers of the corresponding definitions.
    However, the system will not be able to find basic notions.  The  next
    command can help in that case 

       SHOW <objects> .
    
    
    Possible objects are AXIOMS, DEFINITIONS, LEMMAS,  NOTIONS,  THEOREMS,
    VALID FORMULAS, WORDS. 

    There are two modes of shwing: 0 - the system displays  identification
    numbers or only the number of  objects,  1  -  the  system  gives  the
    objects themselves. 

    The mode can be set by the command 

       SET MODE [OF] SHOWING [TO] <i-value> .
    
    
    After starting the system the mode will be set to 0 . 




    6.8 TEMPORARY LIMITATIONS 


    There are some limitations  in  using  THEOR  part,  which  are  of  a
    temporary character and which are not essential. 

    The sentence which enters the  system  should  satisfy  the  following
    conditions: 1. Bound  variables  associated  to  diferent  quantifiers
    should be denoted differently, 2. A bound and  a  free  variable  must
1
                                   - 6.15 -
    never be identic. The user should also take care that  new  sentences,
    resulting from other sentences through the command FORM, satisfy these
    conditions. Since the  system  does  not  accept  the  negation  of  a
    quantifier, sentences containing the negation of a  quantifier  should
    be created by the command FORM.  When  setting  a  sentence  the  user
    should use the syntax of proper GTCL as given in Appendix C. Very long
    sentences may cause a malfunction of the system. Main limitations are: 

       the number of words is at most 120, 
       the number of elementary sentences is at most 30, 
       the number of quantifiers is at most 30, 
       the number of free variables is at most 4, 
       the number of appearences of free variables is at most 50, 
       the number of predicate letters is at most 20. 

    When entering clauses for the command PROVE in the stepwise mode,  the
    user is responsible for the correct form of them.The terms in formulas
    sent to resolution theorem prover (semi-automatic mode) should contain
    at  most  one  arithmetical  operation.  Functional  definitions   and
    operational definitions for binary  graph  operations  should  not  be
    used, since they are not handled in some blocks of the prover. 

    If the sentences or proof trees are stored in WORK FILE  or  in  other
    files, and if they are moved back to the main memory (by command GET),
    the user should be sure that necessary definitions  and  subgoals  are
    not deleted in the meantime. For example, if you send a proof tree  T1
    to a file, if the system forgets T1 in  the  main  memory  (after  the
    command FORGET T1 .), the system cannot further work with T1 if it  is
    now obtained by the command GET T1 . 

    Functions and constants do not have suffixes. 


1








    7 UTILITIES        



    In this chapter the GTCL commands for various utility  operations  are
    described. These operations don't relate to any  particular  topic  of
    those discussed in the previous  chapters.  They  are  rather  general
    purpose manipulative operations, common to the whole system "Graph". 




    7.1 INFORMATIVE OPERATIONS 




    7.1.1 Giving Informations About the System (INFORM) 

    Valuable informations, especially for the beginner  users,  about  the
    system "Graph" can  be  obtained  directly  on  the  terminal  by  the
    command: 

       INFORM [[ABOUT] <topic name>] .
    
    
    <Topic name> denotes the topic about which the information is  needed.
    An introductory to the whole system "Graph" is obtained if  the  topic
    name is omitted. 

    Informations can be get about the next topics: AGT,  BOOK,  CALCULATE,
    CHECK,  COLLABORATORS,  COMMANDS,  CONNECTIVE,  CREATE,   DEFINITIONS,
    DELETE, DETERMINE, DRAW,  ENUMERATE,  EXPRESSION,  FACILITIES,  FILES,
    FILMAN, FIND, FINISH, FORGET,  FORM,  FORMULA,  GENERATE,  GET,  GTCL,
    INFORM, INVESTIGATE, KEY, LETTER, LIST, MEMAN, MODIFY,  MOVE,  PAPERS,
    PROCEEDINGS, PROPER, PROVE, QUANTIFIERS, RELABEL, SENTENCE, SET, SHOW,
    SORT, STORE, SYSTEM, TYPE, VARIABLES, and VERBS. 

    Example: INFORM ABOUT GTCL .
    
    


    7.1.2 Showing Tables of Keywords (SHOW) 

    Tables are another sources of informations. During the work  with  the
    system "Graph" they are referenced by HELPHELP level messages  of  the
    form "(consult Table #)", where # stands for the number of  the  table
    to be consulted. 

    Tables contain the list of the acceptable keywords or data types at  a
    given moment when entering a GTCL  command.  They  are  all  shown  in
    Appendix B. The user  can  look  up  at  any  table  directly  on  the
    terminal, too, by issuing the GTCL command: 

       SHOW TABLE <i-value> .
1
                                   - 7.2 -

    
    
    Example: SHOW TABLE 5 .
    
    



    7.2 MANIPULATIONS WITH THE DATA IN THE MEMORY 


    The memory represents the system's work area. It holds data of various
    types that are generated by the appropriate  GTCL  commands.  In  this
    section the common manipulative operations, independent of data types,
    are described. 



    7.2.1 Copying Data (SET) 

    A copy of data in the memory can be made by the command: 

       SET <name 1> = <name 2> .
    
    
    A new variable with name <name 1> is formed  with  the  value  of  the
    variable with name <name 2>. The data type is determined expicitly  or
    implicitly (as described in Section 2.3) by  <name 1>.  <Name 2>  must
    not contain a keyword denoting the data type, unless <name 1>  denotes
    a graph variable (in that case keywords GRAPH or  TREE  must  be  used
    when implicit type convention does not hold for <name 2>. 

    Example: SET F1 = BETA .
             SET G15 = TREE GAMA .
    
    


    7.2.2 Showing Variable Names and Values (SHOW) 

    Informations about the existing variables  and  their  values  in  the
    memory are obtained by the command: 

       SHOW [THE] [<type>] {VARIABLES} [<name>] .
                           {DATA     }
    
    
    With the keyword VARIABLES a list of variables, in the form of a  four
    column table, will be displayed  on  the  terminal.  Every  column  is
    divided into four subcolumns, containing the next  items  about  every
    variable: 

    a) NAME - Name of the variable (up to 5 characters); 
    b) TYP  - type of the variable (one letter with yhe next meanings: I -
              integer, R - real, C - complex, G - graph, T  -  tree,  F  -
              family, and S - sentence); 
    c) SIZE - size of the room occupied by the variable i  the  memory  in
              terms of room needed for an integer data (e.g.: a real  data
              occupies room as 2 integers, complex as 4 integers); and 
    d) POS  - position of the variable  in  the  memory  relative  to  the
              beginning of the memory in  terms  of  room  needed  for  an
1
                                   - 7.3 -

              integer data. 

    With the keyword DATA the table will for every variable contain two or
    more lines. The first line  contains  the  above  informations  (name,
    type, size, and position). The second  and  eventual  succeding  lines
    contain the value of the variable represented as an array  of  integer
    values (ten of them in every but the last line). The array  shows  the
    internal form of the data as described in Appendix D. 


    The selection of the variables to be included into the report is  done
    by the arguments <type> and <name>. 

    <Type> can be one of the keywords  denoting  the  defined  data  types
    (INTEGER, REAL, COMPLEX, GRAPH, TREE, FAMILY, and SENTENCE) or one  of
    the keywords SYSTEM, ALL, or ANY. The keyword SYSTEM denotes variables
    generated by the system without the user's knowledge (they will appear
    with types "$" or "%"). The keyword ALL denotes all data  types  known
    to the user,  without  system  variables.  Finally,  the  keyword  ANY
    denotes all data types including the system variables,  too.  Omitting
    the argument <type> implies the keyword ALL. 

    <Name> defines one or more variable names using  wildcard  characters.
    Omitting the argument <name> implies the name  pattern  ";;;;;",  i.e.
    all variables of the selected type will be included. 

    Examples: SHOW VARIABLES .
              SHOW GRAPH DATA .
              SHOW VARIABLES FX;;; .
    


    7.2.3 Forgetting Variables (FORGET) 

    Removing data from the memory to release some storage is done  by  the
    command: 

       FORGET [<type>] <name> .
    
    
    <Type> and <name> defines the variables to be removed from the memory.
    <Type> can be one of the keywords  denoting  the  defined  data  types
    (INTEGER, REAL, COMPLEX, GRAPH, TREE, FAMILY,  and  SENTENCE)  or  the
    keyword ALL denoting any type of user defined  variables.  Note,  that
    system variables can't be forgotten,  they  are  under  the  exclusive
    control of the system "Graph". 

    If <type> is omitted, the type of the selected variables is determined
    implicity by <name>. In that case  <name>  should  not  begin  with  a
    wildcard character. 

    Examples: FORGET G1 .
              FORGET FAMILY ;;;;; .
    
    






1
                                   - 7.4 -




    7.3 MANIPULATIONS WITH THE DATA IN THE FILES 


    Files are used to save large amounts of data. There  is  one  standard
    file of medium size called WORK FILE and an arbitrary number  of  user
    defined files (creating user defined files is described in Section  7.
    4). 

    The only possible manipulations with data in  files  are  moving  data
    from memory into a file or vice versa,  showing  data  existing  in  a
    file, and deleting data form a file. 



    7.3.1 Storing Data into Files (STORE) 

    Data are transferred from the memory into a file by command: 

       STORE [<type>] <name> [INTO [FILE] {WORK_FILE  }] .
                             [            {<file name>}]
    
    
    <Type> and <name> defines the variables to be stored into the file. 

    <Type> can be one of the keywords  denoting  the  defined  data  types
    (INTEGER, REAL, COMPLEX, GRAPH, TREE, FAMILY,  and  SENTENCE)  or  the
    keyword ALL denoting any type of user defined variables. 

    If <type> is omitted, the type of the selected variables is determined
    implicity by <name>. In that case  <name>  should  not  begin  with  a
    wildcard character. 

    <File name> denotes the name of a user defined file (see Section 7.4).
    If no file is specified, the work file (WORK FILE) is assumed. 

    Examples: STORE G2 INTO WORK_FILE .
              STORE FA1;; INTO FILE FAMIL .
              STORE TXX1 .
    
    


    7.3.2 Getting Data from Files (GET) 

    Data are transferred from a file into the memory by the command: 

       GET [<type>] <name> [FROM [FILE] {WORK_FILE  }] .
                           [            {<file name>}]
    
    
    <Type>, <name>, and <file name> have  the  same  meanings  as  in  the
    previous section. 

    Example: GET H55 FROM WORK_FILE .
             GET AP;;; FROM FILE XYZ .
             GET GAAA .
    
    
1
                                   - 7.5 -



    7.3.3 Showing Variable Names and Values in Files (SHOW) 

    Informations about the existing variables and  their  values  in  some
    file are obtained by the command: 

       SHOW [THE] [<type>] {VARIABLES} [<name>]
                           {DATA     }
    
            IN [THE] {WORK_FILE       } .
                     {FILE <file name>}
    
    
    The list of variables without (VARIABLES) or  with  (DATA)  values  is
    displayed on the terminal in the same form as described in Section  7.
    2.3. <Type> and <name>  have  the  same  meanings,  too,  except  that
    keywords SYSTEM and ANY are not allowed for <type>. 

    Example: SHOW GRAPH VARIABLES IN THE FILE ALPHA .
    
    


    7.3.4 Deleting Data form Files 

    Deleting data from a file is done by the command: 

       DELETE [<type] <name> [FROM {WORK_FILE        }] .
                             [     {[FILE] <file name}]
    
    
    <Type>, <name>, and <file name> have the same meanings as described in
    Section 7.3.1. 

    Examples: DELETE G1 FROM FILE XYZ .
              DELETE ;BETA FROM WORK_FILE .
              DELETE F15 .
    
    



    7.4 MANIPULATIONS WITH FILES 


    Manipulations with files include  creation  and  deletion  of  a  user
    defined file and showing the list of  existing  files  in  the  system
    graph. 

    These operations are not recommended to use without a special need. 



    7.4.1 Creating Files (CREATE) 

    A user defined file is created by the command: 

1
                                   - 7.6 -

       CREATE FILE <file name>
    
              [FOR <number of data> [DATA]                   ]*** .
              [[OF] [AVERAGE] LENGTH <data length> [INTEGERS]]
              [[PHYSICAL] NAME <file specification>          ]
              [[RECORD] SIZE [OF] <record size> [INTEGERS]   ]
              [CAPACITY [OF] <file capacity> [RECORDS]       ]
    
    
    <File name> denotes the name of the file by which the user  wishes  to
    access the file (see Section 7.3). On the other  hand,  physical  file
    name is the name known to the operating system of  the  computer,  and
    depends on the computer and the operating system. One must consult the
    appropriate manuals of the local coputer center for details. 

    On the VAX-11 computers running under the VAX-VMS operating system the
    most  frequently  used  (but  not  complete)   form   for   the   file
    specification is <filnam>.<typ>, e.g.: "TREES.SIX". In such  case  the
    file will be created in the user's current default directory. 

    Care should be taken in selecting  the  physical  name,  because  some
    operating systems will destroy the already existing file if  the  same
    file specification (e.g.: filnam.typ) is used  in  the  command.  Some
    operative systems (e.g. VAX-VMS), on the other hand, will create a new
    version of the file if the same file  specification  is  selected,  in
    which cases the selection is not so critical. 


    <Number of data> is an integer value denoting the desired capacity  of
    the files in terms of user named data. In this sense, e.g., a graph is
    treated as one data, regardeless of the actual size of the graph. 

    <Data length> is an integer value denoting the axpected  average  size
    of the data stored into the file in  terms  of  space  needed  for  an
    integer value. Appendix D gives informations about the  internal  form
    and size of the data representations. 


    The variable length data mentioned above are stored  into  appropriate
    (but integer) number  of  fixed  length  physical  records.  In  every
    physical record allocated  to  a  data  there  is  an  overhead  space
    consumation of size for one  integer  value  plus  one  in  the  first
    record. On the other side, the last allocated record to a data is,  in
    the average, half empty. 

    <Record size> denotes, in form of  an  integer  value,  the  requested
    physical record size in the file in  terms  of  space  needed  for  an
    integer data. <Record size> must be at least 10. 

    <File capacity> denotes, in form of an integer  value,  the  requested
    number of physical records in the file. 

    In general, due to the internal overhead  in  the  space  consumation,
    holds    that    <number of data>*<data length>    is    less     than
    <file capacity>*<record size> (in an ideal case, with no overhead, the
    two products would be equal). 





1
                                   - 7.7 -


    The only mandatory parts of the described command are the logical  and
    the physical file name. For the other data,  if  skipped,  the  system
    will use default values defined at the installation time. 



    7.4.2 Showing Names of Files (SHOW) 

    The list of files contained in the file directory of system "Graph" is
    obtained by the command: 

       SHOW FILES .
    
    


    7.4.3 Deleting Files (DELETE) 

    Files not needed any more can be rejected by the command: 

       DELETE FILE <file name> .
    
    
    <File name> denotes the logical name of the file defined by  the  user
    when he created the file (see Section 7.4.1). Care should be taken not
    to delete any system's file (a file not created by the user). 

    Note, that the data about the selected file are deleted only from  the
    file directory of system "Graph". The file will,  under  the  physical
    name, still remain in the user's directory on the disk. To release the
    space occupied by the file on the disk, one should use the appropriate
    job control language command (after finishing  the  work  with  system
    "Graph"). 

    Example: DELETE FILE XYZ .
    
    



    7.5 MISCELLANEOUS COMMANDS 




    7.5.1 Changing the Mode of Looping (SET) 

    The mode of procceeding through a loop (as described in  Section  3.6)
    is changed by the command: 

       SET MODE [OF] LOOPING [TO] {CONFIRM  } .
                                  {NOCONFIRM}
    
    Keyword "Confirm" causes the system GRAPH to request a confirmation to
    procceeed for every encountered primary variable when enetered a  loop
    due to useage of wildcard characters in variable name(s). 

    Keyword "Noconfirm"  causes  the  system  GRAPH  to  procceed  without
    requesting confirmation for  any  encountered  pimary  variables  when
    entered a loop  due  to  usage  of  wildcard  characters  in  variable
1
                                   - 7.8 -

    name(s). 

    The initial mode of looping after every start of the system GRAPH (see
    Section 3.1) is "Confirm". 



    7.5.2 Terminating the Work (FINISH) 

    The work of the system "Graph" is terminated by the command: 

       FINISH .
    
    
    The system then saves the current state  of  the  work  area  (of  the
    memory) on the disk, to enable the user to continue his work next time
    from the same place,  and  displays  on  the  terminal  the  following
    message: 

       The work is finished. Good bye.
    

1








    R E F E R E N C E S 



    a) Papers about the system "Graph" 

    1.      Cvetkovic  D.:  A  project  for  using  computers  in  further
            development of graph theory, (The Theory and  Applications  of
            Graphs, Proc. 4th Internat. Conf. Theory and Appl. of  Graphs,
            Kalamazoo 1980, ed. G.Chartrand,  Y.Alavi,  D.L.Goldsmith,  L.
            Lesniak-Foster, D. R. Lick, John Wiley  &  Sons,  New  York  -
            Chichester - Brisbane - Toronto - Singapore, 1981), 285-296 

    2.      Cvetkovic D., Kraus L., Simic S.: Discussing graph theory with
            a computer I, Implementation of  graph  theoretic  algorithms,
            Univ.  Beograd,  Publ.  Elektrotehn.  Fak.  Ser.  Mat.   Fiz.,
            No.716-No.734 (1981), 100-104 

    3.      Stojkovic V., Cvetkovic D.: Analiza pomocu  racunara  recenica
            dela engleskog jezika formalizovanog  za  upotrebu  u  teoriji
            grafova, (XXV jug. konferencija ETAN-a, Mostar 1981, sv. III),
            271-278 

    4.      Cvetkovic D.: Prevodjenje matematickog teksta na jezik formula
            kvantifikatorskog racuna,  (Informatica  81,  Ljubljana  1981,
            3.108), 1-3 

    5.      Cvetkovic D., Pevac  I.:  Generisanje  recenica  ekvivalentnih
            zadatoj recenici, (Informatica 81, Ljubljana 1981, 3.107), 1-3 

    6.      Cvetkovic D.: Dicussing  graph  theory  with  a  computer  II,
            Theorems  suggested  by  the  computer,  Publ.   Inst.   Math.
            (Beograd), 33(47) (1983), 29-33 

    7.      Cvetkovic D., Cipranic M.: Interaktivni programski  sistem  za
            manipulaciju sa  recenicama,  (Zbornik  materijala  XXVI  jug.
            konf. ETAN-a, Subotica 7.-10.6.1982, Beograd 1982,  sv.  III),
            263-269 

    8.      Cvetkovic  D.,  Pevac  I.:  Discussing  graph  theory  with  a
            computer III, Man-machine theorem proving, Publ.  Inst.  Math.
            (Beograd), 34(48) (1984), 37-47 

    9.      Cvetkovic D., Pevac I.: Some heuristics in automatic the  orem
            proving, Publ. Inst. Math. (Beograd), 35(49) (1984), 167-171 

    10.     Cvetkovic D.: Discussing graph  theory  with  a  computer  IV,
            Knowledge organization and examples of theorem proving, (Graph
            Theory, Proc. IV Yugoslav Sem. Graph Theory, Novi  Sad  1983),
            43-68 

    11.     Cvetkovic D., Pevac  I.:  Algorithms  for  transforming  first
            order formulas in their natural  form,  Univ.  Beograd,  Publ.
            Elektrotehn.  Fak.,  Ser.  Mat.  Fiz.,  No.735-No.762  (1982),
            155-160 

1
                                   - 7.2 -

    12.     Cvetkovic D., Pevac I.: Man-machine theorem proving  in  graph
            theory, submitted 

    13.     Hotomski  P.  Z.:  Sposobi  vstroenija  pravila   indukcii   v
            proceduri avtomaticeskogo dokazateljstva teorem s rezolucijej,
            Publ. Inst. Math. (Beograd), 33(47) (1983), 89-95 

    14.     Hotomski P. Z.: Metode  i  pravila  za  mehanicko  dokazivanje
            teorema u teorijama prvog  reda  sa  matematickom  indukcijom,
            Doktorska disertacija, Beograd 1982 

    15.     Kraus  L.:   Jedan   upitni   sistem   opste   namene,   XXVII
            jugoslovenska konferencija ETAN-a, Struga  6.-10.  juna  1983,
            tom IV, 399-406 

    16.     Cvetkovic D.: Further experiences in computer  aided  research
            in graph theory, Graphs, Hypergraphs and  Applications,  Proc.
            Conf. Graph Theory held in Eyba, October 1984, ed.  H.  Sachs,
            Teubner, Leipzig, 1985, 27-30 

    17.     Cvetkovic D., Gutman I.: The computer system "Graph": A useful
            tool in chemical graph  theory,  J.  Comput.  Chem.,  7(1986),
            No.5, 640-644 

    18.     Cvetkovic D.: Discussing graph theory  with  a  computer,  VI,
            Theorems proved by the aid of the computer, submitted 

    b) Papers in whose preparation the system "Graph" was used 

    19.     Cvetkovic D., Doob M., Gutman I.: On graphs whose  eigenvalues
            do not exceed  sqrt(2+sqrt(5)),  Ars  Combinatoria,  14(1982),
            225-239 

    20.     Cvetkovic D., Doob M.: Root systems, forbidden  subgraphs  and
            spectral characterizations  of  line  graphs,  (Graph  Theory,
            Proc. IV Yugoslav Sem. Graph Theory, Novi Sad 1983), 69-99 

    21.     Gutman I., Cvetkovic D.: Finding tricyclic graphs with maximal
            number of  matchings  -  another  example  of  computer  aided
            research in graph theory, Publ. Inst. Math. (Beograd),  35(49)
            (1984), 33-40 

    22.     Cvetkovic D., Petric M.: A table of connected  graphs  on  six
            vertices, Discrete Math., 50(1984), 37-49 

    23.     Cvetkovic  D.:  Spectral  characterizations  of  line  graphs.
            Variations on the theme, Publ. Inst. Math.  (Beograd),  34(48)
            (1984), 31-35 

    24.     Cvetkovic D., Radosavljevic  Z.:  A  construction  of  the  68
            connected regular graphs,  non-isomorphic  but  cospectral  to
            line  graphs,  (Graph  Theory,Proc.  IV  Yugoslav  Sem.  Graph
            Theory, Novi Sad 1983), 101-123 

    c) Other references 

    25.     Cvetkovic D., Radosavljevic Z.: A table of regular graphs with
            at most 10  vertices,  Proc.  VI  Yugoslav  Seminar  on  Graph
            Theory, to appear 

    26.     Cvetkovic D.,  Rowlinson  P.:  Spectra  of  unicyclic  graphs,
1
                                   - 7.3 -

            Graphs and Combinatorics, to appear 

    27.     Rowlinson  P.:  A  deletion-contraction  algorithm   for   the
            characteristic polynomial of a multigraph,  Proc.  Royal  Soc.
            Edinburgh A, to appear 

    28.     Simic S.,  Radosavljevic  Z.:  The  nonregular,  nonbipartite,
            integral graphs with maximum  degree  four,  J.  Combinatorics
            Information and System Sci., to appear 

    29.     Radosavljevic Z., Simic S.: There are just thirteen  connected
            nonregular nonbipartite integral graphs having maximum  vertex
            degree four, Proc. VI Yugoslav Seminar  on  Graph  Theory,  to
            appear 

    30.     Radosavljevic Z., Simic S.:  Computer  aided  search  for  all
            graphs such that both graph  and  its  complement  have  their
            spectra bounded from below by -2, to appear 

    31.     Radosavljevic Z.: Contributions to the theory and practice  of
            the usage of expert systems in graph  theeory  investigations,
            (Serbo-Croatian), Thesis, University of Belgrade, l987 

    32.     Simic  S.,  Kocic  V.:  On  the  largest  eigenvalue  of  some
            homeomorphic graphs, Publ. Inst. Math. (Beograd), to appear 

    33.     Simic S.: Some results on the largest eigenvalue of  a  graph,
            to appear 

    34.     Torgasev A.: Graphs with three negative eigenvalues, Proc.  VI
            Yugoslav Seminar on Graph Theory, to appear 

    35.     Chang  C.-L.,  Lee  R.C.-T.:  Symbolic  logic  and  mechanical
            theorem proving, Academc Press, New York - London, 1973 


1



    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
                           A P P E N D I C I E S

1








    A) A SURVEY OF COMMANDS OF "GTCL" 






                                



    CALCULATE [<r-name>] [AS] [THE] <property> [OF] <g-name> .
    
    
       <property> ::= (ADMITTANCE_SPECTRUM)  |  (ANGLES)  |  BOND_ORDERS |
          CHARGES  |  DISTANCE_INDEX | (DISTANCE_SPECTRUM) | EIGENVALUES |
          EIGENVECTORS  |  ENERGY  |  (MAIN_ANGLES)   |   (R-SPECTRUM)   |
          SEIDEL_SPECTRUM
    
    
    
    
    CHECK [WHETHER] <g-name> [IS] [AN] <property> .
    
    
       <property> ::= ACYCLIC | BIPARTITE | BLOCK | (BLOCK_CUTPOINT_GRAPH)
          |  (BLOCK_GRAPH)  |  CIRCUIT  |  (CLIQUE_GRAPH)  |  COMPLETE   |
          CONNECTED  |  (CUTPOINT_GRAPH) | EULERIAN | FOREST | HAMILTONIAN
          |  HYPOHAMILTONIAN  | (INTERVAL_GRAPH) | LINE_GRAPH | LOOPLESS |
          (MOORE_GRAPH)  |  (OUTERPLANAR) | (PERFECT) | PLANAR | (PRIME) |
          REGULAR  |  (SELFCOMPLEMENTARY)  |  (SELFDUAL)  | SEMI_REGULAR |
          (SEMITOTAL_LINE_GRAPH)      |      (SEMITOTAL_POINT_GRAPH)     |
          STRONGLY_REGULAR  |  (SUBDIVISION_GRAPH)   |   (TOTAL_GRAPH)   |
          TOTALLY_DISCONNECTED  |  (TRAVERSIBLE) | TREE | TRIANGLES_FREE |
          TRIVIAL | UNICYCLIC | WHEEL | WITHOUT_MULTIPLE_LINES
    
    
    
    
                                                {COSPECTRAL            }
                                                {(HOMOMORPHIC)         }
    CHECK [WHETHER] <g-name> AND <g-name> [ARE] {(HOMEOMORPHIC)        } .
                                                {ISOMORPHIC            }
                                                {(SWITCHING_EQUIVALENT)}
    
    
    
    
1
                                   - A.2 -

                                            {CENTRAL       }
    CHECK [WHETHER][THE][POINT]<integer>[IS]{[A] CUT_POINT }[IN]<g-name> .
                                            {[AN] END_POINT}
                                            {ISOLATED      }
    
    
    
    
    CREATE FILE <file name>
    
           [ FOR <number of data> [DATA]                    ]*** .
           [ [OF] [AVERAGE] LENGTH <data length> [INTEGERS] ]
           [ [PHYSICAL] NAME <file specification>           ]
           [ [RECORD] SIZE [OF] <record size> [INTEGERS]    ]
           [ CAPACITY [OF] <file capacity> [RECORDS]        ]
    
    
    
    
    CREATE <g-name> [AS] <type of graph> [OF] [ORDER] <integer> .
    
    
       <type of graph> ::= CIRCUIT  |  COCKTAIL_PARTY  | COMPLETE | CUBE |
          MOBIUS_LADDER  |  PATH | PRISM | RANDOM | (RANDOM_TREE) | STAR |
          WHEEL
    
    
    
    
    CREATE <t-name> [AS] [PROOF] [OF] <s-name> .
    
    
    
    
           { {AUTHORS    } <string>                       }
           { {KEY_PHRASES}                                }
           {                                              }
           { {AXIOM     }                                 }
           { {DEFINITION} <i-value>                       }
           { {LEMMA     }                                 }
           { {THEOREM   }                                 }
    DELETE {                                              } .
           { FILE <file name>                             }
           {                                              }
           { PUBLICATIONS [<i-value>]...                  }
           {                                              }
           { SUBTREE [OF] <t-name>                        }
           {                                              }
           { [<type>] <name> [ FROM {WORK_FILE        } ] }
           {                 [      {[FILE] <file name} ] }
    
    
    
    
1
                                   - A.3 -

    DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] <objects>
    
              [OF] <g-name> .
    
    
       <objects> ::= (AUTOMORPHISM)  | BLOCKS | BRIDGES | CENTRAL_POINTS |
          (CIRCUITS)  |  CLIQUES  | (COCLIQUES) | COMPONENTS | CUTPOINTS |
          (INDEPENDENT_LINES)  | LINES | LOOPS | MAX_DEGREE | MIN_DEGREE |
          (ORBITS)  | PENDANT_LINES I (PENTAGONS) | POINTS | QUADRANGLES |
          TRIANGLES
    
    
    
    
    DETERMINE [<i-name>] [AS] [THE] <invariant> [OF] <g-name> .
    
    
       <invariants> ::= (CHROMATIC_CLASS)    |     (CHROMATIC_INDEX)     |
          CHROMATIC_NUMBER    |    CIRCUMFERENCE   |   (CLIQUE_NUMBER)   |
          (COARSENESS)    |    (COMPLEXITY)    |    (CROSSING_NUMBER)    |
          CYCLOMATIC_NUMBER    |    (DETERMINANT)     |     DIAMETER     |
          (EXTERIOR_STABILITY)  | (GENUS) | GIRTH | (INTERIOR_STABILITY) |
          (LINE_CONNECTIVITY)  |  (PERMANENT)  |  (POINT_CONNECTIVITY)   |
          RADIUS | RANK | (THICKNESS)
    
    
    
    
    DETERMINE [<i-name>] [AS] [THE] {DEGREE      } [OF] [POINT] <integer>
                                    {ECCENTRICITY}
    
            [OF] <g-name> .
    
    
    
    
                                                  {(CIRCUITS) }
                                                  {(CLIQUES)  }
    DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] {(COCLIQUES)}
                                                  {LOOPS      }
                                                  {TRIANGLES  }
    
              [CONTAINING] [POINT] <integer> [OF] <g-name> .
    
    
    
    
    DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] POINTS SIMILAR
    
              [TO] <integer> [OF] <g-name> .
    
    
    
    
1
                                   - A.4 -

    DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] <objects>
    
                   {DEGREE}
              [OF] {LENGTH} <integer> [OF] <g-name> .
                   {SIZE  }
    
    
       <objects> ::= CIRCUIT | (CLIQUES) | (COCLIQUES) | LINES | MATCHINGS
          | (PATHS) | POINTS | (TRAILS) | (WALKS)
    
    
    
    
    DETERMINE [<i-name>] [AS] [THE] [NUMBER] [OF] <objects> BETWEEN
    
              [POINTS] <integer> [AND] <integer> [OF] <g-name> .
    
    
       <objects> ::= (CIRCUITS_CONTAINING)    |    COMMON_NEIGHBOURS     |
          (DISJOINT_PATHS)  |  DISTANCE  |  LINE_LABEL  | LINES_INCIDENT |
          (PATHS) | (TRAILS) | (WALKS)
    
    
    
    
    DRAW [<g-name>  ] .
         [(<t-name>)]
    
    
    
    
    ENUMERATE [PUBLICATIONS] .
    
    
    
    
         { DEFINITION [OF] <phrase>                               }
         {                                                        }
         {            { { AXIOMS }                              } }
         {            { { LEMAS  } [ABOUT] {<key phrase>}...(3) } }
         { [<f-name>] { {THEOREMS}                              } }
         {            {                                         } }
    FIND {            {  THEOREMS [OF] [REFERENCE] <i-value>    } } .
         {                                                        }
         { KEY_PHRASES [CONTAINING] <string>                      }
         {                                                        }
         { PUBLICATIONS {<i-value>}...                            }
         {                                                        }
         { SUBGOALS [OF] [THE] [ROOT] [OF] <t-name>               }
    
    
    
    
1
                                   - A.5 -

    FIND [<language>] <publication type> [BY <authors or editors>]
    
         [ABOUT <key phrase> [, <key phrase>]...(4) ]
    
         [[FROM] YEARS <year> [TO [YEAR] <year>]]
    
         [[WITH] THEOREMS [<i-value>]... ] .
    
    
       <language> ::= BULGARIAN  |  CHINESE  | CZECH  |  DUTCH | ENGLISH |
          FRENCH  |  GERMAN  |  HUNGARIAN  | ITALIAN | JAPANESE | POLISH |
          ROUMANIAN | RUSSISAN | SERBO_CROATIAN | SPANISH
    
    
       <publication type> :==  ABSTRACTS | BOOKS | DOCUMENTS | MANUSCRIPTS
          | PAPERS | PROCEEDINGS | PUBLICATIONS | REPORTS
    
    
    
    
    FINISH .
    
    
    
    
           { COORDINATES [OF] <g-name>   }
           {                             }
    FORGET { PUBLICATIONS [<i-value>]... } .
           {                             }
           { [<type>] <name>             }
    
    
       <type> ::= COMPLEX  |  FAMILY  | GRAPH | INTEGER| REAL | SENTENCE |
                  TREE
    
    
    
    
    FORM [<g-name>] [AS] <operation> [GRAPH] [OF] <g-name> .
    
    
       <operation> ::= BASIS  |  (BLOCK)  | (BLOCK_CUT_POINT) | (CLIQUE) |
          CLOSED_NEIGHBOURHOOD  |  COMPLEMENT  | (CUT_POINT) | (DIGRAPH) |
          INVERSE_LINE    |   LINE   |   LOOP   |   OPEN_NEIGHBOURHOOD   |
          (PSEUDO_INVERSE) | REDUCED | SEMI_TOTAL_LINE  | SEMI_TOTAL_POINT
          | SKELETON | SQUARE | TOTAL
    
    
    
    
1
                                   - A.6 -

                                              {DISTANCE   }
                                              {(PATH)     }
    FORM [<g-name>] [AS] [THE] <integer> [TH] {POWER      } [GRAPH]
                                              {SUBDIVISION}
                                              {(TRAIL)    }
                                              {(WALK)     }
    
         [OF] <g-name> .
    
    
    
    
    FORM [<g-name>] [AS] [THE] <integer> [FOLD] UNION [OF] <g-name> .
    
    
    
    
    FORM [<g-name>] [BY] ADDING <integer> [ISOLATED] [POINTS]
    
         [TO] <g-name> .
    
    
    
    
    FORM [<g-name>] [AS] <operation> [OF] <g-name> [AND] <g-name> .
    
    
       <operation> ::= CORONA  |  JOIN | LEXICOGRAPHIC_PRODUCT | PRODUCT |
          STRONG_PRODUCT | SUM | UNION
    
    
    
    
    FORM [<g-name>] [AS] <option> <f-name> .
    
    
       <option> ::=
    
             { SUBGRAPH [OF] <g-name> INDUCED [BY] {POINTS}              }
             {                                     {LINES }              }
             {                                                           }
             { (SUBGRAPH [OF] <g-name> [BY] CONTRACTING [POINTS])        }
             {                                                           }
             { SUBGRAPH [OF] <g-name> [BY] DELETING {POINTS}             }
             {                                      {LINES }             }
             {                                                           }
             { SPANNING [SUBGRAPH] [OF] <g-name> [BY] {DELETING} [LINES] }
             {                                        {KEEPING }         }
             {                                                           }
             { SUPERGRAPH [OF] <g-name> [BY] { ADDING [LINES]   }        }
             {                               { JOINING [POINTS] }        }
             {                                                           }
             { [BY] SWITCHING <g-name> [W.R.T.] [POINTS]                 }
             {                                                           }
             { {GENERALIZED_LINE} [GRAPH] [OF] <g-name> [BY]             }
             { {PERMUTATION     }                                        }
    
    
    
    
1
                                   - A.7 -

    FORM [<g-name>] <option> <g-name> .
    
    
       <option> ::=
    
         {[BY] ADDING {LOOP} [TO] [POINT] <integer> [IN]                }
         {            {LINE}                                            }
         {                                                              }
         {              { {LOOP          }              }               }
         {[BY] DELETING { {PENDANT [LINE]} [AT] [POINT] } <integer> FROM}
         {              {                               }               }
         {              { POINT                         }               }
         {                                                              }
         {[BY] ISOLATING [POINT] <integer> [BY] [SWITCHING] [IN]        }
    
    
    
    
                         {CONTRACTING [LINES] }
    FORM [<g-name>] [BY] {DELETING [ALL] LINES} <integer> [<integer>]
                         {SUBDIVIDING [LINES] }
    
         [FROM] <g-name> .
    
    
    
    
    FORM <s-name> [AS] [THE] NEGATION [OF] <s-name> .
    
    
    
    
                                  {integer variable}
    FORM <s-name> {[FOR]  ALL   } {point   variable} <s-name> .
                  {[THERE] EXIST} {line    variable}
    
    
    
    
                             {CONJUNCTION            }
                             {DISJUNCTION            }
    FORM <s-name> [AS] [THE] {EQUIVALENCE            } [OF] <s-name>
                             {EXCLUSIVE [DISJUNCTION]}
                             {IMPLICATION            }
    
         [AND] <s-name> .
    
    
    
    
            {SENTENCES [EQUIVALENT][TO]<s-name> [CONTAINING "<notions>"]}
    GENERATE{                                                           }.
            {CONSEQUENCES [OF] <s-name>                                 }
    
    
    
    
1
                                   - A.8 -

        { {AXIOM     }                                }
        { {DEFINITION} <i-value> [AS] <s-name>        }
        { {LEMMA     }                                }
    GET { {THEOREM   }                                } .
        {                                             }
        { [<type>] <name> [FROM [FILE] {WORK_FILE  }] }
        {                 [            {<file name>}] }
    
    
       <type> ::= COMPLEX  |  FAMILY  | GRAPH | INTEGER| REAL | SENTENCE |
                  TREE
    
    
    
    
    INFORM [[ABOUT] <topic name>] .
    
       <topic name> ::= AGT  | BOOK | CALCULATE | CHECK | COLLABORATORS  |
          COMMANDS  |  CONNECTIVE  |  CREATE  |  DEFINITIONS  |  DELETE  |
          DETERMINE | DRAW | ENUMERATE | EXPRESSION | FACILITIES | FILES |
          FILMAN  |  FIND  | FINISH | FORGET | FORM | FORMULA | GENERATE |
          GET  | GTCL | INFORM | INVESTIGATE | KEY | LETTER | LIST | MEMAN
          |  MODIFY  |  MOVE  |  PAPERS  |  PROCEEDINGS | PROPER | PROVE |
          QUANTIFIERS  |  RELABEL | SENTENCE | SET | SHOW | SORT | STORE |
          SYSTEM | TYPE | VARIABLES | VERBS
    
    
    
    
    INVESTIGATE <g-name> .
    
    
    
    
    LIST [<f-name>] <objects> [OF] <g-name> .
    
    
       <objects> ::= BRIDGES  |  (CENTRE)  | CUT_POINTS | LINE_COLOURING |
          (LINE_DEGREES)  |  LINES  |  POINT_COLOURING  |  POINT_DEGREES |
          POINT_ECCENTRICITIES | POINT_ORBITS
    
    
    
    
                          {(CIRCUIT)    }
    LIST [<f-name>] [ANY] {(FOREST)     } [OF] <g-name> .
                          {SPANNING_TREE}
                          {(1-FACTOR)   }
    
    
    
    
1
                                   - A.9 -

    LIST [<f-name>] [COEFFICIENTS [OF]] <polynomial> [OF] <g-name> .
    
    
       <polynomial> ::= CHARACTERISTIC_POLYNOMIAL | (CHROMATIC_POLYNOMIAL)
          | MATCHING_POLYNOMIAL | SEIDEL_POLYNOMIAL
    
    
    
    
    LIST [<f-name>] <objects> [OF] <g-name> .
    
    
       <objects> ::= BLOCKS  |  (CIRCUITS)  |  CLIQUES  |  (COCLIQUES)   |
          COMPONENTS    |    (FACES)    |     (HAMILTONIAN_CIRCUITS)     |
          (MAXIMAL_MATCHINGS)    |    (HEXAGONS)    |    (PENTAGONS)     |
          POINT_NEIGHBOURS    |    (QUADRANGLES)    |    (SEMIBLOCKS)    |
          (SPANNING_TREES)  | (TRIANGLES) | (1-FACTORS) | PARALLEL_LINES |
          SERIAL_LINES
    
    
    
    
    LIST SUBGOALS [OF] <t-name> .
    
    
    
    
                {<f-name> [BY] [SPLITTING]                              }
                {                                                       }
                {<g-name>                                               }
                {                                                       }
                {PUBLICATION <i-value> REPLACING <options>              }
                {                                                       }
                {                   [    {[CASE             ] <s-name>}]}
    MODIFY [THE]{                   [    {[TRANSITION [GOAL]]         }]}.
                {[ROOT][OF] <t-name>[[BY]{                            }]}
                {                   [    {DEFINITIONS                 }]}
                {                   [    {LEMMAS                      }]}
                {                   [    {VALID_FORMULAS              }]}
                {                                                       }
                {SUBGOAL <i-value> [OF] <t-name>                        }
    
    
    
    
1
                                   - A.10 -

       <options> ::=
    
          {[;]LANGUAGE [BY] <language>                                }***
          {                                                           }
          {   {FIRST_PAGE_NUMBER}                                     }
          {   {ISSUE_NUMBER     }                                     }
          {   {LAST_PAGE_NUMBER }                                     }
          {[;]{PROCEEDING_NUMBER} [BY] <i-value>                      }
          {   {VOLUME_NUMBER    }                                     }
          {   {SIZE             }                                     }
          {   {YEAR             }                                     }
          {                                                           }
          {   {DESCRIPTION       }                                    }
          {   {JOURNAL_NAME      }                                    }
          {[;]{REVIEW_DESCRIPTION} [BY] <string>                      }
          {   {TITLE             }                                    }
          {                                                           }
          {[;] PREFACE_SIZE { <i-value> }                             }
          {                 { <string>  }                             }
          {                                                           }
          {[;]{AUTHORS   } [<old string>] BY <new string>             }
          {   {PUBLISHERS}                                            }
          {                                                           }
          {[;] KEY_PHRASES [<old string> [,<old string>]...(4)]       }
          {                                                           }
          {                BY <new string> [,<new string>]...(4)      }
          {                                                           }
          {   {CITING_PUBLICATION     }                               }
          {[;]{REFERENCED_PUBLICATIONS}[<i-value>]... BY{<i-value>}...}
          {   {THEOREMS               }                               }
    
    
       <language> ::= BULGARIAN  |  CHINESE  | CZECH  |  DUTCH | ENGLISH |
          FRENCH  |  GERMAN  |  HUNGARIAN  | ITALIAN | JAPANESE | POLISH |
          ROUMANIAN | RUSSISAN | SERBO_CROATIAN | SPANISH
    
    
    
    
                                    { UP                         }
                                    { DOWN                       }
    MOVE [THE] [ROOT] [OF] <t-name> { RIGHT                      } .
                                    { LEFT                       }
                                    { [TO] [THE] POINT <i-value> }
    
    
    
    
          { <s-name>                          }
    PROVE {                                   } .
          { [SUBGOAL <i-value>] [OF] <t-name> }
    
    
    
    
1
                                   - A.11 -

                                         { (CANONICALLY)            }
                                         { (COLOURS    )            }
                                         { (COMPONENTS )            }
                                         { (DEC-DEGREES)            }
            {LINES  }               [AT] { (INC-DEGREES)            }
    RELABEL {POINTS } [OF] <g-name> [BY] { (RANDOM     )            } .
                                         {                          }
                                         { {PERMUTATION  }          }
                                         { {C-PERMUTATION} <f-name> }
                                         { {CYCLICALLY   }          }
                                         { {STARTING_BY  }          }
    
    
    
    
        { <name 1>  = <name 2>                                       }
        {                                                            }
        { <c-name>  = <c-value>                                      }
        {                                                            }
        { <f-name>  = [<integer set> [, <integer set>]...]           }
        {                                                            }
        { <g-name> [= ( <np> [,] <nl> ) [<list of pairs of points>]] }
        {                                                            }
        { <i-name>  = <i-value>                                      }
        {                                                            }
        { <r-name>  = <r-value>                                      }
        {                                                            }
        { <s-name>  = {[ROOT [OF]] <t-name>}                         }
        {             {"<text>"            }                         }
        {                                                            }
    SET {           { {CALCULATING           }                }      } .
        {           { {CHECKING              }                }      }
        {           { {COMPLEXITY            }                }      }
        {           { {DETERMINING           }                }      }
        {           { {INVESTIGATING         }                }      }
        {           { {PROVING               } [TO] <i-value> }      }
        {           { {SHOWING               }                }      }
        { MODE [OF] { {                      }                }      }
        {           { {       {FAMILIES    } }                }      }
        {           { {TYPING {GRAPHS      } }                }      }
        {           { {       {PROOFS      } }                }      }
        {           { {       {PUBLICATIONS} }                }      }
        {           {                                         }      }
        {           { LOOPING [TO] {CONFIRM  }                }      }
        {           {              {NOCONFIRM}                }      }
        {                                                            }
        { [THE] ROOT [OF] <t-name> [TO] [BE] [TRUE]                  }
    
    
1
                                   - A.12 -

       <integer set> ::= [<i-value>]...
    
       <list of pairs of points> ::= <i> <j> [, <i> <j>]...
    
       <np> - number of points (integer value 1,2,...).
       <nl> - number of lines (integer value 0,1,2,...).
       <i> <j>  - pair of points which are connected by a line
                  (integer values 1,2,...,<np>).
    
    
    
    
        {                                    [        {FILE {<name>   }]}
        {                                    [        {     {WORK_FILE}]}
        { [THE] [<type>] {VARIABLES} [<name>][IN [THE]{               }]}
        {                {DATA     }         [        {MEMORY         }]}
        {                                    [        {WORK_FILE      }]}
    SHOW{                                                               } .
        { TABLE <i-value>                                               }
        {                                                               }
        { <objects-1>                                                   }
        {                                                               }
        { <objects-2> [BEGINNING [WITH] <string>]                       }
    
    
       <type> ::= ALL  | ANY | COMPLEX | FAMILY | GRAPH | INTEGER | REAL |
          SENTENCE | SYSTEM | TREE
    
       <objects-1> ::= AXIOMS | DEFINITIONS | FILES | LEMMAS  |  NOTIONS |
          THEOREMS | VALID_FORMULAS | WORDS
    
       <objects-2> ::= AUTHORS | JOURNALS | KEY_PHRASES | PBLISHERS
    
    
    
    
         { {(FAMILIES [<name>])                      }                 }
         { {                                         }                 }
         { {                     {(DEGREES         )}}                 }
         { { GRAPHS [<name>] [BY]{ EIGENVALUES      }} [INTO <prefix>] }
         { {                     {(SPECTRAL_MOMENTS)}}                 }
    SORT { {                                         }                 } .
         { { {INTEGERS} [<name>] [BY] [VALUES]       }                 }
         { { {REALS   }                              }                 }
         {                                                             }
         { PUBLICATIONS [BY] {AUTHORS}                                 }
         {                   {YEARS  }                                 }
    
    
    
    
1
                                   - A.13 -

          { {AXIOM  }                                                  }
          { {LEMMA  } <s-name>                                         }
          { {THEOREM}                                                  }
          {                                                            }
          { [BASIC      ]                                              }
    STORE { [FUNCTIONAL ] DEFINITION [:] "<notion>" [,] "<definition>" } .
          { [OPERATIONAL]                                              }
          {                                                            }
          { [<type>] <name> [INTO [FILE] {WORK_FILE  }]                }
          {                 [            {<file name>}]                }
    
    
       <type> ::= COMPLEX  |  FAMILY  | GRAPH | INTEGER| REAL | SENTENCE |
                  TREE
    
    
    
    
    STORE [<language>] <publication type> [:]
    
          <description of the publication>
    
          [ REVIEWED [IN] <review description>            ]***
          [                                               ]
          [ ABOUT <key phrase> [[,] <key phrase>]...(4)   ]
          [                                               ]
          [ [WITH] THEOREMS [<i-value>]...                ]    .
          [                                               ]
          [ {REFERING [TO]} [PUBLICATIONS] [<i-value>]... ]
          [ {CONTAINING   }                               ]
          [                                               ]
          [ CITED [IN] [PUBLICATIONS] [<i-value>]...      ]
    
    
       <language> ::= BULGARIAN  |  CHINESE  | CZECH  |  DUTCH | ENGLISH |
          FRENCH  |  GERMAN  |  HUNGARIAN  | ITALIAN | JAPANESE | POLISH |
          ROUMANIAN | RUSSISAN | SERBO_CROATIAN | SPANISH
    
    
       <publication type> :==  ABSTRACTS | BOOKS | DOCUMENTS | MANUSCRIPTS
          | PAPERS | PROCEEDINGS | REPORTS
    
    
    
    
         { <name>                      }
         {                             }
         { [HEAD [OF]] <t-name>        }
         { [ROOT [OF]]                 }
    TYPE {                             } .
         { IDENTIFICATION [NUMBERS]    }
         {                             }
         { PUBLICATIONS [<i-value>]... }
         {                             }
         { [TRANSLATION [OF]] <s-name> }
    
    
    
    

1








    B) TABLES OF KEYWORDS FOR COMMANDS 




    TABLE  1 - Possible verbs to start a command
    
    
    CAlculate      Enumerate      GET            PROve
    CHeck          FIND           INForm         Relabel
    CReate         FINIsh         INVestigate    Set
    DELete         FORGet         LIst           SHow
    DETermine      FORM           MODify         SOrt
    DRaw           GENERATe       MOVe           STore
                                                 Type
    
    TABLE  2 - Possible continuations of the command
    
               DETermine [<i-name>] [AS] [THE] [NUMBER] [OF] ...
    
    
    Automorphism        CUtpoints           MATchings
    BLocks              CYclomatic_number   MAX_degree
    BRidges             DEGree              MIN_DEgree
    CEntral_points      DETerminant         NEIGHBours
    CIRCUITS            DIAmeter            Orbits
    CIRCUITS_Containing DISJoint_paths      PAths
    CIRCUMference       DISTance            PENDant_lines
    CHROMATIC_Class     ECcentricity        PENTagons
    CHROMATIC_Index     EXterior_stability  PERmanent
    CHROMATIC_Number    GEnus               POINT_Connectivity
    CLIQUE_Number       GIrth               POINTS
    CLIQUES             INDEPEndent_lines   Quadrangles
    COArseness          INTERIor_stability  RANk
    COCliques           LINE_Connectivity   RADius
    COMMon_neighbours   LINE_Label          THickness
    COMPLexity          LINES               TRAils
    COMPOnents          LINES_Incident      Walks
    CRossing_number     LOOP
    
    
    TABLE  3 - Possible continuations of the command
    
               CReate <g-name> [AS] ...
    
    
    CIrcuit        CUbe           PRism          STar
    COCtail_party  Mobius_ladder  RANDOM         Wheel
    COMplete       PAth           RANDOM_Tree
    
    
1
                                   - B.2 -

    TABLE  4 - Possible continuations of the command
    
               CAlculate [<r-name>] [AS] [THE] ...
    
    
    ADmittance_spectrum  DISTANCE_Index     ENergy
    ANgles               DISTANCE_Spectrum  Main_angles
    Bond_oredrs          EIGENVAlues        R-spectrum
    Charges              EIGENVEctors       Seidel_spectrum
    
    
    TABLE  5 - Possible continuations of the command
    
               FORM <g-name> [AS [THE]] ...
                             [BY      ]
    
    
    Adding                   LOOP
    BAsis                    Open_neighbourhood
    BLOCK                    PErmutation
    BLOCK_Cut_point          PRODUCt
    CLIque                   PSEUDO_inverse
    CLOsed_neighbourhood     REDUCEd
    COMplement               SEMI_TOTAL_Line
    CONtracting              SEMI_TOTAL_Point
    CORona                   SKELETon
    CUtpoint                 SPanning
    DEleting                 SQUARE
    DIGraph                  STRONG_product
    Generalized_line         SUBGraph
    INVERSe_line             SUBdividing_line
    ISOLATing                SUPergraph
    JOIN                     SWitching
    LEXICOgraphic_product    TOtal
    LINE                     Union
    
    
    TABLE  6 - Possible continuations of the command
    
               CHeck [WHETHER] [THE] <g-name> And <g-name> [ARE] ...
    
    
    Cospectral   HOMEomorphic   HOMOmorphic   Switching_equivalent
    
    
1
                                   - B.3 -

    TABLE  7 - Possible continuations of the command
    
               CHeck [WHETHER] [THE] <g-name> [Is] ...
    
    
    Acyclic                  PLanar
    BIpartite                PRime
    BLOCK                    Regular
    BLOCK_Cutpoint_graph     SELFcomplementary
    BLOCK_Graph              SELFDual
    CIrcuit                  SEMI_Regular
    CLique_graph             SEMITOTAL_Line_graph
    COMplete                 SEMITOTAL_Point_graph
    CONnected                STrongly_regular
    CUtpoint_graph           TOTAL_Graph
    Eulerian                 TOTALLy_disconnected
    HAmiltonian              TRAversible
    HYpohamiltonian          TREe
    Interval_graph           TRIAnglesfree
    LIne_graph               TRIVial
    LOopless                 Unicyclic
    Moore_graph              WHeel
    Outerplanar              WIthout_multiple_lines
    PErfect
    
    
    TABLE  8 - Possible continuations of the command
    
               CHeck [WHETHER] [THE] [POINT] <integer> [Is] [An] ...
    
    
    CEntral        CUtpoint       End_point      Isolated
    
    
1
                                   - B.4 -

    TABLE  9 - Possible continuations of the command
    
               LIst <f-name> ...
    
    
    ANY                           LINES
    BLocks                        MATching_polinomial
    BRidges                       MAXimal_matchings
    CEntre                        PArallel_lines
    CHAracteristic_polynomial     PEntagons
    CHRomatic_polynomial          POINT_Colouring
    CIRCUIT                       POINT_Degrees
    CIRCUITS                      POINT_Eccentricities
    COCliques                     POINT_Neighbours
    COEfficients                  POINT_Orbits
    COMponents                    Quadrangles
    CLiques                       SEIdel_polynomial
    CUt_points                    SEMi_blocks
    FACES                         SERial_lines
    FOREST                        SPANNING_TREE
    HAmiltonian_circuits          SPANNING_TREES
    HExagons                      Triangles
    Independent_circuits          1-FACTOR
    LINE_Colouring                1-FACTORS
    LINE_Degrees
    
    
    TABLE 10 - Possible continuations of the command
    
               LIst [<f-name>] {ANY              }...
                               {COEfficients [OF]}
    
    
    CHAracteristic_polynomial     POINT_Degrees
    CHRomatic_polynomial          POINT_Eccentricities
    CUt_points                    POINT_Orbits
    LINE_Colouring                SEIdel_polynomial
    LINE_Degrees                  SPANNING_TREE
    MATching_polynomial           1-FACTOR
    POINT_Colouring
    
    
    TABLE 11 - Possible continuations of the command
    
               Relabel {Points} [OF] <g-name> [BY] ...
                       {Lines }               [AT]
    
    
    CAnnonicaly    C-Permutation  Inc-degrees    Random
    COLours        CYclically     Permutations   Starting_by
    COMponents     Dec-degrees
    
    
1
                                   - B.5 -

    TABLE 12 - Possible continuations of the command
    
               FORM <i-name> [TH  ] ...
                             [FOLD]
    
    
    Distance       POwer          TRail          WAlk
    PAth           Subdivision    Union          WIndmill
    
    
    TABLE 13 - Possible continuations of the command
    
               STore ...
    
    
    ABSTRAct       DOCUMEnt       <i-name>       REPORT
    AXIOM          DUTCH          ITALIAn        <r-name>
    BASIC          ENGLISh        JAPANEse       ROUMANian
    BOOK           <f-name>       LEMMA          RUSSIAn
    BULGARian      FRENCH         MANUSCript     SERBO_Croatian
    CHINESe        FUNCTIonal     Operational    <s-name>
    CZECH          GERMAN         PAPER          SPANISh
    <c-name>       <g-name>       POLISH         THEOREm
    DEFINItion     HUNGARian      PROCEEdings    <t-name>
    
    
    TABLE 14 - Possible continuations of the command
    
               FIND ...
    
    
    ABSTRAct       DUTCH          Key_phrases    REPORT
    AXioms         ENGLISh        Lemmas         ROUMANian
    BOOK           <f-name>       MANUSCript     RUSSIAn
    BULGARian      FRENCH         PAPER          SERBO_Croatian
    CHINESe        GERMAN         POLISH         SPANIsh
    CZECH          HUNGARian      PROCEEdings    SUBGOALS
    DEFINItion     ITALIAn        PUblications   Theorems
    DOCUMEnt       JAPANEse
    
    
    TABLE 15 - Possible continuations of the command
    
               Type ...
    
    
    <c-name>       HEAD           PUBLICations   <s-name>
    <f-name>       IDENTIfication <r-name>       <t-name>
    <g-name>       <i-name>       ROOT           TRANSLation
    
    
1
                                   - B.6 -

    TABLE 16 - Possible continuations of the command
    
               DELete ...
    
    
    AXIOM          <f-name>       Publications   SUBTREe
    <c-name>       <g-name>       <r-name>       THEOREm
    DEFINItion     <i-name>       <s-name>       <t-name>
    FILE           LEMMA
    
    
    TABLE 17 - Possible continuations of the command
    
               GET ...
    
    
    AUTHORs        FILE           KEY_PHrases    THEOREm
    AXIOM          <f-name>       LEMMA          <t-name>
    <c-name>       <g-name>       <r-name>
    DEFINItion     <i-name>       <s-name>
    
    
    TABLE 18 - Possible continuations of the command
    
               INForm [ABout] ...
    
    
    AGt            ENumerate      GTcl           PROVe
    Book           EXpression     INForm         Quantifiers
    CAlculate      FAcilities     INVestigate    Relabel
    CHeck          FILEs          Key            SENtence
    COLlaborators  FILMan         LEtter         SET
    COMmands       FIND           LIst           SHow
    CONnective     FINIsh         MEman          SOrt
    CReate         FORGet         MODify         STore
    DEFinitions    FORM           MOVe           SYstem
    DELete         FORMUla        PApers         Type
    DETermine      GENerate       PROCeedings    VAriables
    DRaw           GET            PROPer         VErbs
    
    
    TABLE 19 - Possible continuations of the command
    
               FORM <s-name> [AS [THE]] ...
                             [BY      ]
    
    
    All              EQuivalence                  IMPLICation
    Conjuction       EXClusive [Disjunction]      Negation
    Disjunction      EXists
    
    
1
                                   - B.7 -

    TABLE 20 - Possible continuations of the command
    
               FORM ...
    
    
    ADding                EXClusive [Disjunction]    PSEUDO_inverse
    ALl                   EXIsts                     Reduced
    BAsis                 <g-name>                   <s-name>
    BLOCK                 GENERAlized                SEMI_TOTAL_Line
    BLOCK_Cut_point       IMPLICation                SEMI_TOTAL_Point
    CLIque                <integer>                  SKeleton
    CLOsed_neighbourhood  INVERSE_Line               SPanning
    COMplement            ISOLATing                  SQuare
    CONJuction            JOIN                       STrong_product
    CONTracting           LEXICOgraphic_product      SUBgraph
    CORona                LINE                       SUM
    CUt_point             LOOP                       SUPergraph
    DEleting              Open_neighbourhood         SWitching
    DIGraph               NEGATIon                   TOtal
    DISjunction           PERMUTation                Union
    EQuivalence           PRODUCt
    
    
    TABLE 21 - Possible continuations of the command
    
               LIst ...
    
    
    ANY                       FACES                POINT_Eccentricities
    BLocks                    FOREST               POINT_Neighbours
    BRidges                   HAmiltonian_circuits POINT_orbits
    CEntre                    HExagons             Quadrangles
    CHAracteristic_polynomial Independent_circuits SEIdel_polynomial
    CHRomatic_polynomial      LINE_Colouring       SEMi_blocks
    CIRCUIT                   LINE_Degrees         SERial_lines
    CIRCUITS                  LINES                SPANNING_TREE
    COCliques                 MAXimal_matchings    SPANNING_TREES
    COEfficients              PArallel_lines       SUbgoals
    COMponents                PEntagons            Triangles
    CLiques                   POINT_Colouring      1-FACTOR
    CUt_points                POINT_Degrees        1-FACTORS
    <f-name>
    
    
    TABLE 22 - Possible continuations of the command
    
               SHow ...
    
    
    ABstracts   DEfinition   Manuscripts    SEntence
    ALl         DOcuments    Notions        SYstem
    ANy         FAmily       PApers         TAble
    AUthors     FIles        PRoceedings    THeorems
    AXioms      Graph        PUBLICations   TRee
    Books       Integer      PUBLIShers     VALid_formulas
    Complex     Journals     REAl           VARiables
    DAta        Key_phrases  REPorts        Words
                Lemmas
    
    
1
                                   - B.8 -

    TABLE 23 - Possible continuations of the command
    
               MODify Publication <i-value> Replacing LANguage [BY] ...
    
    
    BULGARian    ENGLISh      ITALIAn      RUSSIAn
    CHINESe      FRENCH       JAPANEse     SERBO_Croatian
    CZECH        GERMAN       POLISH       SPANISh
    DUTCH        HUNGARian    ROUMANian
    
    

1








    C) SYNTAX OF PROPER "GTCL" 




    <EXPRESSION> ::= <TERM> | +<TERM> | -<TERM> | <EXPRESSION>+<TERM> |
                     <EXPRESSION>-<TERM>
    
    <TERM> ::= <FACTOR> | <TERM>*<FACTOR> | <TERM>/<FACTOR>
    
    <FACTOR> ::= <PRIMARY> | <FACTOR>**<PRIMARY>
    
    <PRIMARY> ::= <NUMBER> | <N-VARIABLE> | <INDEXED-N-VARIABLE> |
                  (<EXPRESSION>)
    
    <N-VARIABLE> ::= <R-VARIABLE> | <I-VARIABLE> | <X-VARIABLE>
    
    <R-VARIABLE> ::= <R-LETTER> | <R-LETTER><NUMBER>
    
    <I-VARIABLE> ::= <I-LETTER> | <I-LETTER><NUMBER>
    
    <X-VARIABLE> ::= <X-LETTER> | <X-LETTER><NUMBER>
    
    <R-LETTER> ::= A | B | C | D | E
    
    <I-LETTER> ::= K | L | M | N
    
    <X-LETTER> ::= U | V | W | X | Y | Z
    
    <INDEXED-N-VARIABLE> ::= <N-VARIABLE>(<INDEX-SET>)
    
    <INDEX-SET> ::= <VALUE> | <INDEX-SET><VALUE>
    
    <VALUE> ::= <I-VARIABLE> | <X-VARIABLE> | <NUMBER>
    
    <FORMULA> ::= <EXPRESSION><RELATION><EXPRESSION>
    
    <RELATION> ::= '< | '> | '<= | '>= | = | # | @
    
    <NAME> ::= <VARIABLE> | <INDEXED-VARIABLE> | <SEQUENCE>
    
    <VARIABLE> ::= <N-VARIABLE> | <G-VARIABLE>
    
    <G-VARIABLE> ::= <G-LETTER> | <G-LETTER><NUMBER>
    
    <G-LETTER> ::= G | H
    
    <INDEXED-VARIABLE> ::= <VARIABLE>(<INDEX-SET>)
    
    <SEQUENCE> ::= <INDEXED-VARIABLE>(<SPAN-SET>)
    
    <SPAN-SET> ::= <SPAN> | <SPAN-SET>:<SPAN>
    
    <SPAN> ::= <I-VARIABLE>=<VALUE>,...,<VALUE> |
               <X-VARIABLE>=<VALUE>,...,<VALUE>
    
1
                                   - C.2 -

    <NUMBER> ::= <DIGIT> | <NUMBER><DIGIT>
    
    <DIGIT> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
    
    <VERB> ::= <SIMPLE-VERB> | <SIMPLE-VERB><NEGATION>
    
    <MULTI-SIMPLE-NOUN> ::= <SIMPLE-NOUN> |
                            <MULTI-SIMPLE-NOUN><SIMPLE-NOUN>
    
    <NOUN> ::= <MULTI-SIMPLE-NOUN> | <VALUE><MULTI-SIMPLE-NOUN>
    
    <ADJECTIV> ::= <SIMPLE-ADJECTIV> | <SPECIAL-ADJECTIV> | <VALUE> |
                   <EXPRESSION>
    
    <SPECIAL-ADJECTIV> ::= OF <NOUN-PHRASE> | <VALUE><SIMPLE-ADJECTIV> |
                           JOINED BY <SUBJECT> | WITHOUT <NOUN-PHRASE> |
                           OBTAINED FROM <NOUN-PHRASE> BY <NOUN-PHRASE>
    
    <NOUN-PHRASE> ::= <NOUN> | <NAME> | <NOUN><NAME> |
                      <ADJECTIV-PHRASE><NOUN> |
                      <ADJECTIV-PHRASE><NOUN><NAME> | <ARTICLE><NOUN> |
                      <ARTICLE><ADJECTIV-PHRASE><NOUN>
    
    <ADJECTIV-PHRASE> ::= <ADJECTIV> | <ADJECTIV-PHRASE><ADJECTIV>
    
    <PREDICATE> ::= <VERB><NOUN-PHRASE> | <VERB><ADJECTIV-PHRASE>
    
    <SUBJECT> ::= <NOUN-PHRASE> | <NOUN-PHRASE> OF <NOUN-PHRASE> |
                  <NOUN-PHRASE> AND <NOUN-PHRASE> |
                  <NOUN-PHRASE> OR <NOUN-PHRASE>
    
    <Q-SET> ::= <I-VARIABLE> | <X-VARIABLE> | <Q-SET><I-VARIABLE> |
                <Q-SET><X-VARIABLE>
    
    <QUANTIFIER> ::= FOR ALL <Q-SET> | THERE EXIST <Q-SET> SUCH THAT |
                     THERE EXISTS <Q-SET> SUCH THAT
    
    <SENTENCE> ::= <FORMULA> | <SUBJECT><PREDICATE> |
                   IF <SENTENCE> THEN <SENTENCE> |
                   <SENTENCE><KEY-WORD><SENTENCE> |
                   <MULTI-QUANTIFIER><SENTENCE>
    
    <MULTI-QUANTIFIER> ::= <QUANTIFIER> | <MULTI-QUANTIFIER><QUANTIFIER>
    
    <KEY-WORD> ::= AND | OR | IFF
    
    <VALUE> ::= <I-VARIABLE> | <X-VARIABLE> | <NUMBER>
    
    <NAME> ::= <I-VARIABLE> | <X-VARIABLE> | <R-VARIABLE> | <G-VARIABLE> |
               <INDEXED-VARIABLE> | <SEQUENCE>

1








    D) INTERNAL REPRESENTATIONS 



    By the command  

       SHOW DATA  <name> .
    
    the user can get the internal representation of the data whose name he
    has given. 







    D.1 GRAPH REPRESENTATION 



    A graph is represented by a sequence of integers as follows: 

    a) place 1: the number NP of points; 
    b) place 2: the number NL of lines; 
    c) places 3-12: vector IPRO (of dimension 10)  containing  information
       about several graph properties as explained below; 
    d) next 2*NL places: lines of  the  graph  represented  by  their  end
       points; 
    e) next IPRO(1)*NL places: weights of lines (weighted graphs  are  not
       processed in the recent version of the system); 
    f) next 2*NP places: coordinates of points when drawing a graph  (only
       if the graph has entered the system via light pen or after  command
       MODIFY; otherwise these 2*NP places are not used). 
    Coordinates of vector IPRO contains some  integers  according  to  the
    following scheme: 

       coordinate 1: 0 lines have no weight
                     1 integer weight
                     2 real weight
                     4 complex weight
    
       coordinate 2: 1 graph has no loops
                     2 graph has loops
    
       coordinate 3: 1 graph has no multiple lines
                     2 graph has multiple lines
    
    
    Coordinates 4-8 contain one of 0, 1, 2.  Each  coordinate  tells  some
    thing about a graph property. 0 means that this property has not  been
    checked; 1 denotes that graph has the  property  and  2  denotes  that
    graph has not the property. Properties for  coordinates  4-8  are  the
    following: bipartite, to be a tree, regular, planar, connected. 


1
                                   - D.2 -




    D.2 SENTENCE REPRESENTATION 


    A sentence is internaly represented by an integer  sequence  with  the
    meaning as follows:  

    a) integer 1: the length LC of the coded English text  
    b) integer 2: the length LF of the predicate formula  into  which  the
       sentence is translated 
    c) next LC integers: coded English text 
    d) next LF integers: coded predicate formula 
    e) next integer: the number ND of definitions used in  translation  of
       the sentence into the predicate formula 
    f) next ND integers: identification numbers of definition used 

    Hence, the total length of the sequence is LC+LF+ND+3 . 

    English text is coded according to the following scheme: 

    a) first LW integers: words of the sentence  are  coded,  each  of  LW
       words by an integer, 
    b) next integer: the  number  NEX  of  words  containing  mathematical
       simbols 
    c) next NEX integers: addresses of ends of these words in the sequence
       JEX described below; let n be the address of the last such word 
    d) next n integer: sequence JEX where  words  containing  mathematical
       symbols are stored one after another and coded so that each  symbol
       is represented by an integer 
    e) next NEX integers: addresses of the NEX words in  the  sequence  of
       words (first LW integers) 
    f) last integer: the number LW of words. 

    Each word is coded by a  positive  integer  with  the  exception  that
    plural  of  a  noun  gets  a  negative  integer,  opposite   to   that
    corresponding  to  singular  of  the  same  noun.   Words   containing
    mathematical symbols are of the following types and in the sequence of
    words they are coded by small negative integers: 

       non-negative integer    -1
       integer variable        -2
       point or line variable  -3
       real variable           -4
       graph variable          -5
       term                    -6
       formula                 -7
       indexed variable        -8
       sequence                -9
    
    
    In the sequence JEX words containing mathematical symbols are coded by
    the following table (each symbol by an integer): 

1
                                   - D.3 -

         (   -1          @  -18         L  -32         D  -42
         )   -2          '  -19         M  -33         E  -43
         ,   -3          +  -20         N  -34         U  -45
         =  -12          -  -21         G  -35         V  -46
         #  -13          *  -22         H  -36         W  -47
         <  -14         **  -23         A  -39         X  -48
        <=  -15          /  -24         B  -40         Y  -49
         >  -16          .  -25         C  -41         Z  -50
        >=  -17          K  -31
    
    
    Non-negative integers are coded by themselves. 

    If J is one of abone letters whose code is k and if n  is  a  positive
    integer then the code of variable Jn is k+(-20)n. 

    Meaning of some symbols: # diferent from, <= less than or equal to, >=
    greater than or equal to, @ divisibility  relation  (m@n  means  n  is
    divisible by m), n'=n+1,  * multiplication  symbol,  ** exponentiation
    symbol, / division symbol. 

    Variables are strings of at must five  symbols,  first  one  of  above
    letters and others being digits. Variables beginning with  letters  K,
    L, M, N, are integer variables, those with G, H graph variables; A, B,
    C real variables; D,E complex variables; U, V, W line variables; X, Y,
    Z point variables.  

    The formula into which the sentence is  translated  is  coded  by  the
    following table: 

    
              Coding symbols of predicate calculus
    
         (   -1          <  -14          )  -27          P  -39
         )   -2         <=  -15             -28          Q  -40
         ,   -3          >  -16             -29          R  -41
      NOT.   -4         >=  -17          $  -30          S  -42
      .OR.   -5          @  -18          K  -31          T  -43
     .AND.   -6          '  -19          L  -32          A  -44
        =>   -7          +  -20          M  -33          U  -45
       <=>   -8          -  -21          N  -34          V  -46
      .OR.   -9          *  -22          G  -35          W  -47
       ALL  -10         **  -23          H  -36          X  -48
       EXT  -11          /  -24          F  -37          V  -49
         =  -12          .  -25          O  -38          Z  -50
         #  -13          (  -26
    
    
    Conventions for coding non-negative integers and strings in which  one
    of above letters is followed  by  digits,  are  the  same  as  in  the
    previous table. 

    Strings beginning with letters K-N, G-H, U-Z, have the same meaning as
    before, those  with  O - constants,  then  those  with  P-T  predicate
    letters and, finally, those with A - symbols of graph operations. 

    Predicates beginning with P, Q, R, S, T have 0, 1, 2, 3,  4  arguments
    respectively. 

    Brackets coded by -26 and -27 are used only for denoting arguments  of
    a predicate or of a function. 
1
                                   - D.4 -


    Although the user cannot see records in files it  could  be  sometimes
    useful to know the structure of records. 

    RECORDS IN THE WORD FILE: 

    a) places 1-8: words have at most 16 letters and 8 first places  in  a
       record are reserved for these letters 
    b) place 9: the number of letters 
    c) place 10: code (a positive integer) 
    d) place 11: grammatical type ( 1 for articles, 2 for negations, 3 for
       auxiliary words, 4 for verbs, 5 for nouns and 6 for adjectives) 
    e) place 12: the number of definitions in which  a  notion  containing
       this word is used (at most 5) 
    f) place 13: the number of key phrases in which this word is contained
       (at most 8) 
    g) places 14-18: identification number of the definitions 
    h) places 19-23: identification number of key phrases. 

    Words are ordered alphabetically. 

    RECORDS IN THE DEFINITION FILE: 

    a) place 1: identification number; 
    b) place 2: the number ND of definitions used by this definition; 
    c) place 3: the number NDD of definitions which use this definition; 
    d) place 4: the length LCN of the coded English text of the notion; 
    e) next LCN places: notion coded as the text of a sentence; 
    f) next  LCD+LFD+2  places:  definition  (coded  English  text  +  the
       corresponding predicate formula) stored as in a sentence ( LCD  and
       LFD are at the beginning); 
    g) next ND places: identification numbers of definitions used by  this
       definition; 
    h) next NDD places: identification numbers  of  definitions  in  which
       this definition is used. 




    D.3 PROOF TREE REPRESENTATION 


    A proof tree is represented by  a  sequence  of  integers.  First  ten
    positions represent the head of the tree.  Other  positions  represent
    points of the tree, each point  being  described  by  three  positions
    (integers).  The  points  are  actual  points  of   the   tree   (each
    representing a subgoal  in  the  proof)  or  potential  (free)  points
    reserved for extension of the tree. 

    The proof tree is represented as a  rooted  chained  tree.  In  actual
    points we  have  pointers  to  their  "relatives"  ("sons",  "father",
    "brothers") and free points are chained (always having a  pointers  to
    the next free point). Pointers give relative addresses  of  some  data
    with respect to the first place (integer) in the tree. 

    The head has the following form: 

    a) position 1: the number NP of all points (actual and potential) 
    b) position 2: number of free points; 
    c) position 3: address of the  first  position  of  the  "first"  free
                   point; 
1
                                   - D.5 -
    d) position 4: address of the first position of the "last" free point; 
    e) position 5: address of the first position of the root; 
    f) position 6: number of positions per a point (always 3); 
    g) position 7: length of the head (always 10);  
    h) position 8: address of the  record  (in  the  subgoal  file)  where
                   information about recent lemmas  (produced  by  command
                   "MODIFY <t-name> .") is stored; 
    i) positions 9-10: not used. 

    In free points the second and the  third  position  contain  0.  First
    position contains the address of the first position of the "next" free
    point. "Last" free point has 0 also in the first position. 

    In actual points we have the following: 

    a) position 1: address of the first "son" if it exists; othetwise 0 if
       the subgoal is not proved and -1 if it is proved; 
    b) position 2: address of the "next brother"; if  the  "next  brother"
       does not exist then address of the "father" with minus sign; if the
       "father" does not exist (only for the first point) then 0; 
    c) position 3: identification number of the sentence representing  the
       subgoal (subgoals are stored in a special file). 

    The length of the tree is 10+3*NP . 




    D.4  FAMILY REPRESENTATION 


    Members of a family are sets of integers. A family  is  determined  by
    the number N of members and by two vectors: ENDS  with  N  coordinates
    and RECORD with ENDS(N) coordinates. Members of the family are  stored
    one behind another into the vector RECORD.  For  each  member  of  the
    family vector ENDS gives the address of its end in the vector RECORD. 

    Families which are under certain names memorized in the system "Graph"
    are internally represented by a sequence of integers consisting of the
    number N and coordinates of vectors ENDS and RECORD  taken  one  after
    another. 




    D.5 NUMERICAL VALUES 


    Numerical values are data of type INTEGER, REAL,  and  COMPLEX.  Their
    internal representation is the same as used  by  the  standard  PDP-11
    hardware and software. Using memory space occupied by an integer value
    as a unit, any real value occupies space as 2 integer values, and  any
    complex value as 4 integers (first two places represen the  real  part
    and the second two places the imaginary part of the value). 


1








    E) DESCRIPTION OF GRAPH CATALOGUES AND SOME OTHER FILES 




    There are the following catalogues of graphs and  other  objects  (for
    each catalogue the logical and the physical name of the  corresponding
    file is given): 

            catalogue                         logical name  physical name
    
    1. connected graph up to 6 points               SIXPO     USER.SIX
    2. regular graphs up to 10 points               REGUL     USER.RGL
    3. trees up to 10 points                        TREES     USER.TRS
    4. connected cubic graphs on 12 points          CUBIC     USER.CUB
    5. self-complementary graphs up to 9 points     SELFC     USER.SFC
    6. sets of cospectral non-isomorphic graphs     PINGS     USER.PNG
    7. integers from 1 to 99                        INTEG     USER.INT
    8. sets of small integers                       COMBI     USER.CMB
    
    
    We shall give below some details on these catalogues. 

    1. The 141 connected graphs up to six points are  stored  under  names
       which begin with G, the second character  denoting  the  number  of
       points. Graphs are ordered lexicographically by  spectral  moments.
       The order of the 112 graphs on six points coincides  with  that  of
       [1]. 

    2. The 250 regular graphs up to  10  points  are  stored  under  names
       beginning with G. The second character  in  the  name  denotes  the
       number of points (for graphs on 10 vertices the digit 0  is  used);
       the third one denotes the degree of the graph. Graphs  are  ordered
       lexicographically by spectral moments as given in [2]. 

    3. Trees up to 10 points are stored under names  GT001  -  GT200.  The
       order  is  the  same  as  in  [3]  (the  lexicographic   order   by
       coefficients of the characteristic polynomial). 

    4. Connected cubic graphs on 12 vertices are stored under names G01  -
       G85. The order is lexicographic by eigenvalues [4]. 

    5. The 50 self-complementary graphs up  to  nine  points  are  ordered
       lexicographically by spectral moments. Names of graphs  begin  with
       HS, the third character denoting the number of points. 

    6. A few sets of non-isomorphic cospectral graphs are given. Names  of
       graphs begin with G, the second character  denotes  the  number  of
       points. 

    7. Integers 1,2,...,99 are stored under names I01, I02, ..., I99. 

    8. All non-empty  sets  with  at  most  four  elements  consisting  of
       integers 1,2,...,9 are stored as families (names begin with F). The
       second character denotes the cardinality of the set. 

1
                                   - E.2 -

                        

    The names of objects in these files can be obtained by the command 

       SHOW VARIABLES IN FILE <logical name> .
    
    
    The objects can be moved into the main memory by the command 

       GET <name> FROM FILE <logical name> .
    
    
    The content of system's files related to the bibliography and  theorem
    prover can be obtained by command SHOW and FIND as described  in  this
    Manual. The work file contains  over  thirty  sentences  (whose  names
    begin with SDR) which are suitable for introductory  experiments  with
    the theorem prover. 




    R E F E R E N C E S 


    1. Cvetkovic D., Petric  M.:  A  table  of  connected  graphs  on  six
       vertices, Discrete Math., 50(1984), 37-49 

    2. Cvetkovic D., Radosavljevic Z.: A table of regular graphs  with  at
       most 10 vertices, in preparation 

    3. Cvetkovic D., Doob M., Sachs H.: Spectra of  graphs  -  Theory  and
       application, Deutscher Verlag der Wissenschaften - Academic  Press,
       Berlin - New York, second edition, 1982 

    4. Bussemaker F.C., Cobeljic S., Cvetkovic D., Seidel  J.J.:  Computer
       investigation of cubic graphs, Technological University  Eindhoven,
       T.H.-Report  76-WSK-01;  Cubic  graphs  on  <=  14   vertices,   J.
       Combinatorial Theory (B), 23(1977), 234-235 



























