American Journal of Modeling and Optimization
ISSN (Print): 2333-1143 ISSN (Online): 2333-1267 Website: Editor-in-chief: Dr Anil Kumar Gupta
Open Access
Journal Browser
American Journal of Modeling and Optimization. 2014, 2(1), 34-38
DOI: 10.12691/ajmo-2-1-5
Open AccessArticle

Polynomial Simulation and Refutation of Complex Formulas of Resolution over Linear Equations in Propositional Proof System

Vishwa Nath Maurya1, and Avadhesh Kumar Maurya2

1Professor & Principal, Shekhawati Engineering College, Rajasthan Technical University, India

2Assistant Professor, Department of Electronics & Communication Engineering Lucknow Institute of Technology, U.P. Technical University, Lucknow, India

Pub. Date: March 18, 2014

Cite this paper:
Vishwa Nath Maurya and Avadhesh Kumar Maurya. Polynomial Simulation and Refutation of Complex Formulas of Resolution over Linear Equations in Propositional Proof System. American Journal of Modeling and Optimization. 2014; 2(1):34-38. doi: 10.12691/ajmo-2-1-5


In this paper, we present that the propositional proof system R(lin) (Resolution over Linear Equations) established by Ran Raz and Iddo Tzameret is not a super system, there exists a sequence of tautologies, which require proof complexity exponential in size of tautologies. We show that there are the sequence of unsatisfiable collections of disjuncts of linear equations, which require exponential lower bounds in R(lin) and have polynomially bounded refutations by incorporating renaming inference rule to R(lin) system. Some additional properties of R(lin) have been described that many of the “hard” provable in R outstanding examples of propositional tautologies (contradictions) have polynomially bounded proofs in R(lin).

Resolution over linear equations Resolution systems Refutation Proof complexity Hard-determinable formula Polynomial simulation

Creative CommonsThis work is licensed under a Creative Commons Attribution 4.0 International License. To view a copy of this license, visit


[1]  Aleksanyan S. R., Chubaryan A. A., “The polynomial bounds of proof complexity in Frege systems”, Siberian Mathematical Journal, Vol. 50, No. 2, 2009, pp. 243-249.
[2]  Buss S.R., “Some remarks on lengths of propositional proofs”, Archive for Mathematical Logic, 34, 1995, pp. 377-394.
[3]  Chubaryn An., “Relative efficiency of proof systems in classical propositional logic”, IZV. NAN Armenii, Mathematika, 37, No. 5, 2002, pp. 71-84.
[4]  Chubaryn An., Chubaryn Arm., Nalbandyan H., Sayadyan S., “A hierarchy of resolution systems with restricted substitution rules”, Computer Technology and Application, David Publishing, USA, vol. 3, No. 4, 2012, pp. 330-336.
[5]  Cook S.A., Reckhow A.R., “The relative efficiency of propositional proof systems”, Journal of Symbolic Logic, vol. 44, 1979, pp. 36-50.
[6]  Johnsonbaugh R., Discrete Mathematics, Fifth Edition, Pearson Education Singapore, 2002.
[7]  Krajicek J., “On the weak pigeonhole principle”, Fundamentals of Mathematics, 170, 2001, pp. 123-140.
[8]  Pudlak P. “Lengths of proofs” Handbook of proof theory, North-Holland, 1998, pp. 547-637.
[9]  Raz Ran, Tzameret Iddo, “Resolution over linear equations and multilinear proofs”, Ann. Pure Appl. Logic 155 (3), 2008, pp. 194-224.
[10]  Tseitin G. S. “On the complexity of derivation in the propositional calculus”, (in Russian), Zap. Nauchn. Semin. LOMI, Leningrad: Nauka, Vol. 8, 1968, pp. 234-259.