This readme file gives an overview of the code used for LT.

The directory CODE contains all of the code needed to run lt.  The files have
the following contents and uses:

OLDCODE is a directory which contains early versions of LT which were made 
	superfluous for some reason or other.

PROBS   contains problems from principia mathematica. 
		p2 holds problems from chapters 2 and 3.
		chs4and5 holds problems from chapters 4 and 5.

comp_gen_lt  	compares the generality of two sets of learned theorems.

do_tex	     	loads files to generate tables in LaTeX format from a 
		saved state.

foreign		is used by tabular2 to load the foreign math functions from
		math.c

logic		is a quick and dirty theorem prover that uses a generate
		and test algorithm to explore all truth values.  

make_driver	creates a file that runs all of the problems in a given order.
		It does not do anything, except generate calls to lt/2 in
		one of the running versions of LT. 

math.c		is a list of c functions needed for computation of statistics
		for tabular2

math.o 		is the object file from math.c

pstart		is the precedences required to interpret the logic symbols

tabular2	generates tables in LaTeX format from a saved state.

lt		is the running version of LT.  It has no implies restriction,
		and assumes no provens.  There are some minor variations on
		this program found in this directory as well.  They are:
		
		no_assume_lt, which does not assume non-provens.
		imp_lt,  which has the implies restriction, but assumes
				non-provens.
		inst_lt, which does not learn instances,
				has no implies restriction, and assumes
				non-provens?