    This directory contains axiomatizations for several sample theories, as
well as a file containing the help messages for LP.  Future releases of LP will
provide a library of more fully developed theories.

                                --- Booleans ---

bool            Partial axiomatization of booleans
boolequiv       Complete axiomatization in terms of disjunction, equivalence
boolxor         Complete axiomatization in terms of conjunction, exclusive-or


                          --- Abstract Data Types ---

list		Complete axiomatization of finite lists
set1		Partial axiomatization of finite sets 
		(generated by empty and insert)
set2		Equationally complete axiomatization of finite sets
		(generated by empty, singleton, and union)


                      --- Number Systems and Functions ---

ackermann	Ackermann's function
int		Equationally complete axiomatization of integers
nat		Equationally complete axiomatization of natural numbers


                           --- Algebraic Systems ---

group 		Groups defined by the usual three equations
group1		Groups defined by one equation (in terms of /)
group2		Groups defined by two equations (in terms of /)
grt 		Groups defined by surjectivity of right and left translations
l-r		L-R systems
taussky		Taussky axioms for groups


                  --- Algebraic Systems with AC Operators ---

abgrp		Abelian groups
b-ring		Boolean rings
c-ring		Commutative rings
c-ring-u	Commutative rings with unit element
lattice		Free distributive lattices
ring		Rings
ring-u		Rings with unit element
