A first-order theory whose consequences can be decided by an algorithm that terminates on every input first-order sentence. Decidability of a chosen axiom set alone does not ensure decidability of its consequences.
New to topics? Read the docs here!