|
Abstract : |
The famous Herbrand's theorem of mathematical logic plays an important role in automated theorem proving. In the rst part of this article, we recall the theorem and formulate a number of natural decision problems related to it. Somewhat surprisingly, these problems happen to be equivalent. One of these problems is the so-called simultaneous rigid E-unication problem. In the second part, we survey recent result on the simultaneous rigid E-unication problem. Note. This article complements the original version [11] by mentioning the new results and references to recently published papers. However, we tried to preserve the original text for historical reasons, so the new material is given as footnotes., |
