Some first-order theories are algorithmically decidable; examples of this include Presburger arithmetic, real closed fields and static type systems of many programming languages.
Unele teorii de ordinul întâi sunt algoritmic decidabile; exemple în acest sens includ aritmetica Presburger⁠(d), corpurile reale închise⁠(d) și sistemele de tipare statică⁠(d) ale multor limbaje de programare.