Volume 2, Issue 3, June 2013, Page: 128-133
Refutation Of Hard-Determinable Formulas In The System “Resolution Over Linear Equations” And Its Generalization
Anahit Chubaryan, Department of Informatics and Applied Mathematics, Yerevan State University, Yerevan, Armenia
Armine Chubaryan, Department of Informatics and Applied Mathematics, Yerevan State University, Yerevan, Armenia
Arman Tshitoyan, Department of Informatics and Applied Mathematics, Yerevan State University, Yerevan, Armenia
Received: May 11, 2013;       Published: Jun. 20, 2013
DOI: 10.11648/j.pamj.20130203.13      View  2643      Downloads  78
Abstract
We research the power of the propositional proof system R(lin) (Resolution over Linear Equations) described by Ran Raz and Iddo Tzameret. R (lin) is the generalization of R (Resolution System) and it is known that many tautologies, which require the exponential lower bounds of proof complexities in R, have polynomially bounded proofs in R (lin). We show that there are the sequences of unsatisfiable collections of disjuncts of linear equations, which require exponential lower bounds in R (lin). After adding the renaming rule, mentioned collections have polynomially bounded refutations.
Keywords
Resolution Systems, Resolution over Linear Equations, Refutation, Proof Complexity, Hard-Determinable Formula
To cite this article
Anahit Chubaryan, Armine Chubaryan, Arman Tshitoyan, Refutation Of Hard-Determinable Formulas In The System “Resolution Over Linear Equations” And Its Generalization, Pure and Applied Mathematics Journal. Vol. 2, No. 3, 2013, pp. 128-133. doi: 10.11648/j.pamj.20130203.13
Reference
[1]
S. R. Aleksanyan, A. A. Chubaryan "The polynomial bounds of proof complexity in Frege systems", Siberian Mathematical Journal, vol. 50, № 2, pp. 243-249, 2009.
[2]
S.R.Buss, "Some remarks on lenghts of propositional proofs", Archive for Mathematical Logic, 34, 377-394, 916-927. 1995.
[3]
An. Chubaryn, «Relative efficiency of proof systems in classical propositional logic, Izv. NAN Armenii, Mathematika, 37,N5, pp 71-84, 2002.
[4]
An.Chubaryan, Arm.Chubaryan, H.Nalbandyan, S.Sayadyan, "A Hierarchy of Resolution Systems with Restricted Substitution Rules", Computer Technology and Application, David Publishing, USA, vol. 3, № 4, pp. 330-336, 2012.
[5]
S.A.Cook, A.R.Reckhow, "The relative efficiency of propositional proof systems", Journal of Symbolic Logic, vol. 44, pp. 36-50, 1979.
[6]
J.Krajicek, "On the weak pigeonhole principle", Fund. Math. 170, 123-140, 2001.
[7]
P. Pudlak "Lengths of proofs" Handbook of proof theory, North-Holland, pp. 547-637, 1998.
[8]
Ran Raz, Iddo Tzameret, "Resolution over linear equations and multilinear proofs", Ann. Pure Appl. Logic 155(3), pp. 194-224, 2008.
[9]
G. S. Tseitin "On the complexity of derivation in the propositional calculus", (in Russian), Zap. Nauchn. Semin. LOMI. Leningrad: Nauka, vol. 8, pp. 234-259, 1968.
Browse journals by subject