Article contents
Conservative reduction classes of Krom formulas1
Published online by Cambridge University Press: 12 March 2014
Abstract
A Krom formula of pure quantification theory is a formula in conjunctive normal form such that each conjunct is a disjunction of at most two atomic formulas or negations of atomic formulas. Every class of Krom formulas that is determined by the form of their quantifier prefixes and which is known to have an unsolvable decision problem for satisfiability is here shown to be a conservative reduction class. Therefore both the general satisfiability problem, and the problem of satisfiability in finite models, can be effectively reduced from arbitrary formulas to Krom formulas of these several prefix types.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1982
Footnotes
The authors thank the “Stiftung Volkswagenwerk” for its financial support of the conference on logic and complexity theory held in Aachen in September 1979, during which this collaborative work was initiated, and also the Institut für Mathematische Logik und Grundlagenforschung of the University of Münster for its hospitality during the week after the conference. We are also grateful to Warren Goldfarb for his corrections to an earlier draft of this paper.
References
REFERENCES
- 2
- Cited by