Tractability of cut-free Gentzen type propositional calculus with permutation inference. (English) Zbl 0874.03065
Summary: We present a new propositional calculus that has desirable natures with respect to both automatic reasoning and computational complexity: we introduce an inference rule, called permutation, into a cut-free Gentzen type propositional calculus. It allows us to obtain a system which (1) guarantees the subformula property and (2) has polynomial size proofs for hard combinatorial problems, such as pigeonhole principles. We also discuss the relative efficiency of our system. Frege systems polynomially prove the partial consistency of our system.
Keywords:
automatic reasoning; computational complexity; permutation; cut-free Gentzen type propositional calculus; polynomial size proofs for hard combinatorial problems; pigeonhole principles; consistency; subformula property; relative efficiency; Frege systemsReferences:
| [1] | Ajtai, M., (The complexity of the pigeonhole principle. The complexity of the pigeonhole principle, 29th Annual Symp. On the Foundations of Computer Science (1988)), 346-355 · Zbl 0811.03042 |
| [2] | Benhamou, B.; Sais, L., Tractability through symmetries in propositional calculus, J. Autom. Reasoning, 12, 89-102 (1994) · Zbl 0804.68134 |
| [3] | Buss, S. R., Polynomial size proofs of the pigeonhole principle, J. Symbol. Logic, 52, 916-927 (1987) · Zbl 0636.03053 |
| [4] | S.R. Buss, private communication, 1993.; S.R. Buss, private communication, 1993. |
| [5] | Buss, S. R., Weak Formal Systems and Connections to Computational Complexity (January-May, 1988), Student-written lecture notes for topics course at U.C. Berkley |
| [6] | Buss, S. R., Propositional consistency proofs, Ann. Pure Appl. Logic, 52, 3-29 (1991) · Zbl 0749.03040 |
| [7] | Buss, S. R., Bounded Arithmetic (1986), Bibliopolis: Bibliopolis Napoli · Zbl 0649.03042 |
| [8] | Clote, P., (On polynomial size Frege proofs of certain combinatorial principles. On polynomial size Frege proofs of certain combinatorial principles, Arithmetic, Proof Theory, and Computational Complexity (1993), Clarendon Press: Clarendon Press Oxford), 162-184 · Zbl 0793.03046 |
| [9] | Cook, S. A.; Reckhow, R. A., The relative efficiency of propositional proof systems, J. Symbol. Logic, 44, 36-50 (1979) · Zbl 0408.03044 |
| [10] | Cook, S. A., (Feasibly constructive proofs and the propositional calculus. Feasibly constructive proofs and the propositional calculus, Proc. 7th A.C.M. Symp. on the Theory of Computation (1975)), 83-97 · Zbl 0357.68061 |
| [11] | Gallier, J., Logic for Computer Science (1987), Wiley: Wiley New York |
| [12] | Haken, A., The intractability of resolution, Theoret. Comput. Sci., 39, 297-308 (1985) · Zbl 0586.03010 |
| [13] | Tseitin, G. S., (On the complexity of derivation in propositional calculus. On the complexity of derivation in propositional calculus, Studies in Mathematics and Mathematical Logic Part 2 (1968), V.A. Steklov Math. Institute) · Zbl 0197.00102 |
| [14] | Urquhart, A., The complexity of Gentzen systems for propositional logic, Theoret. Comput. Sci., 66, 87-97 (1989) · Zbl 0688.03039 |
| [15] | Urquhart, A., Hard examples for resolution, J. Assoc. Comput. Mach., 34, 209-219 (1987) · Zbl 0639.68093 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
