|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
Herbrand's Theorem and Equational Reasoning: Problems and Solutions
Degtyarev, Anatoli and Gurevich, Yuri and Voronkov, Andrei (2001) Herbrand's Theorem and Equational Reasoning: Problems and Solutions. In: Current trends in theoretical computer science: entering the 21st centuary. World Scientific, pp. 303-326. ISBN 0-444-82949-0
The famous Herbrand's theorem of mathematical logic plays an important role in automated theorem proving. In the first 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-unification problem. In the second part, we survey recent result on the simultaneous rigid E-unification problem.
Repository Staff Only: item control page