Geodesic
Proof compressions with circuit-structured substitutions
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XI, Tome 358 (2008), pp. 77-99 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between cutfree (or normal) proofs and the corresponding (non-normal) proofs with cuts (or modus ponens). The task of automatic theorem proving is, on the other hand, usually based on the construction of cutfree or only atomic-cuts proofs, since this procedure produces less alternative choices. There are familiar tautologies whose cutfree proofs are huge while the non-cutfree being small. The aim of this paper is to discuss basic methods of weight and/or size reduction of deductions by switching from traditional tree-structured deductions to circuit-structured deductions. A desired efficiency is achieved by adding standard weakening rule of inference upgraded by adding suitable (propositional) unifications modulo variable substitutions. We show examples where such unification provides strong (in fact exponential) compression of cutfree deductions. Bibl. – 10 titles. 
@article{ZNSL_2008_358_a4,
     author = {L. Gordeev and E. H. Haeusler and V. G. da Costa},
     title = {Proof compressions with circuit-structured substitutions},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {77--99},
     year = {2008},
     volume = {358},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2008_358_a4/}
}
TY  - JOUR
AU  - L. Gordeev
AU  - E. H. Haeusler
AU  - V. G. da Costa
TI  - Proof compressions with circuit-structured substitutions
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2008
SP  - 77
EP  - 99
VL  - 358
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2008_358_a4/
LA  - en
ID  - ZNSL_2008_358_a4
ER  - 
%0 Journal Article
%A L. Gordeev
%A E. H. Haeusler
%A V. G. da Costa
%T Proof compressions with circuit-structured substitutions
%J Zapiski Nauchnykh Seminarov POMI
%D 2008
%P 77-99
%V 358
%U http://geodesic.mathdoc.fr/item/ZNSL_2008_358_a4/
%G en
%F ZNSL_2008_358_a4
L. Gordeev; E. H. Haeusler; V. G. da Costa. Proof compressions with circuit-structured substitutions. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XI, Tome 358 (2008), pp. 77-99. http://geodesic.mathdoc.fr/item/ZNSL_2008_358_a4/

[1] P. Beame, T. Pitassi, Propositional proof complexity: Past, present and future, Technical Report TR98-067, Electronic Colloquium on Computational Complexity, 1998 | MR

[2] S. R. Buss, “Polynomial size proofs of the propositional pigeonhole principle”, J. of Symbolic Logic, 52:4 (1987), 916–927 | DOI | MR | Zbl

[3] V. G. da Costa, Compactação de provas lógicas, PhD Thesis, Pontifícia Universidade Católica do Rio de Janeiro, 2007

[4] W. Felscher, Lectures on Mathematical Logic. II: Calculi for Derivations and Deductions, Gordon and Breach Sci. Publ., Amsterdam, 2000

[5] M. Finger, “DAG Sequent Proofs with a Substitution Rule”, We will show Them – Essays in honour of Dov Gabbay's 60th birthday, Vol. 1, Kings College Publications, London, 2005, 671–686

[6] M. Finger, D. Gabbay, Cut and pay, Manuscript, 2005 | MR

[7] L. Gordeev, “On cut elimination in the presence of Peirce rule”, Arch. Math. Logic, 26 (1987), 147–164 | DOI | MR | Zbl

[8] A. Haken, “The intractability of resolution”, Theoretical Computer Science, 39 (1985), 297–308 | DOI | MR | Zbl

[9] Zap. Nauchn. Semin. LOMI, 49, 1975, 67–122 | DOI | Zbl | Zbl

[10] G. S. Tseitin, “On the complexity of derivation in the propositional calculus”, Studies in Constructive Mathematics and Mathematical Logic, II, ed. A. O. Slisenko, 1968, 115–125 | Zbl