README.txt
       colog14I  
       2/7/2023

    colog14I.zip (~2.3MB) contains colog component Java sources and classes,
    colog14I.jar, and utility files. 

    Unzip colog14I.zip.  Locate the colog14I folder in a convenient work location.

    This archive was compiled with the help of the ANTLR3.5.3
    parsing tool antlr-3.5.3-complete.jar {see https://www.antlr3.org/download.html}
   
    Inside the colog4I folder ...
      
      colog.jar (~339KB) 
         Executable jar file -- double click opens the app on desktop.
         colog program files can be dropped on the theory pane. The ???
         tab on the right pane has some basic colog information.

      org/ 
         This folder contains the antlr-3.5.3-complete.jar extracted runtime 
         classes (org/antlr/runtime/*) required to parse colog and fol inputs 
         to the colog14I app. 
   
      colog.java
         This file is a top-level driver component for 
         colog prover (gui or cpommand-line).
   
      sam/ (Skolem Abstract Machine)
         This folder is the primary components package for the
         colog14I theory parser and the various inference components.
   
      makeall  
         Read this source file in a text editor to see details.
         This source file will:
            1- remove jar and class files from the archive
            2- compile all the .java source files in the archive 
            3- create the colog14I.jar app file
         Assuming that fp is the full system path to colog14I 
         (e.g., fp is  ~/colog14I), the makeall command can be 
         executed like this :
               > source fp/makeall fp

   If one modifies the colog input grammar (sam/lang/antlr/colog.g), 
   then the colog lexer and parser need to be regenerated. 
   Similarly for the grammar Fol.g (sam/fol/antlr/Fol.g).
   See files sam/lang/antlr/compile and sam/fol/antlr/compileFol
   to inspect  relevant compile commands.
   
   License
      The colog14I sources are copyrighted.  There are no
      restrictions on copying, changing or extending
      as long as original sources are cited.
_____________________________________________________________________

   SPECIAL NOTE regarding colog "false" rules and "goal" rules: The 
   sam.lang.CologAnalyzer does not enforce the following conventions
   and that can cause misleading or incorrect colog app reports, or 
   promote unnecessary inferences. The colog programmer needs to heed 
   the following (unchecked) conventions. 

   1.  false-BEFORE-goal
    All "false" rules should come before all "goal" rules in a colog 
    theory for the following reason. Consider the simple theory ...
          true => p, q.
          q => goal.
          p => false.
    If one loads this little theory into the colog14I app, 
    the following inference tree is generated 
            true 
             |
             p
             |
             q
             |
            goal
    and the report is that a PROOF was found, which is misleading, because 
    the order of the rules did not allow the false 3rd rule to apply soon 
    enough. Move the false rule up before the goal rule...
          true => p, q.
          p => false.   // N.B. "false before goal"
          q => goal.
    The colog app now generates the following inference tree.
         true 
           |
           p
           |
         false
    and the report is that a PROOF (i.e. REFUTATION proof) was found, which is 
    logically correct.  The motto is: CATCH CONTRADICTIONS EARLY. Exercise: 
    formulate a small theory illustrating the need for the false-BEFORE-goal 
    principle for a consistency rule, such as ' ~p(X),p(X) => false. ' 

    2.  false-BEFORE-goal EARLY in the theory
    The reason for this is to avoid unnecessary colog inferences on branchs 
    that could have terminated earlier using a goal rule. For example, try the 
    following example which uses late false rule and goal rule.
          true => p.
          p => q | r. 
          q => u | v.
          r => w | x. 
          u => false.
          p => goal. 
    Observe the PROOF (4 branches), and then run again after moving the last 2 rules 
    to the top (PROOF, 1 branch).
          u => false.
          p => goal. 
          true => p.
          p => q | r. 
          q => u | v.
          r => w | x. 
    The 2nd version avoids unnecessary inferences for a PROOF.
    
    When in doubt: false-BEFORE-goal and then the other rules in the theory.
    Also: DO NOT use goal or false as literals in any rule antecedent or in 
    conjunction with other consequent literals or in disjunctive consequent 
    colog rules.