sat.plf:

Contains the definitions of variables, literals, clauses and rules for (deferred) resolution.  The simplify operation in Figure 8 is defined in the "simplify_clause" side condition.

smt.plf:

Contains definition of "term" and additional definitions for function types.  The definition "arrow" is the type used for function types and "apply" represents the binary application of a function to an argument.  
Also contained is the definition of equality and distinct, and rules for natural deduction.

th_base.plf:

Contains some of the basic rules for SMT proofs, including mappings between literals and boolean variables (see "atom"), clausifications, and "let" rules for proofs.  Other rules for theory lemmas such assume true/false (see "ast"/"asf"), and rules for equality "trans"/"symm"/"cong" are given.

th_real.plf:

Basic definitions for the Real theory.  A real term is of type (term Real) where Real is a base type.  Reals are represented as rationals in the gnu mp library (given by the built-in LFSC type "mpq").  A term of type (term Real) can be constructed from a constant in the gnu mp library using the defintion "a_real". 
This file also contains basic transitivity and normalization rules for arithmetic predicates.

th_lra.plf:

This defines proof rules for the "lra" signature for QF_LRA.  Real variables are represented as terms of type "var_real".  A term of type "(term Real)" representing such a variable can be constructed using "a_var_real".  A list of monomials can be constructed using "lmonn"/"lmonc".  A linear polynomial can be constructed with "polyc".  Finally, "poly_term" is effectively used to cast polynomials to terms, so that polynomial representations may be used in arithmetic predicates over terms.
Rules given in the text such as lra_add=~ represent multiple rules whose concrete syntax is "lra_add_=_>", for example.  The rules given in the text as pol_norm+ are defined as "pn_+", for example.  Note that in the later, judgements of the form (poly_norm p t) are used, which says that p is the resulting normalized polynomial equivalent of term t  (written as t=p in the text).  The pol_norm~ rule given in the text represents multiple rules, such as the rule "poly_norm_>=" in concrete syntax.
Here is a summary of side conditions in this signature:
- (lmon_neg l) negates the linear monomial list l. 
- (lmon_add l_1 l_2) concatenates (adds) the linear monomial lists l_1 and l_2.  
- (lmon_mult_c l c) multiplies each element of linear monomial list l by constant c. 
- (poly_neg p) negates the constant and monomial parts of polynomial p.
- (poly_add p_1 p_2) componentwise adds the constant and monomial parts of polynomials p_1 and p_2.  
- (poly_sub p_1 p_2) componentwise subtracts the constant and monomial parts of polynomials p_1 and p_2.  
- (poly_mult_c p c) multiplies the constant and monomial parts of polynomial p by constant c.  
- (isolate v l) returns the pair (c, l'), where l = c*v + l', where v is not in FV(l'). 
- (isolate_h v l) is a helper function for isolate. 
- (is_lmon_zero l) returns true if linear monomial list l simplifies to zero.  
- (is_poly_const p) if the monomial component of p is zero, return the constant component of p, and fail otherwise. 

th_lra-cvc3.plf:

This defines proof rules for the "lrac" signature for QF_LRA, which is described in the appendix of the technical report "CVC3 proof conversion to LFSC".  The concrete names for proof rules mostly follow names mentioned in this text.  Many of these rules mimic the native rules of cvc3's proof format, with a few exceptions.  Side conditions are used to simulate the effect of certain cvc3 inferences, including and/or elimination and normalization operations.  Some additional rules are provided in this file that were used specifically to handle cvc3 proofs for LRA.