Conservative reduction classes of Krom formulas
Journal of Symbolic Logic 47 (1):110-130 (1982)
| 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 | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,664 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesNick Bezhanishvili (2008). Frame Based Formulas for Intermediate Logics. Studia Logica 90 (2):139 - 159.
Klaus Denecke & Dara Phusanga (2008). Hyperformulas and Solid Algebraic Systems. Studia Logica 90 (2):263 - 286.
Ursula Gropp (1988). Coinductive Formulas and a Many-Sorted Interpolation Theorem. Journal of Symbolic Logic 53 (3):937-960.
Johan van Benthem (2005). Guards, Bounds, and Generalized Semantics. Journal of Logic, Language and Information 14 (3).
M. Marshall (2006). Local-Global Properties of Positive Primitive Formulas in the Theory of Spaces of Orderings. Journal of Symbolic Logic 71 (4):1097 - 1107.
Harry R. Lewis (1976). Krom Formulas with One Dyadic Predicate Letter. Journal of Symbolic Logic 41 (2):341-362.
G. Gutiérrez, I. P. de Guzmán, J. Martínez, M. Ojeda-Aciego & A. Valverde (2002). Satisfiability Testing for Boolean Formulas Using Δ-Trees. Studia Logica 72 (1):85 - 112.
M. R. Krom (1970). The Decision Problem for Formulas in Prenex Conjunctive Normal Form with Binary Disjunctions. Journal of Symbolic Logic 35 (2):210-216.
Charles E. Hughes (1976). A Reduction Class Containing Formulas with One Monadic Predicate and One Binary Function Symbol. Journal of Symbolic Logic 41 (1):45-49.
Stål O. Aanderaa & Harry R. Lewis (1973). Prefix Classes of Krom Formulas. Journal of Symbolic Logic 38 (4):628-642.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads6 ( #145,458 of 549,005 )Recent downloads (6 months)1 ( #63,327 of 549,005 )How can I increase my downloads? |
My notes
Discussion
