Site logo

POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS

This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

CC BY-NC 4.0 This work is licensed under Creative Commons Attribution–NonCommercial International License (CC BY-NC 4.0).

Abstract

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

Subscribe to TheGufo Newsletter​