I have been reading some papers where I keep reading stuff like “first-order formula modulo a background theory”. Does anyone know what modulo means in this case ? Is it something like “with respect to”?
A theory, in this sense, is an equivalence relation on the formula, which states when these formula are equivalent (as in: $F$ is equivalent to $G$ iff $F$ implies $G$ and $G$ implies $F$). The theory is usually presented by a set of deduction rules, though this is not an obligation.
The word theory is often used in the context of rewriting systems: if you have rules to rewrite terms (which may be formulas, but the concept is more general) of the form $t \rightarrow t'$, then the induced equivalence relation $t_1 (\leftarrow \cup \rightarrow)^* t_2$ (any number of rewriting steps, alternating directions as often as desired) is the equational theory of this rewriting system.
Technically, “first-order formula modulo a theory $T$” means that you are manipulating equivalence classes which are sets of formulas. Intuitively and practically, this is saying that we are manipulating formulas, but we may replace a formula by some other equivalent formula at any time.
In first order logic there are formulae that are not necessarily valid. The equality
$x + y = y + x$
does not hold for arbitrary interpretations of equality and the addition symbol. It does hold for the interpretation of $+$ and $=$ in standard arithmetic. So if we assume the theory of Peano arithmetic (or first order arithmetic, or even Presburger arithmetic), then, the first order formula is said to be true "modulo a background theory".
More generally, if you assume you are working with a specific theory such as a fragment of arithmetic, or a theory of strings, or lists, or any of the many logical theories that exist, the phrase "true modulo a background theory" means, you are assuming first order logic with some axioms which will not be repeated explicitly every time.