Optimizing propositional calculus formulas with regard to questions of deducibility (Q1117918)

In order to get shorter proofs, it is quite natural to add theorems to an axiom system and to deduce from the extended system. In terms of computational logic that is the problem of improving deductions of query clauses C from a set of clauses \({\mathcal C}\) by adding consequent clauses to this set. The authors of this paper investigate the possibility to improve decision complexity of the problem \({\mathcal C}\vdash C\) (\({\mathcal C}\), C being propositional) by adding to \({\mathcal C}^ a \)polynomially bounded set of clauses \({\mathcal D}({\mathcal C})\) s.t. \({\mathcal C}\cup {\mathcal D}({\mathcal C})\vdash C\) becomes a polynomial time decision problem (optimization problem). IF \({\mathcal D}\) could be constructed from \({\mathcal C}\) in polynomial time too, then such an improvement clearly would yield \(P=NP\). On the other hand, the impossibility of such an improvement implies \(P\neq NP\). Thus the authors investigate a restricted optimization problem; they show that by admitting only \(\leq k\)-literal query clauses, addition of all m-literal clauses deducible from \({\mathcal C}\) with \(m<k\) does not change the CoNP-completeness of the deduction problem. Most part of the paper is devoted to the optimization of clause forms under resolution (i.e., how can resolution be improved by adding a polynomial number of deducible clauses to the input clauses, arbitrary query clauses being admitted?). Based on exponentiality of resolution [\textit{A. Urquhart}, J. Assoc. Comput. Mach. 34, 209-219 (1987; Zbl 0639.68093)], the authors show that adding \(O(n/\log^ 2n)\) clauses does not yield a polynomial time decision method; thus \(O(n/\log^ 2n)\) is a lower bound for the optimization problem of resolution. Furthermore it is shown that propositional Horn formulas cannot be optimized w.r.t. SLD- resolution (a consequence is that SLD resolution cannot be done in polynomial time). Finally it is proved that propositional Horn formulas cannot be optimized w.r.t. the PROLOG inference mechanism (the authors give a method to avoid loops), even if multiple occurrences of atoms in a goal are deleted; in this case, an exponential lower bound for the worst- case time complexity is derived.