Article citationsMore >>

Johnsonbaugh R., Discrete Mathematics, Fifth Edition, Pearson Education Singapore, 2002.

has been cited by the following article:

Article

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

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


American Journal of Modeling and Optimization. 2014, Vol. 2 No. 1, 34-38
DOI: 10.12691/ajmo-2-1-5
Copyright © 2014 Science and Education Publishing

Cite this paper:
Vishwa Nath Maurya, 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.

Correspondence to: Vishwa  Nath Maurya, Professor & Principal, Shekhawati Engineering College, Rajasthan Technical University, India. Email: prof.drvnmaurya@gmail.com

Abstract

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).

Keywords