Home Latest Advanced Search By Year By Division 

Not Logged in. Login 
Herbrand's Theorem and Equational Reasoning: Problems and SolutionsDegtyarev, 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. 303326. ISBN 0444829490
AbstractThe 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 socalled simultaneous rigid Eunification problem. In the second part, we survey recent result on the simultaneous rigid Eunification problem.
Repository Staff Only: item control page 
Accessibility  Terms and Conditions  Last Modified 01 November 2007 
© 2007 DCS, King's College London, Strand, London WC2R 2LS, England, United Kingdom. Tel +44 (0)20 7836 5454 