Propositional logic is a kind of formal logic that studies statements and their relationships. It is the foundation of first-order logic.
A statement is a sequence of words conforming to the syntactical and grammatical rules of a natural language, plus some additional rules specific to propositional logic:
A machine can process statements as merely syntactic structures, without making any attempt to interpret their semantic content, and thereby infer new statements.
Propositional logic has limited capacity for abstraction: it doesn't allow reasoning over variables and functions having mutable and general content.
Well-formed formulas (WFFs) are sequences of symbols (syntactic structures) that hold a truth value, analagously to propositions. There are rules for operating on WFFs that constitute propositional calculus. Only on WFFs can we perform inference and prove theorems.
All propositions are well-formed formulas. We can connect them into larger WFFs (compound propositions) by way of logical operators.
not
and
or
implication
A clause is a collection of literals joined by some logical connective, usually ∨ ("disjunctive clause") but sometimes ∧ ("conjunctive clause").