Sciweavers

Share
CSL
2001
Springer

On a Generalisation of Herbrand's Theorem

9 years 27 days ago
On a Generalisation of Herbrand's Theorem
In this paper we investigate the purely logical rule of term induction, i.e. induction deriving numerals instead of arbitrary terms. In this system it is not possible to bound the length of Herbrand disjunctions in terms of proof length and logical complexity of the end-formula as usual. The main result is that we can bound the length of the reduct of Herbrand disjunctions in this way. (Reducts are defined by omitting numerals.)
Matthias Baaz, Georg Moser
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where CSL
Authors Matthias Baaz, Georg Moser
Comments (0)
books