# zbMATH — the first resource for mathematics

Describing proofs by short tautologies. (English) Zbl 1172.03027
It is well-known that the size of Herbrand disjunction is super-exponential in the size of a proof (with cut or modus ponens). The author provides an elegant construction of a short propositional tautology similar to Herbrand disjunction and completely encoding a given proof. Assuming that a proved formula $$F$$ as well as every cut formula in the proof is prenex, take all quantifier-free instances $$F_1,\ldots,F_k$$ of $$F$$ in the given proof, all quantifier-free instances $$C_1,\ldots,C_l$$ of antecedent cut formulas and all quantifier-free instances $$D_1,\ldots,D_m$$ of succedent cut formulas. The implication $$(\bigvee_{i\leq l}C_i\rightarrow \&_{j\leq m}D_j)\rightarrow F_1\vee\ldots\vee F_k$$ is proved by a quantifier-free derivation which encodes the previous derivation of $$F$$.

##### MSC:
 03F05 Cut-elimination and normal-form theorems 03F07 Structure of proofs 03F20 Complexity of proofs
##### Keywords:
proof theory; Herbrand’s theorem; cut-elimination
CERES
Full Text:
##### References:
  Baaz, M.; Hetzl, S.; Leitsch, A.; Richter, C.; Spohr, H., CERES: an analysis of Fürstenberg’s proof of the infinity of primes, Theoretical computer science, 403, 160-175, (2008) · Zbl 1181.68264  Baaz, M.; Hetzl, S.; Leitsch, A.; Richter, C.; Spohr, H., Proof transformation by CERES, () · Zbl 1125.03012  Baaz, M.; Leitsch, A., On skolemization and proof complexity, Fundamenta informaticae, 20, 4, 353-379, (1994) · Zbl 0815.03003  Baaz, M.; Leitsch, A., Cut normal forms and proof complexity, Annals of pure and applied logic, 97, 127-177, (1999) · Zbl 0940.03062  Baaz, M.; Leitsch, A., Cut-elimination and redundancy-elimination by resolution, Journal of symbolic computation, 29, 2, 149-176, (2000) · Zbl 0976.03059  Buss, S.R., On herbrand’s theorem, (), 195-209  Carbone, A., Interpolants, cut elimination and flow graphs for the propositional calculus, Annals of pure and applied logic, 83, 249-299, (1997) · Zbl 0873.03050  G. Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift, 39 (1934-1935) 176-210, 405-431 · Zbl 0010.14501  S. Hetzl, Characteristic clause sets and proof transformations, Ph.D. Thesis, Vienna University of Technology, 2007  S. Hetzl, Proof profiles. Characteristic Clause Sets and Proof Transformations, VDM, 2008  Hetzl, S.; Leitsch, A., Proof transformations and structural invariance, () · Zbl 1123.03050  Hilbert, D.; Bernays, P., Grundlagen der Mathematik II, (1939), Springer · JFM 65.0021.02  Luckhardt, H., Herbrand-analysen zweier beweise des satzes von Roth: polynomiale anzahlschranken, Journal of symbolic logic, 54, 1, 234-263, (1989) · Zbl 0669.03024  Pudlák, P., The lengths of proofs, (), 547-637 · Zbl 0920.03056  Takeuti, G., Proof theory, (1987), North-Holland Amsterdam
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.