arXiv subjects
Publications and source records attributed to Grigoriy V. Bokov.
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 quantified boolean formula problem. We describe a simple deterministic algorithm that, for a given quantified boolean formula $F$, stops in time bounded by $O(|F|^4)$ and answers yes if $F$ is true and no otherwise.
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.
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 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.
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.
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.