***********************************************************
***********************************************************
README file

KOLA Theorem Proof Scripts

June, 1998

***********************************************************
***********************************************************

--------------------
REQUIREMENTS
--------------------

The Specifications of KOLA and the Proof Scripts used to Verify KOLA
Rewrite Rules and COKO transformations use the Larch Specification tool
(LSL version 3.1 beta 3) and Theorem Prover (LP version 3.1 alpha).
These can be retrieved from:

   http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html              

--------------------
INSTALLATION
--------------------

1. If necessary, install the Larch Specification tool (LSL) and 
   theorem prover (LP) as per the instructions located at the
   Larch web site at MIT.

2. Create a directory in which to install the KOLA Specifications
   and Proof Scripts.  From here on in, we will refer to this directory as <local_dir>.

3. If you haven't already, download the tar'd and
   compressed KOLA specification package, kola.tar.Z, 
   into <local_dir>.

3. The next two steps describe how to uncompress and untar the kola.tar.Z file.
   After step 2a, kola.tar.Z will be renamed to kola.tar.
   After step 2b, there will be new directories under
   <local_dir>. These directories will contain the compilable
   KOLA specifications and theorem prover scripts.
   
   a. To uncompress the compressed file, kola.tar.Z, type:

	    uncompress kola.tar.Z 

   b. To untar the tar file, kola.tar, type:

	    tar xvf kola.tar


--------------------
DIRECTORIES
--------------------

The result of 'untarring' the KOLA file is the following
tree of directories:

                 <local_dir>/
                     |
  -------------------------------------------------
  |         |              |      |       |       |     
 COPYRIGHT Makefile      README   kola/  aux/   scripts/

 1. COPYRIGHT: copyright statement for the entire KOLA package
 
 2. Makefile: 

 3. README: this file

 4. kola: This directory contains the KOLA specifications

 5. aux:  This directory contains KOLA specifications required
		  to compile the Theorem Prover Scripts

 6. scripts:  This directory contains the Theorem Prover Scripts
		  for the following rewrite rules and transformations:

		  cnf-scripts:			Rewrite rules for the CNF Transformation, presented in [CZ98a]
		  snf-scripts:			Rewrite rules for the SNF Transformation, presented in [CZ98a]
		  pushdown-scripts:		Rewrite rules for the Pushdown Transformation, partially presented in [CZ98a]
		  magic-scripts:		Rewrite rules for the Magic Sets Transformation, partially presented in [CZ98a]
		  SIGMOD98_Scripts:		Rewrite rules for all transformations presented in [CZ98a]
		  VLDB98_Scripts:		Rewrite rules for all transformations presented in [CZ98b]


-----------------------------------
"Executing" The KOLA Specifications
-----------------------------------

1.  Adjust the values set to variables

     LSL, and
     LP

    in the makefile located at <local_dir>/Makefile so
	that they are set to the locations of the lsl specification
	compiler, and lp theorem prover at your site.

2.  From the main directory (<local_dir>), type "make specs"

	cd <local_dir> 
	make specs

   This will compile all of the KOLA specifications located
   in <local_dir>/kola.  Alternatively, individual specifications
   can be compiled by typing:

    cd <local_dir>
	make <operator>_Axioms.lp

   such that <operator>.lsl is the name of the file in <local_dir>/kola
   that is to be compiled.  (For example, to compile the specification
   for KOLA's Iterate former, one would type:

   cd <local_dir>
   make Iterate_Axioms.lp

3.  To begin again at any point, first type "make clean" from <local_dir>.

	cd <local_dir> 
	make clean

--------------------------------------
"Executing" The Theorem Prover Scripts
--------------------------------------

1.  Adjust the values set to variables

     LSL, and
     LP

    in the makefile located at <local_dir>/Makefile so
	that they are set to the locations of the lsl specification
	compiler, and lp theorem prover at your site.

2.  From the main directory (<local_dir>), type "make proofs":

	cd <local_dir> 
	make proofs

   This will first compile all KOLA specifications located
   in <local_dir>/kola, and then execute the theorem prover
   scripts:

     <local_dir>/scripts/SIGMOD98_Scripts.lp, and
     <local_dir>/scripts/VLDB98_Scripts.lp

   for the transformations and rules used in our papers
   [CZ98a] and [CZ98b] respectively.  After execution, 
   <local_dir> will contain log files from the execution
   of the theorem prover:

     <local_dir>/scripts/SIGMOD98_Scripts.lplog, and
     <local_dir>/scripts/VLDB98_Scripts.lplog

   Alternatively, individual proof scripts can be executed
   by typing:

    cd <local_dir>
	make <script_filename>.lplog

   such that <script_filename> is the name of the file in <local_dir>/scripts
   containing the theorem prover scripts to be executed.  (For example, to compile the scripts
   establishing the correctness of the CNF transformation presented in [CZ98a], one
   would type:

    cd <local_dir>
    make cnf-scripts.lp

   After execution, <local_dir> will contain the log file from this execution
   (cnf-scripts.lplog).

3.  To begin again at any point, first type "make clean" from <local_dir>.

	cd <local_dir> 
	make clean


-------------------
Caveats
-------------------
These specifications and scripts have been tested with the Solaris (Sparc)
versions of the Larch specification tool and prover.  No testing
has been done on any other platform.
     
-------------------
References
-------------------
[CZ98a] Changing the Rules: Transformations for Rule-Based Optimizers     
        Mitch Cherniack and Stan Zdonik, In Proceedings of the 1998 ACM   
        SIGMOD International Conference on Management of Data, Seattle,   
        WA, June, 1998.                                                   
                                                                          
		For an up-to-date version of [CZ98a], see:                                
		  ftp://wilma.cs.brown.edu/u/mfc/sigmod98.ps.Z                          
     
[CZ98b] Inferring Function Semantics to Optimize Queries,                 
        Mitch Cherniack and Stan Zdonik, In Proceedings of the 24th       
        International Conference on Very Large Data Bases, New York,      
        NY, August, 1998                                                  
                                                                          
		For an up-to-date version of [CZ98b], see:                        
		  ftp://wilma.cs.brown.edu/u/mfc/vldb98.ps.Z                      


-------------------
PLEASE NOTE
-------------------
     
Please report any difficulties executing the specifications and/or
theorem prover scripts to mfc@cs.brandeis.edu