Unfortunately while valid logical formulas have finite deductions, proving that a formula is not valid (or equivalently that some formula is satisfiable) is Tur

Unfortunately while valid logical formulas have finite deductions, proving that a formula is not valid (or equivalently that some formula is satisfiable) is Turing complete and thus impossible. So the set of valid first order formulae is recursively enumerable. However, if you limit your scope to finite sets bounded by some size, the problem is merely NP-complete. Given a program, you can construct a formula which is satisfiable iff the program halts (with said formula being polynomial in size with respect to the size of the program).