POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS
DOI:
https://doi.org/10.46991/PYSU:A/2011.45.3.003Keywords:
proof complexity, Split Tree, resolution system, resolution over linear equations, determinative conjunct, quasi-hard determinative formulaAbstract
In this paper the notion of quasi-hard determinative formulas is introduced and the proof complexities of such formulas are investigated. For some class of quasi-hard determinative formulas the same order lower and upper bounds for the length of proofs are obtained in several proof systems, basing on disjunctive normal forms (conjunctive normal forms).
Downloads
Published
2011-10-17
How to Cite
Abajyan, A. (2011). POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS. Proceedings of the YSU A: Physical and Mathematical Sciences, 45(3 (226), 3–8. https://doi.org/10.46991/PYSU:A/2011.45.3.003
Issue
Section
Mathematics
License
Copyright (c) 2022 Proceedings of the YSU
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.