Reduction to first degree in quantificational S5

1979 ◽  
Vol 44 (2) ◽  
pp. 207-214
Author(s):  
Michael J. Carroll
Keyword(s):  
Reduction Class

AbstractIt is shown that the modally first-degree formulas of quantificational S5 constitute a reduction class.

Krom formulas with one dyadic predicate letter

1976 ◽  
Vol 41 (2) ◽  
pp. 341-362 ◽  
Author(s):  
Harry R. Lewis
Keyword(s):  
Normal Forms ◽  
Decision Problems ◽  
The Matrix ◽  
Reduction Class ◽  
Complex Construction ◽  
Full Class

Let Kr be the class of all those quantificational formulas whose matrices are conjunctions of binary disjunctions of signed atomic formulas. Decision problems for subclasses of Kr do not invariably coincide with those for the corresponding classes of quantificational formulas with unrestricted matrices; for example, the ∀∃∀ prefix subclass of Kr is solvable, but the full ∀∃∀ class is not ([AaLe],- [KMW]). Moreover, the straightforward encodings of automata which have been used to show the unsolvability of various subclasses of Kr ([Aa], [Bö], [AaLe]) yield but little information about signature subclasses, i.e. subclasses determined by the number and degrees of the predicate letters occurring in a formula. By a new and highly complex construction Theorem 1 establishes the best possible result on classification by signature.Theorem 1. Let C be the class of all formulas in Kr with a single predicate letter, which is dyadic; then C is a reduction class for satisfiability.Thus a signature subclass of Kr is solvable just in case the corresponding class of unrestricted quantificational formulas is solvable, to wit, just in case no predicate letter of degree exceeding one may occur. To obtain a richer classification by signature we consider further restrictions on the matrix. Let Or be the class of formulas in Kr having disjunctive normal forms with only two disjuncts. Theorem 2 sharpens Orevkov's proof of the unsolvability of Or ([Or]; see also [LeGo]).Theorem 2. Let D be the class of formulas in Or with just two predicate letters, both pentadic; then D is a reduction class for satisfiability.

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

Skolem reduction classes

1975 ◽  
Vol 40 (1) ◽  
pp. 62-68 ◽  
Author(s):  
Warren D. Goldfarb ◽  
Harry R. Lewis
Keyword(s):  
Decision Problem ◽  
Atomic Formula ◽  
Complex Situation ◽  
Quantification Theory ◽  
Reduction Class

Among the earliest and best-known theorems on the decision problem is Skolem's result [7] that the class of all closed formulas with prefixes of the form ∀···∀∃···∃ is a reduction class for satisfiability for the whole of quantification theory. This result can be refined in various ways. If the Skolem prefix alone is considered, the best result [8] is that the ∀∀∀∃ class is a reduction class, for Gödel [3], Kalmár [4], and Schütte [6] showed the ∀∀∃···∃ class to be solvable. The purpose of this paper is to describe the more complex situation that arises when (Skolem) formulas are restricted with respect to the arguments of their atomic subformulas. Before stating our theorem, we must introduce some notation.Let x, y1, y2, be distinct variables (we shall use v1, v2, ··· and w1, w2, ··· as metavariables ranging over these variables), and for each i ≥ 1 let Y(i) be the set {y1, ···, yi}. An atomic formula Pv1 ··· vk will be said to be {v1, ···, vk}-based. For any n ≥ 1, p ≥ 1, and any subsets Y1, ··· Yp of Y(n), let C(n, Y1, ···, Yp) be the class of all those closed formulas with prefix ∀y1 ··· ∀yn∃x such that each atomic subformula not containing the variable x is Yi-based for some i, 1 ≤ i ≤ p.

The ??? reduction class

Cybernetics ◽  
1967 ◽  
Vol 2 (1) ◽  
pp. 15-19 ◽  
Author(s):  
V. F. Kostyrko
Keyword(s):  
Reduction Class

Conservative reduction classes of Krom formulas

1982 ◽  
Vol 47 (1) ◽  
pp. 110-130 ◽  
Author(s):  
Stål O. Aanderaa ◽  
Egon Börger ◽  
Harry R. Lewis
Keyword(s):  
Normal Form ◽  
Decision Problem ◽  
Conjunctive Normal Form ◽  
Satisfiability Problem ◽  
Quantification Theory ◽  
Finite Models ◽  
Reduction Class

AbstractA 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.

Breast Reduction Class

2011 ◽  
Vol 128 ◽  
pp. 42
Author(s):  
Kelly Lynne Killeen ◽  
Patricia Sandholm ◽  
Stiles Jewett ◽  
Daniel Ladizinsky
Keyword(s):  
Breast Reduction ◽  
Reduction Class

On the solvability of a subclass of the surányi reduction class

1963 ◽  
Vol 28 (3) ◽  
pp. 237-244
Author(s):  
Richard Goldberg
Keyword(s):  
Present Note ◽  
Direct Proof ◽  
Finite Domain ◽  
Reduction Class

In [1] Dreben showed that the subclass K′ (described below) of the Suranyi reduction class is recursively solvable by showing that the subclass is finitely controllable; that is, by showing that any member S of K′ is satisfiable only if it is finitely satisfiable. Dreben's argument is very complex, but much of the complexity is due to his proving not merely solvability, but the deeper property of finite controllability. In the present note, by exploiting certain features of Dreben's technique, a simpler, direct proof of the solvability of K′ is obtained — that is, a proof in which the question of satisfiability in a finite domain plays no role.

The decision problem for formulas in prenex conjunctive normal form with binary disjunctions

1970 ◽  
Vol 35 (2) ◽  
pp. 210-216 ◽  
Author(s):  
M. R. Krom
Keyword(s):  
Normal Form ◽  
Positive Solution ◽  
Decision Problem ◽  
Conjunctive Normal Form ◽  
Decision Problems ◽  
First Order ◽  
Reduction Class ◽  
Image Position ◽  
Positive Integers ◽  
Order Predicate Calculus

In [8] S. J. Maslov gives a positive solution to the decision problem for satisfiability of formulas of the formin any first-order predicate calculus without identity where h, k, m, n are positive integers, αi, βi are signed atomic formulas (atomic formulas or negations of atomic formulas), and ∧, ∨ are conjunction and disjunction symbols, respectively (cf. [6] for a related solvable class). In this paper we show that the decision problem is unsolvable for formulas that are like those considered by Maslov except that they have prefixes of the form ∀x∃y1 … ∃yk∀z. This settles the decision problems for all prefix classes of formulas for formulas that are in prenex conjunctive normal form in which all disjunctions are binary (have just two terms). In our concluding section we report results on decision problems for related classes of formulas including classes of formulas in languages with identity and we describe some special properties of formulas in which all disjunctions are binary including a property that implies that any proof of our result, that a class of formulas is a reduction class for satisfiability, is necessarily indirect. Our proof is based on an unsolvable combinatorial tag problem.

Sign in / Sign up

Export Citation Format

Share Document