The finite controllability of the Maslov case

1974 ◽  
Vol 39 (3) ◽  
pp. 509-518 ◽  
Author(s):  
Stål Aanderaa ◽  
Warren D. Goldfarb
Keyword(s):  
Atomic Formula ◽  
Finite Model ◽  
Quantification Theory ◽  
Maslov Class

In this paper we show the finite controllability of the Maslov class of formulas of pure quantification theory (specified immediately below). That is, we show that every formula in the class has a finite model if it has a model at all. A signed atomic formula is an atomic formula or the negation of one; a binary disjunction is a disjunction of the form A1 ⋁ A2, where A1 and A2 are signed atomic formulas; and a formula is Krom if it is a conjunction of binary disjunctions. Finally, a prenex formula is Maslov if its prefix is ∃···∃∀···∀∃···∃ and its matrix is Krom.A number of decidability results have been obtained for formulas classified along these lines. It is a consequence of Theorems 1.7 and 2.5 of [4] that the following are reduction classes (for satisfiability): the class of Skolem formulas, that is, prenex formulas with prefixes ∀···∀∃···∃, whose matrices are conjunctions one conjunct of which is a ternary disjunction and the rest of which are binary disjunctions; and the class of Skolem formulas containing identity whose matrices are Krom. Moreover, the following results (for pure quantification theory, that is, without identity) are derived in [1] and [2]: the classes of prenex formulas with Krom matrices and prefixes ∃∀∃∀, or prefixes ∀∃∃∀, or prefixes ∀∃∀∀ are all reduction classes, while formulas with Krom matrices and prefixes ∀∃∀ comprise a decidable class. The latter class, however, is not finitely controllable, for it contains formulas satisfiable only over infinite universes. The Maslov class was shown decidable by Maslov in [11].

scholarly journals Random models and the Maslov class

1989 ◽  
Vol 54 (2) ◽  
pp. 460-466
Author(s):  
Warren Goldfarb
Keyword(s):  
Efficient Method ◽  
Probability Space ◽  
Random Model ◽  
Finite Model ◽  
Quantification Theory ◽  
Finite Models ◽  
Model Method ◽  
Maslov Class ◽  
Random Models ◽  
Novel Method

In [GS] Gurevich and Shelah introduce a novel method for proving that every satisfiable formula in the Gödel class has a finite model (the Gödel class is the class of prenex formulas of pure quantification theory with prefixes ∀∀∃ … ∃). They dub their method “random models”: it proceeds by delineating, given any F in the Gödel class and any integer p, a set of structures for F with universe {1, …, p} that can be treated as a finite probability space S. They then show how to calculate an upper bound on the probability that a structure chosen at random from S makes F false; from this bound they are able to infer that if p is sufficiently large, that probability will be less than one, so that there will exist a structure in S that is a model for F. The Gurevich-Shelah proof is somewhat simpler than those known heretofore. In particular, there is no need for the combinatorial partitionings of finite universes that play a central role in the earlier proofs (see [G] and [DG, p. 86]). To be sure, Gurevich and Shelah obtain a larger bound on the size of the finite models, but this is relatively unimportant, since searching for finite models is not the most efficient method to decide satisfiability.Gurevich and Shelah note that the random model method can be used to treat the Gödel class extended by initial existential quantifiers, that is, the prefix-class ∀…∀∃…∃; but they do not investigate further its range of applicability to syntactically specified classes.

Random models and solvable Skolem classes

1993 ◽  
Vol 58 (3) ◽  
pp. 908-914
Author(s):  
Warren Goldfarb
Keyword(s):  
Normal Form ◽  
Systematic Approach ◽  
Finite Model ◽  
Theoretic Property ◽  
Quantification Theory ◽  
Maslov Class ◽  
Random Models ◽  
Universal Quantifiers ◽  
Necessary And Sufficient ◽  
Made In

A Skolem class is a class of formulas of pure quantification theory in Skolem normal form: closed, prenex formulas with prefixes ∀…∀∃…∃. (Pure quantification theory contains quantifiers, truth-functions, and predicate letters, but neither the identity sign nor function letters.) The Gödel Class, in which the number of universal quantifiers is limited to two, was shown effectively solvable (for satisfiability) sixty years ago [G1]. Various solvable Skolem classes that extend the Gödel Class can be obtained by allowing more universal quantifiers but restricting the combinations of variables that may occur together in atomic subformulas [DG, Chapter 2]. The Gödel Class and these extensions are also finitely controllable, that is, every satisfiable formula in them has a finite model. In this paper we isolate a model-theoretic property that connects the usual solvability proofs for these classes and their finite controllability. For formulas in the solvable Skolem classes, the property is necessary and sufficient for satisfiability. The solvability proofs implicitly relied on this fact. Moreover, for any formula in Skolem normal form, the property implies the existence of a finite model.The proof of the latter implication uses the random models technique introduced in [GS] for the Gödel Class and modified and applied in [Go] to the Maslov Class. The proof thus substantiates the claim made in [Go] that random models can be adapted to the Skolem classes of [DG, Chapter 2]. As a whole, the results of this paper provide a more general, systematic approach to finite controllability than previous methods.

On formulas with valid cases

1956 ◽  
Vol 21 (2) ◽  
pp. 148-148
Author(s):  
W. V. Quine
Keyword(s):  
Atomic Formula ◽  
Quantification Theory ◽  
Truth Value ◽  
The One ◽  
Do So

Commonly, when we succeed in showing a formula of quantification theory to be consistent, we do so by producing a true interpretation. Sometimes we achieve the same effect without even exceeding the resources of quantification theory itself: we show a formula consistent by producing a valid formula from it by substitution. Example: ‘(∃x)Fx ⊃ (x)(∃y) (Gxy ▪ Fy)’ is seen consistent by noting its valid substitution case ‘(∃x)Fx ⊃ (x)(∃y)(Fx ∨ Fy ▪ Fy)’. How generally available is this latter method? I shall show that it is available if and only if the formula whose consistency is shown is satisfiable in a one-member universe.The “only if” part is immediate. For, if ψ is a substitution case of ϕ, then ϕ is satisfiable wherever ψ is; and ψ, if valid, is satisfiable in a one-member universe.Conversely, suppose a true interpretation of ϕ in a one-member universe. Each predicate letter of ϕ is thereby interpreted outright as true or false, in effect, since there is no varying the values of ‘x’, ‘y’, etc. Now form ψ from ϕ by substitution as follows: change each atomic formula ϕi(e.g. ‘Fx’, ‘Fy’, ‘Gxy’) to ⌜ϕi⊃ϕi⌝ if its predicate letter is one that was interpreted as true, or to ⌜ϕi ▪ − ⊃ϕi⌝ if its predicate letter is one that was interpreted as false. Clearly ψ under all interpretations even in large universes, will receive the truth value that ϕ received under the supposed interpretation in the one-member universe. So ψ is valid.

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.

On the Gödel class with identity

1981 ◽  
Vol 46 (2) ◽  
pp. 354-364 ◽  
Author(s):  
Warren D. Goldfarb
Keyword(s):  
Recursive Function ◽  
Decision Problem ◽  
Decision Procedure ◽  
Finite Model ◽  
Quantification Theory ◽  
Free Variables ◽  
Primitive Recursive

The Gödel Class is the class of prenex formulas of pure quantification theory whose prefixes have the form ∀y1∀y2∃x1 … ∃xn. The Gödel Class with Identity, or GCI, is the corresponding class of formulas of quantification theory extended by inclusion of the identity-sign “ = ”. Although the Gödel Class has long been kndwn to be solvable, the decision problem for the Gödel Class with Identity is open. In this paper we prove that there is no primitive recursive decision procedure for the GCI, or, indeed, for the subclass of the GCI containing just those formulas with prefixes ∀y1∀y2∃x.Throughout this paper we take quantification theory to include, aside from logical signs, infinitely many k-place predicate letters for each k > 0, but no function signs or constants. Moreover, by “prenex formula” we include only those without free variables. A decision procedure for a class of formulas is a recursive function that carries a formula in the class to 0 if the formula is satisfiable and to 1 if not. A class is solvable iff there exists a decision procedure for it. A class is finitely controllable iff every satisfiable formula in the class has a finite model. Since we speak only of effectively specified classes, finite controllability implies solvability (but not conversely).The GCI has a curious history. Gödel showed the Gödel Class (without identity) solvable in 1932 [4] and finitely controllable in 1933 [5].

Finite Model Theory

1995 ◽  
Author(s):  
Heinz-Dieter Ebbinghaus ◽  
Jörg Flum
Keyword(s):  
Model Theory ◽  
Finite Model ◽  
Finite Model Theory

scholarly journals A spatio-temporal specification language and its completeness & decidability

2020 ◽  
Vol 9 (1) ◽  
Author(s):  
Tengfei Li ◽  
Jing Liu ◽  
Haiying Sun ◽  
Xiang Chen ◽  
Lipeng Zhang ◽  
...  
Keyword(s):  
Intelligent Transportation System ◽  
Cyber Physical Systems ◽  
Specification Language ◽  
Finite Model ◽  
Critical Systems ◽  
Physical Systems ◽  
Spatial Objects ◽  
Temporal Properties ◽  
Spatio Temporal ◽  
Temporal Specification

AbstractIn the past few years, significant progress has been made on spatio-temporal cyber-physical systems in achieving spatio-temporal properties on several long-standing tasks. With the broader specification of spatio-temporal properties on various applications, the concerns over their spatio-temporal logics have been raised in public, especially after the widely reported safety-critical systems involving self-driving cars, intelligent transportation system, image processing. In this paper, we present a spatio-temporal specification language, STSL PC, by combining Signal Temporal Logic (STL) with a spatial logic S4 u, to characterize spatio-temporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatio-temporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL PC combines the power of temporal modalities and spatial operators, and enjoys important properties such as finite model property. We provide a Hilbert-style axiomatization for the proposed STSL PC and prove the soundness and completeness by the spatio-temporal extension of maximal consistent set and canonical model. Further, we demonstrate the decidability of STSL PC and analyze the complexity of STSL PC. Besides, we generalize STSL to the evolution of spatial objects over time, called STSL OC, and provide the proof of its axiomatization system and decidability.

Modern Quantification Theory

2021 ◽  
Author(s):  
Shizuhiko Nishisato ◽  
Eric J. Beh ◽  
Rosaria Lombardo ◽  
Jose G. Clavel
Keyword(s):  
Quantification Theory

scholarly journals Study on the Attractiveness Factors of Online Courses

2019 ◽  
Vol 9 (2) ◽  
pp. 128 ◽  
Author(s):  
Jia-Xuan Han ◽  
Min-Yuan Ma
Keyword(s):  
Online Teaching ◽  
Online Courses ◽  
Rapid Development ◽  
Grid Method ◽  
Type I ◽  
Digital Learning ◽  
Key Factors ◽  
Quantification Theory ◽  
Global Trend ◽  
Education Industry

With the rapid development of online courses, digital learning has become a global trend. In this context, this study analyzed the high intake population of online courses for online affective cognition, and explored what the user’s attraction factors for online courses are. The key factors that affect consumers’ usage of online courses and the weights of impact relations are presented, aiming to provide guidance for future improvement of online courses. This study was conducted through the evaluation grid method of Miryoku engineering. In order to make the charm factors more accurate and representative, this study summarized the charm elements using the Kawakita Jiro (KJ) method, and then quantified the factors in the form of a questionnaire. Through the statistical analysis of the questionnaire and quantification theory type I, the correlation between the charm feeling and the online course as well as the weight of each item (original evaluation item) and category (specific evaluation item) were calculated. Through the research and discussion on the charm factors of online teaching, the results analyzed and integrated in this paper could give more substantive suggestions and help to the education industry.

Sign in / Sign up

Export Citation Format

Share Document