Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
  
Screen decoration graphicsLogo

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

[img]Postscript - Repository staff only - Requires a viewer, such as GSview
235Kb

Abstract

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.

Item Type:Book Section
Subjects:UNSPECIFIED
ID Code:889
Deposited By:Dr Anatoli Degtyarev
Deposited On:08 Nov 2007 08:33
Last Modified:08 Nov 2007 08:33

Repository Staff Only: item control page