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

03F05 Cut-elimination and normal-form theorems
03F07 Structure of proofs
03F20 Complexity of proofs
Full Text: DOI
[1] 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
[2] Baaz, M.; Hetzl, S.; Leitsch, A.; Richter, C.; Spohr, H., Proof transformation by CERES, () · Zbl 1125.03012
[3] Baaz, M.; Leitsch, A., On skolemization and proof complexity, Fundamenta informaticae, 20, 4, 353-379, (1994) · Zbl 0815.03003
[4] Baaz, M.; Leitsch, A., Cut normal forms and proof complexity, Annals of pure and applied logic, 97, 127-177, (1999) · Zbl 0940.03062
[5] Baaz, M.; Leitsch, A., Cut-elimination and redundancy-elimination by resolution, Journal of symbolic computation, 29, 2, 149-176, (2000) · Zbl 0976.03059
[6] Buss, S.R., On herbrand’s theorem, (), 195-209
[7] 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
[8] G. Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift, 39 (1934-1935) 176-210, 405-431 · Zbl 0010.14501
[9] S. Hetzl, Characteristic clause sets and proof transformations, Ph.D. Thesis, Vienna University of Technology, 2007
[10] S. Hetzl, Proof profiles. Characteristic Clause Sets and Proof Transformations, VDM, 2008
[11] Hetzl, S.; Leitsch, A., Proof transformations and structural invariance, () · Zbl 1123.03050
[12] Hilbert, D.; Bernays, P., Grundlagen der Mathematik II, (1939), Springer · JFM 65.0021.02
[13] Luckhardt, H., Herbrand-analysen zweier beweise des satzes von Roth: polynomiale anzahlschranken, Journal of symbolic logic, 54, 1, 234-263, (1989) · Zbl 0669.03024
[14] Pudlák, P., The lengths of proofs, (), 547-637 · Zbl 0920.03056
[15] 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.