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

Vishwa Nath Maurya^1, and Avadhesh Kumar Maurya²

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

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

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

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:
Resolution over linear equations Resolution systems Refutation Proof complexity Hard-determinable formula Polynomial simulation

This work is licensed under a Creative Commons Attribution 4.0 International License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

References:

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