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.

color_base.plf:

This file gives some basic definitions for interpolant-generating calculii in LFSC, including a simplify function for formulas to reduce the size of interpolants produced

color_euf.plf:

This file gives the basic definitions for interpolant-generating calculii for the theory of uninterpretted functions with equality (EUF).  Some side conditions such as "color_mark" and "color_mark_formula" are used to color terms and formulas as containing variables from A/B.

euf_interpolation.plf:

This file defines a particular interpolant-generating calculus for EUF, based on the procedure described in "Ground Interpolation for the Theory of Equality" (Fuchs et al).  More details on this proof signature can be found in "Certified Interpolation for EUF" (Reynolds et al).