Abstract

We study some structural and numerical properties of varieties for determinative disjunctive normal forms, introduced here for given propositional formula. We consider for classical and non-classical propositional logics some proof systems, which are constructed on the base of determinative disjunctive normal forms. We investigate also the relation between the proof complexities in some well-known classical and non-classical proof systems (Resolution, Cut-free sequent, Gentzen refutation, Cutting planes etc.) and numerical properties of varieties for determinative disjunctive normal forms for classical and non-classical tautologies.

This work is licensed under a Creative Commons Attribution 4.0 License.