  Consider for instance the case of Gregory Brumfiel, a real algebraic geometer. In his book “Partially ordered rings and semi-algebraic geometry” (1979), Brumfiel contrasts different methods for proving theorems about real closed fields. One of them relies on a decision procedure for a particular axiomatization of the theory of real closed fields. By this method one can find elementary proofs of sentences formulated in the language of that theory—at least in principle, since, as Brumfiel remarks, “it certainly might be very tedious, if not physically impossible, to work out this elementary proof.” (166)