A note on disjunctive form tautologies

Open Access

1 April 1973

journal article
research article
Published by Association for Computing Machinery (ACM) in ACM SIGACT News

Vol. 5 (2) , 17-20
https://doi.org/10.1145/1811123.1811124

Abstract

Cook [1] and Karp [2] have shown that a large class of combinatorial decision problems can be solved in time bounded by a polynomial in the size of the problem iff there is a polynomial time procedure for deciding whether a disjunctive formula with at most three literals per disjunct in the propositional calculus is a tautology.

Keywords

PROBLEM IFF
LARGE CLASS
COMBINATORIAL DECISION PROBLEM
POLYNOMIAL TIME PROCEDURE
DISJUNCTIVE FORM TAUTOLOGY
DISJUNCTIVE FORMULA
PROPOSITIONAL CALCULUS
DECISION PROBLEM
POLYNOMIAL TIME

Funding Information

Office of Naval Research (N00014-70-A-0362-0006)

This publication has 2 references indexed in Scilit:

Reducibility among Combinatorial Problems
Published by Springer Nature ,1972
The complexity of theorem-proving procedures
Published by Association for Computing Machinery (ACM) ,1971