Herbrand’s Theorem and Equational Reasoning: Problems and Solutions

The article (written in a popular form) explains that a number of different algorithmic problems related to Herbrand’s theorem happen to be equivalent. Among these problems are the intuitionistic provability problem for the existential fragment of first-order logic with equality, the intuitionistic provability problem for the prenex fragment of first-order with equality, and the simultaneous rigid E-unification problem (SREU). The article explains an undecidability proof of SREU and decidability proofs for special cases. It contains an extensive bibliography on SREU.