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.
| Published in | Pure and Applied Mathematics Journal (Volume 2, Issue 3) |
| DOI | 10.11648/j.pamj.20130203.13 |
| Page(s) | 128-133 |
| Creative Commons |
This is an Open Access article, distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution and reproduction in any medium or format, provided the original work is properly cited. |
| Copyright |
Copyright © The Author(s), 2024. Published by Science Publishing Group |
Resolution Systems, Resolution over Linear Equations, Refutation, Proof Complexity, Hard-Determinable Formula
| [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. |
APA Style
Anahit Chubaryan, Armine Chubaryan, Arman Tshitoyan. (2013). Refutation Of Hard-Determinable Formulas In The System “Resolution Over Linear Equations” And Its Generalization. Pure and Applied Mathematics Journal, 2(3), 128-133. https://doi.org/10.11648/j.pamj.20130203.13
ACS Style
Anahit Chubaryan; Armine Chubaryan; Arman Tshitoyan. Refutation Of Hard-Determinable Formulas In The System “Resolution Over Linear Equations” And Its Generalization. Pure Appl. Math. J. 2013, 2(3), 128-133. doi: 10.11648/j.pamj.20130203.13
AMA Style
Anahit Chubaryan, Armine Chubaryan, Arman Tshitoyan. Refutation Of Hard-Determinable Formulas In The System “Resolution Over Linear Equations” And Its Generalization. Pure Appl Math J. 2013;2(3):128-133. doi: 10.11648/j.pamj.20130203.13
Share This Article
Twitter
Linked In
Facebook
Copy
Download@article{10.11648/j.pamj.20130203.13,
author = {Anahit Chubaryan and Armine Chubaryan and Arman Tshitoyan},
title = {Refutation Of Hard-Determinable Formulas In The System “Resolution Over Linear Equations” And Its Generalization},
journal = {Pure and Applied Mathematics Journal},
volume = {2},
number = {3},
pages = {128-133},
doi = {10.11648/j.pamj.20130203.13},
url = {https://doi.org/10.11648/j.pamj.20130203.13},
eprint = {https://article.sciencepublishinggroup.com/pdf/10.11648.j.pamj.20130203.13},
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.},
year = {2013}
}
TY - JOUR T1 - Refutation Of Hard-Determinable Formulas In The System “Resolution Over Linear Equations” And Its Generalization AU - Anahit Chubaryan AU - Armine Chubaryan AU - Arman Tshitoyan Y1 - 2013/06/20 PY - 2013 N1 - https://doi.org/10.11648/j.pamj.20130203.13 DO - 10.11648/j.pamj.20130203.13 T2 - Pure and Applied Mathematics Journal JF - Pure and Applied Mathematics Journal JO - Pure and Applied Mathematics Journal SP - 128 EP - 133 PB - Science Publishing Group SN - 2326-9812 UR - https://doi.org/10.11648/j.pamj.20130203.13 AB - 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. VL - 2 IS - 3 ER -
Information
Email: