| Peer-Reviewed

Refutation Of Hard-Determinable Formulas In The System “Resolution Over Linear Equations” And Its Generalization

Received: 11 May 2013     Published: 20 June 2013
Views:       Downloads:
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.

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), 2013. Published by Science Publishing Group

Keywords

Resolution Systems, Resolution over Linear Equations, Refutation, Proof Complexity, Hard-Determinable Formula

References
[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.
Cite This Article
  • 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

    Copy | Download

    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

    Copy | Download

    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

    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}
    }
    

    Copy | Download

  • 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  - 

    Copy | Download

Author Information
  • Department of Informatics and Applied Mathematics, Yerevan State University, Yerevan, Armenia

  • Department of Informatics and Applied Mathematics, Yerevan State University, Yerevan, Armenia

  • Department of Informatics and Applied Mathematics, Yerevan State University, Yerevan, Armenia

  • Sections