Home

Lectures on Jacques Herbrand as a Logician

Wirth, Siekmann, Benzmueller & Autexier. Lectures on Jacques Herbrand as a Logician. SEKI Report SR-2009-01.

Herbrand's work, more than that of any other, provides the intellectual foundations of logic programming. This very readable article discusses Herbrands' contributions to proof theory and the formulation of the idea of a recursive function, and most importantly to PL, his fundamental theorem that yields a semi-decision algorithm for first-order logic and his unification algorithm.

By Charles Stewart at 2009-06-05 13:42 | Theory | other blogs | 8208 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Herbrand Logic

This is an interesting and closely related paper: Herbrand Logic.

By Hank Thediek at Thu, 2009-06-11 02:37 | login or register to post comments

Is Herbrand Logic Herbrand's logic?

This article nicely summarises a thesis, that the interpretation of structures given in first-order logic into the structure's Herbrand universe is usually the best interpretation, which seems to be widespread in the theory of Prolog.

Pay attention to theorem 6: this thesis only makes sense with theories whose axioms are in Skolem normal form. This is quite hairy for theories with axiom schemas: eg. ZFC's axiom of replacement, so one usually wants to recast such theories into a higher-order theory with appropriate second-order variables to replace the schemas.

I'm guessing that Herbrand didn't actually advocate the thesis in this paper.

By Charles Stewart at Thu, 2009-06-11 13:22 | login or register to post comments

Herbrand's Logic?

I'm guessing that Herbrand didn't actually advocate the thesis in this paper.

I am guessing that you are right. In the introduction the authors define Herbrand logic as first-order logic plus Herbrand semantics. This seems to be sufficiently different to require a new definition.
The introduction tells a story of how the paper came about and why.

By Hank Thediek at Thu, 2009-06-11 17:42 | login or register to post comments