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.

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.

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

Note on a problem of L. Henkin

1956 ◽  
Vol 21 (1) ◽  
pp. 33-35 ◽  
Author(s):  
Abraham Robinson
Keyword(s):  
Normal Form ◽  
Predicate Calculus ◽  
Universal Quantifiers ◽  
Image Position ◽  
Necessary And Sufficient

A statement X in the lower predicate calculus is said to be persistent with respect to the set of statements K ([2], [3]), if whenever X holds in a model M of K then X holds also in all extensions of M which are models of K. If X is persistent with respect to the empty set, then it may be said to be absolutely persistent.A statement X is called existential, if it is in prenex normal form and does not contain any universal quantifiers. This includes the possibility that X does not contain any quantifiers at all.Let E be the class of all existential statements. Then it is not difficult to see that E is quasi-disjunctive. That is to say, given statements Y1, Y2 in E, there exists a statement Y in E such thatis provable.L. Henkin [1] has raised the question how to characterise the statements X which are persistent with respect to a given set K (e.g. a set of axioms for a field or a group) by a syntactical condition. He has shown that, in order that a statement X be absolutely persistent, it is necessary and sufficient that there exist a statement Y ϵ E such thatis provable.

Default Logic Models of Certain Inheritance Systems with Exceptions

1993 ◽  
Vol 18 (2-4) ◽  
pp. 129-149
Author(s):  
Serge Garlatti
Keyword(s):  
Hierarchical Structure ◽  
Formal Semantics ◽  
Sufficient Conditions ◽  
Nonmonotonic Reasoning ◽  
Default Logic ◽  
Representation Systems ◽  
The Hierarchical Structure ◽  
Necessary And Sufficient ◽  
Structure Of Knowledge ◽  
Made In

Representation systems based on inheritance networks are founded on the hierarchical structure of knowledge. Such representation is composed of a set of objects and a set of is-a links between nodes. Objects are generally defined by means of a set of properties. An inheritance mechanism enables us to share properties across the hierarchy, called an inheritance graph. It is often difficult, even impossible to define classes by means of a set of necessary and sufficient conditions. For this reason, exceptions must be allowed and they induce nonmonotonic reasoning. Many researchers have used default logic to give them formal semantics and to define sound inferences. In this paper, we propose a survey of the different models of nonmonotonic inheritance systems by means of default logic. A comparison between default theories and inheritance mechanisms is made. In conclusion, the ability of default logic to take some inheritance mechanisms into account is discussed.

scholarly journals A Note on Decomposable and Reducible Integer Matrices

Symmetry ◽  
2021 ◽  
Vol 13 (7) ◽  
pp. 1125
Author(s):  
Carlos Marijuán ◽  
Ignacio Ojeda ◽  
Alberto Vigneron-Tenorio
Keyword(s):  
Normal Form ◽  
Linear Algebra ◽  
Sufficient Conditions ◽  
Necessary And Sufficient Conditions ◽  
Integer Matrix ◽  
Hermite Normal Form ◽  
Necessary And Sufficient

We propose necessary and sufficient conditions for an integer matrix to be decomposable in terms of its Hermite normal form. Specifically, to each integer matrix, we associate a symmetric integer matrix whose reducibility can be efficiently determined by elementary linear algebra techniques, and which completely determines the decomposability of the first one.

Delay stabilization of periodic orbits in coupled oscillator systems

2010 ◽  
Vol 368 (1911) ◽  
pp. 319-341 ◽  
Author(s):  
B. Fiedler ◽  
V. Flunkert ◽  
P. Hövel ◽  
E. Schöll
Keyword(s):  
Normal Form ◽  
Numerical Simulations ◽  
Periodic Orbits ◽  
Coupled Oscillators ◽  
Coupled Oscillator ◽  
Non Invasive ◽  
Coupling Parameters ◽  
Necessary And Sufficient ◽  
Time Delayed Feedback ◽  
Coupled Oscillator Systems

We study diffusively coupled oscillators in Hopf normal form. By introducing a non-invasive delay coupling, we are able to stabilize the inherently unstable anti-phase orbits. For the super- and subcritical cases, we state a condition on the oscillator’s nonlinearity that is necessary and sufficient to find coupling parameters for successful stabilization. We prove these conditions and review previous results on the stabilization of odd-number orbits by time-delayed feedback. Finally, we illustrate the results with numerical simulations.

SOLVING SPATIAL CONSTRAINTS WITH GLOBAL DISTANCE COORDINATE SYSTEM

2006 ◽  
Vol 16 (05n06) ◽  
pp. 533-547 ◽  
Author(s):  
LU YANG
Keyword(s):  
Coordinate System ◽  
Systematic Approach ◽  
Distance Geometry ◽  
Spatial Constraints ◽  
Constraint Equations ◽  
System A ◽  
Short Program ◽  
Complete Set ◽  
Point Line ◽  
Made In

A systematic approach making use of distance geometry to solve spatial constraints is introduced. We demonstrate how to create the constraint equations by means of a relevant distance coordinate system. A short program is made (in Maple) which implements the algorithm producing automatically a complete set of constraint equations for a given point-plane configuration. The point-line-plane configurations are converted into point-plane ones beforehand.

The Place of Reasons in Epistemology

2018 ◽  
Author(s):  
Kurt Sylvan ◽  
Ernest Sosa
Keyword(s):  
Building Block ◽  
Epistemic Normativity ◽  
Epistemic Reasons ◽  
Middle Ground ◽  
Theoretic Property ◽  
Propositional Justification ◽  
Doxastic Justification ◽  
The Road ◽  
Necessary And Sufficient

This chapter defends a middle ground between two extremes in the literature on the place of reasons in epistemology. Against members of the “reasons first” movement, we argue that reasons are not the sole grounds of epistemic normativity. We suggest that the virtue-theoretic property of competence is rather the key building block. To support this approach, we note that reasons must be possessed to ground central epistemic properties, and argue that possession is grounded in competence. But while we here diverge with reasons-firsters, we also distance ourselves from those who deem reasons unimportant. Indeed, we hold that having sufficient epistemic reasons is necessary and sufficient for propositional justification, and that proper basing on them yields doxastic justification. But since possession and proper basing are grounded in competence, reasons are not the end of the road: competence enables them to do their work, putting them—and us—in the middle.

A Compact Imbedding Theorem for Functions without Compact Support

1971 ◽  
Vol 14 (3) ◽  
pp. 305-309 ◽  
Author(s):  
R. A. Adams ◽  
John Fournier
Keyword(s):  
Sobolev Space ◽  
Compact Support ◽  
Unbounded Domains ◽  
Bounded Domains ◽  
Complete Continuity ◽  
Compact Imbedding ◽  
Compactness Theorems ◽  
Image Position ◽  
Necessary And Sufficient ◽  
Made In

The extension of the Rellich-Kondrachov theorem on the complete continuity of Sobolev space imbeddings of the sort1to unbounded domains G has recently been under study [1–5] and this study has yielded [4] a condition on G which is necessary and sufficient for the compactness of (1). Similar compactness theorems for the imbeddings2are well known for bounded domains G with suitably regular boundaries, and the question naturally arises whether any extensions to unbounded domains can be made in this case.

scholarly journals A finite model-theoretical proof of a property of bounded query classes within PH

2004 ◽  
Vol 69 (4) ◽  
pp. 1105-1116 ◽  
Author(s):  
Leszek Aleksander Kołodziejczyk
Keyword(s):  
Normal Form ◽  
Model Theory ◽  
Finite Model ◽  
Sufficient Condition ◽  
Finite Model Theory ◽  
Finite Models ◽  
Constructible Function ◽  
Simple Sufficient Condition

Abstract.We use finite model theory (in particular, the method of FM-truth definitions, introduced in [MM01] and developed in [K04], and a normal form result akin to those of [Ste93] and [G97]) to prove:Let m ≥ 2. Then:(A) If there exists k such that NP⊆ Σm TIME(nk)∩ Πm TIME(nk), then for every r there exists kr such that :(B) If there exists a superpolynomial time-constructible function f such that NTIME(f), then additionally .This strengthens a result by Mocas [M96] that for any r, .In addition, we use FM-truth definitions to give a simple sufficient condition for the arity hierarchy to be strict over finite models.

Sign in / Sign up

Export Citation Format

Share Document