On the practical value of Herbrand disjunctions
Uwe Petermann · Logic and Logical Philosophy · 2004
Herbrand disjunctions are a means for reducing the problem of whether a first-oder formula is valid in an open theory T or not to the problem whether an open formula, one of the so called Herbrand disjunctions, is T -valid or not. Nevertheless, the set of Herbrand disjunctions, which has to be examined, is undecidable in general. Fore this reason the practical value of Herbrand disjunctions has been estimated negatively (cf. [30]). Relying on completeness proofs which are based on the algebraization technique presented in [30], but taking a more optimistic view, we show how Herbrand disjunctions become the base of a method for building in theories into automatic theorem provers [26]. Surveying newer results we discuss how to treat heterogeneous theories [29] as well as practical implications of different normal form transformations.