Showing 1–6 of 6 results for author: Bokov, G V

Complexity of the CNF-satisfiability problem

Authors: Grigoriy V. Bokov

Abstract: This paper is devoted to the complexity of the Boolean satisfiability problem. We consider a version of this problem, where the Boolean formula is specified in the conjunctive normal form. We prove an unexpected result that the CNF-satisfiability problem can be solved by a deterministic Turing machine in polynomial time. This paper is devoted to the complexity of the Boolean satisfiability problem. We consider a version of this problem, where the Boolean formula is specified in the conjunctive normal form. We prove an unexpected result that the CNF-satisfiability problem can be solved by a deterministic Turing machine in polynomial time. △ Less

Submitted 20 July, 2018; v1 submitted 6 April, 2018; originally announced April 2018.

Comments: 4 pages, submitted to the journal Computational complexity

The complexity of propositional proofs

Authors: Grigoriy V. Bokov

Abstract: In this paper, we consider the complexity of propositional proofs of classical and intuitionistic tautologies. In fact, we describe a nondeterministic polynomial-time decision procedure for intuitionistic implicational tautologies. For this purpose, we reduce a decision problem for intuitionistic implicational tautologies to a decision problem for deductive proof diagrams which are a short form fo… ▽ More In this paper, we consider the complexity of propositional proofs of classical and intuitionistic tautologies. In fact, we describe a nondeterministic polynomial-time decision procedure for intuitionistic implicational tautologies. For this purpose, we reduce a decision problem for intuitionistic implicational tautologies to a decision problem for deductive proof diagrams which are a short form for representing of proofs in the intuitionistic implicational calculus. Next, we transform deductive proof diagrams to a special form in which any proof has the size bounded by a polynomial in the length of input formula. Also, we show that this procedure can be extended to all classical and intuitionistic tautologies, and deduce some corollaries including results about complexity classes and polynomially bounded proof systems. △ Less

Submitted 18 January, 2017; v1 submitted 14 September, 2016; originally announced September 2016.

Comments: This paper has been withdrawn by the author due to a crucial sign error in Lemma 4.7

Undecidable iterative propositional calculus

Authors: Grigoriy V. Bokov

Abstract: In this paper, we consider iterative propositional calculi, which are finite sets of propositional formulas together with the rules of modus ponens and weak substitution (when formula being substituted must be already inferred). We construct an undecidable iterative propositional calculus using axioms in 3 variables. Particulary, we show that the general problem of derivability for these calculi i… ▽ More In this paper, we consider iterative propositional calculi, which are finite sets of propositional formulas together with the rules of modus ponens and weak substitution (when formula being substituted must be already inferred). We construct an undecidable iterative propositional calculus using axioms in 3 variables. Particulary, we show that the general problem of derivability for these calculi is undecidable. △ Less

Submitted 22 April, 2015; originally announced April 2015.

Comments: 10 pages, in Russian

On the number of variables in undecidable superintuitionistic propositional calculi

Authors: Grigoriy V. Bokov

Abstract: In this paper, we construct an undecidable 3-variable superintuitionistic propositional calculus, i.e., a finitely axiomatizable extension of the intuitionistic propositional calculus with axioms containing only 3 variables. Since there are no 2-variable superintuitionistic propositional calculi, this is the minimal possible number of variables. In this paper, we construct an undecidable 3-variable superintuitionistic propositional calculus, i.e., a finitely axiomatizable extension of the intuitionistic propositional calculus with axioms containing only 3 variables. Since there are no 2-variable superintuitionistic propositional calculi, this is the minimal possible number of variables. △ Less

Submitted 6 November, 2015; v1 submitted 13 April, 2015; originally announced April 2015.

Comments: 18 pages, 1 figure

Undecidable problems for propositional calculi with implication

Authors: Grigoriy V. Bokov

Abstract: In this article, we deal with propositional calculi over a signature containing the classical implication $\to$ with the rules of modus ponens and substitution. For these calculi we consider few recognizing problems such as recognizing derivations, extensions, completeness, and axiomatizations. The main result of this paper is to prove that the problem of recognizing extensions is undecidable for… ▽ More In this article, we deal with propositional calculi over a signature containing the classical implication $\to$ with the rules of modus ponens and substitution. For these calculi we consider few recognizing problems such as recognizing derivations, extensions, completeness, and axiomatizations. The main result of this paper is to prove that the problem of recognizing extensions is undecidable for every propositional calculus, and the problems of recognizing axiomatizations and completeness are undecidable for propositional calculi containing the formula $x \to ( y \to x )$. As a corollary, the problem of derivability of a fixed formula $A$ is also undecidable for all $A$. Moreover, we give a historical survey of related results. △ Less

Submitted 3 February, 2015; originally announced February 2015.

Comments: 18 pages. arXiv admin note: text overlap with arXiv:1407.7010

Undecidability of the problem of recognizing axiomatizations for implicative propositional calculi

Authors: Grigoriy V. Bokov

Abstract: In this paper we consider propositional calculi, which are finitely axiomatizable extensions of intuitionistic implicational propositional calculus together with the rules of modus ponens and substitution. We give a proof of undecidability of the following problem for these calculi: whether a given finite set of propositional formulas constitutes an adequate axiom system for a fixed propositional… ▽ More In this paper we consider propositional calculi, which are finitely axiomatizable extensions of intuitionistic implicational propositional calculus together with the rules of modus ponens and substitution. We give a proof of undecidability of the following problem for these calculi: whether a given finite set of propositional formulas constitutes an adequate axiom system for a fixed propositional calculus. Moreover, we prove the same for the following restriction of this problem: whether a given finite set of theorems of a fixed propositional calculus derives all theorems of this calculus. The proof of these results is based on a reduction of the undecidable halting problem for the tag systems introduced by Post. △ Less

Submitted 25 July, 2014; originally announced July 2014.

Comments: 13 pages

Journal ref: Logic Journal of the IGPL (2015) 23 (2): 341-353