As a logic-based system, a SNePS KB consists of a set of terms, and functions and formulas over those terms. The set of logical connectives and quantifiers extends the usual set used by first-order logics, all taking one or more arbitrarily-sized sets of arguments. In accord with the intended use of SNePS to represent the mind of a natural-language-competent intelligent agent, propositions are first-class entities of the intended domain, so formulas are actually proposition-denoting functional terms. SNePSLOG, the input-output language of the logic-based face of SNePS, looks like a naive logic in that function symbols (including "predicates"), and formulas (actually proposition-denoting terms) may be the arguments of functions and may be quantified over. The underlying SNePS, however, is a first order logic, with the user's function symbols and formulas reified.