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.)

• Type: Conference
• Year: 2001
• Where: CSL
• Authors: Matthias Baaz, Georg Moser
• Keywords: Automated Reasoning, CSL 2001, Herbrand Disjunctions, Induction Deriving Numerals, Logical Rule