An undecidable two sorted predicate calculus

1969 ◽  
Vol 34 (1) ◽  
pp. 21-23 ◽  
Author(s):  
A. B. Slomson
Keyword(s):  
Decision Procedure ◽  
The Other ◽  
Predicate Calculus ◽  
First Order ◽  
Predicate Language

Let L be a first order predicate language with two sorts of variables and a single dyadic predicate letter whose first place is to be filled by variables of one sort and whose second place is to be filled by variables of the other sort. In answer to a question of M. H. Löb we show that there is no decision procedure for determining whether or not a sentence of L is universally valid.

On simplifying the matrix of a wff

1968 ◽  
Vol 33 (2) ◽  
pp. 180-192 ◽  
Author(s):  
Peter Andrews
Keyword(s):  
Normal Form ◽  
Decision Procedure ◽  
Conjunctive Normal Form ◽  
Predicate Calculus ◽  
First Order ◽  
The Matrix ◽  
Order Predicate Calculus

In [3], [4], and [5] Joyce Friedman formulated and investigated certain rules which constitute a semi-decision procedure for wffs of first order predicate calculus in closed prenex normal form with prefixes of the form ∀x1 … ∀xκ∃y1 … ∃ym∀z1 … ∀zn. Given such a wff QM, where Q is the prefix and M is the matrix in conjunctive normal form, Friedman's rules can be used, in effect, to construct a matrix M* which is obtained from M by deleting certain conjuncts of M.

scholarly journals A decision procedure for a class of formulas of first order predicate calculus

1964 ◽  
Vol 14 (4) ◽  
pp. 1305-1319 ◽  
Author(s):  
Melven Krom
Keyword(s):  
Decision Procedure ◽  
Predicate Calculus ◽  
First Order ◽  
Order Predicate Calculus

scholarly journals An elimination theorem of uniqueness conditions in the intuitionistic predicate calculus

1982 ◽  
Vol 85 ◽  
pp. 223-230 ◽  
Author(s):  
Nobuyoshi Motohashi
Keyword(s):  
Free Variable ◽  
The Other ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Classical Predicate

This paper is a sequel to Motohashi [4]. In [4], a series of theorems named “elimination theorems of uniqueness conditions” was shown to hold in the classical predicate calculus LK. But, these results have the following two defects : one is that they do not hold in the intuitionistic predicate calculus LJ, and the other is that they give no nice axiomatizations of some sets of sentences concerned. In order to explain these facts more explicitly, let us introduce some necessary notations and definitions. Let L be a first order classical predicate calculus LK or a first order intuitionistic predicate calculus LJ. n-ary formulas in L are formulas F(ā) in L with a sequence ā of distinct free variables of length n such that every free variable in F occurs in ā.

Quantification and the empty domain

1954 ◽  
Vol 19 (3) ◽  
pp. 177-179 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Truth Table ◽  
The Other ◽  
Predicate Calculus ◽  
Quantification Theory ◽  
First Order ◽  
Small Domain ◽  
Usual Theory ◽  
Exclusive Or ◽  
Order Predicate Calculus ◽  
Supplementary Test

Quantification theory, or the first-order predicate calculus, is ordinarily so formulated as to provide as theorems all and only those formulas which come out true under all interpretations in all non-empty domains. There are two strong reasons for thus leaving aside the empty domain.(i) Where D is any non-empty domain, any quantificational formula which comes out true under all interpretations in all domains larger than D will come out true also under all interpretations in D. (Cf. [4], p. 92.) Thus, though any small domain has a certain triviality, all but one of them, the empty domain, can be included without cost. To include the empty one, on the other hand, would mean surrendering some formulas which are valid everywhere else and thus generally useful.(ii) An easy supplementary test enables us anyway, when we please, to decide whether a formula holds for the empty domain. We have only to mark the universal quantifications as true and the existential ones as false, and apply truth-table considerations.Incidentally, the existence of that supplementary test shows that there is no difficulty in framing an inclusive quantification theory (i.e., inclusive of the empty domain) if we so desire. A proof in this theory can be made to consist simply of a proof in the exclusive (or usual) theory followed by a check by the method of (ii). We may, however, be curious to see a more direct or autonomous formulation: one which does not consist, like the above, of the exclusive theory plus a rule of expurgation. And, in fact, such formulations have of late been forthcoming: Mostowski [5], Hailperin [3], and, as part of a broader context, Church [2]. I shall not presuppose acquaintance with these papers, except in my final paragraph (and then only with [3]).

scholarly journals Thematic Maps for the Variation of Bearing Capacity of Soil Using SPTs and MATLAB

Geosciences ◽  
2020 ◽  
Vol 10 (9) ◽  
pp. 329
Author(s):  
Mahdi O. Karkush ◽  
Mahmood D. Ahmed ◽  
Ammar Abdul-Hassan Sheikha ◽  
Ayad Al-Rumaithi
Keyword(s):  
Bearing Capacity ◽  
Mean Squared Error ◽  
Ground Level ◽  
The Other ◽  
Thematic Maps ◽  
First Order ◽  
Squared Error ◽  
Order Polynomial ◽  
Interpolation Polynomials ◽  
Penetration Tests

The current study involves placing 135 boreholes drilled to a depth of 10 m below the existing ground level. Three standard penetration tests (SPT) are performed at depths of 1.5, 6, and 9.5 m for each borehole. To produce thematic maps with coordinates and depths for the bearing capacity variation of the soil, a numerical analysis was conducted using MATLAB software. Despite several-order interpolation polynomials being used to estimate the bearing capacity of soil, the first-order polynomial was the best among the other trials due to its simplicity and fast calculations. Additionally, the root mean squared error (RMSE) was almost the same for the all of the tried models. The results of the study can be summarized by the production of thematic maps showing the variation of the bearing capacity of the soil over the whole area of Al-Basrah city correlated with several depths. The bearing capacity of soil obtained from the suggested first-order polynomial matches well with those calculated from the results of SPTs with a deviation of ±30% at a 95% confidence interval.

Resolution systems and their applications I

1980 ◽  
Vol 3 (2) ◽  
pp. 235-268
Author(s):  
Ewa Orłowska
Keyword(s):  
Theorem Proving ◽  
Sufficient Conditions ◽  
Predicate Calculus ◽  
Resolution Method ◽  
First Order ◽  
Deductive Systems ◽  
Resolution System ◽  
Resolution Principle ◽  
Necessary And Sufficient ◽  
Classical Predicate

The central method employed today for theorem-proving is the resolution method introduced by J. A. Robinson in 1965 for the classical predicate calculus. Since then many improvements of the resolution method have been made. On the other hand, treatment of automated theorem-proving techniques for non-classical logics has been started, in connection with applications of these logics in computer science. In this paper a generalization of a notion of the resolution principle is introduced and discussed. A certain class of first order logics is considered and deductive systems of these logics with a resolution principle as an inference rule are investigated. The necessary and sufficient conditions for the so-called resolution completeness of such systems are given. A generalized Herbrand property for a logic is defined and its connections with the resolution-completeness are presented. A class of binary resolution systems is investigated and a kind of a normal form for derivations in such systems is given. On the ground of the methods developed the resolution system for the classical predicate calculus is described and the resolution systems for some non-classical logics are outlined. A method of program synthesis based on the resolution system for the classical predicate calculus is presented. A notion of a resolution-interpretability of a logic L in another logic L ′ is introduced. The method of resolution-interpretability consists in establishing a relation between formulas of the logic L and some sets of formulas of the logic L ′ with the intention of using the resolution system for L ′ to prove theorems of L. It is shown how the method of resolution-interpretability can be used to prove decidability of sets of unsatisfiable formulas of a given logic.

Neural computation of motion in the fly visual system: quadratic nonlinearity of responses induced by picrotoxin in the HS and CH cells

1995 ◽  
Vol 74 (6) ◽  
pp. 2665-2684 ◽  
Author(s):  
Y. Kondoh ◽  
Y. Hasegawa ◽  
J. Okuma ◽  
F. Takahashi
Keyword(s):  
Mean Square Error ◽  
Order Term ◽  
Mirror Image ◽  
Second Order ◽  
The Other ◽  
Linear Component ◽  
Mean Square ◽  
Nonlinear Component ◽  
First Order ◽  
Order Kernel

1. A computational model accounting for motion detection in the fly was examined by comparing responses in motion-sensitive horizontal system (HS) and centrifugal horizontal (CH) cells in the fly's lobula plate with a computer simulation implemented on a motion detector of the correlation type, the Reichardt detector. First-order (linear) and second-order (quadratic nonlinear) Wiener kernels from intracellularly recorded responses to moving patterns were computed by cross correlating with the time-dependent position of the stimulus, and were used to characterize response to motion in those cells. 2. When the fly was stimulated with moving vertical stripes with a spatial wavelength of 5-40 degrees, the HS and CH cells showed basically a biphasic first-order kernel, having an initial depolarization that was followed by hyperpolarization. The linear model matched well with the actual response, with a mean square error of 27% at best, indicating that the linear component comprises a major part of responses in these cells. The second-order nonlinearity was insignificant. When stimulated at a spatial wavelength of 2.5 degrees, the first-order kernel showed a significant decrease in amplitude, and was initially hyperpolarized; the second-order kernel was, on the other hand, well defined, having two hyperpolarizing valleys on the diagonal with two off-diagonal peaks. 3. The blockage of inhibitory interactions in the visual system by application of 10-4 M picrotoxin, however, evoked a nonlinear response that could be decomposed into the sum of the first-order (linear) and second-order (quadratic nonlinear) terms with a mean square error of 30-50%. The first-order term, comprising 10-20% of the picrotoxin-evoked response, is characterized by a differentiating first-order kernel. It thus codes the velocity of motion. The second-order term, comprising 30-40% of the response, is defined by a second-order kernel with two depolarizing peaks on the diagonal and two off-diagonal hyperpolarizing valleys, suggesting that the nonlinear component represents the power of motion. 4. Responses in the Reichardt detector, consisting of two mirror-image subunits with spatiotemporal low-pass filters followed by a multiplication stage, were computer simulated and then analyzed by the Wiener kernel method. The simulated responses were linearly related to the pattern velocity (with a mean square error of 13% for the linear model) and matched well with the observed responses in the HS and CH cells. After the multiplication stage, the linear component comprised 15-25% and the quadratic nonlinear component comprised 60-70% of the simulated response, which was similar to the picrotoxin-induced response in the HS cells. The quadratic nonlinear components were balanced between the right and left sides, and could be eliminated completely by their contralateral counterpart via a subtraction process. On the other hand, the linear component on one side was the mirror image of that on the other side, as expected from the kernel configurations. 5. These results suggest that responses to motion in the HS and CH cells depend on the multiplication process in which both the velocity and power components of motion are computed, and that a putative subtraction process selectively eliminates the nonlinear components but amplifies the linear component. The nonlinear component is directionally insensitive because of its quadratic non-linearity. Therefore the subtraction process allows the subsequent cells integrating motion (such as the HS cells) to tune the direction of motion more sharply.

scholarly journals Ganglioside incorporation and release by the isolated perfused rat liver

1991 ◽  
Vol 274 (2) ◽  
pp. 581-585 ◽  
Author(s):  
S C Kivatinitz ◽  
A Miglio ◽  
R Ghidoni
Keyword(s):  
Rat Liver ◽  
The Other ◽  
Regulatory Role ◽  
Isolated Perfused Rat Liver ◽  
Order Kinetic ◽  
Perfused Rat Liver ◽  
Ganglioside Gm1 ◽  
First Order ◽  
Pseudo First Order

The fate of exogenous ganglioside GM1 labelled in the sphingosine moiety, [Sph-3H]GM1, administered as a pulse, in the isolated perfused rat liver was investigated. When a non-recirculating protocol was employed, the amount of radioactivity in the liver and perfusates was found to be dependent on the presence of BSA in the perfusion liquid and on the time elapsed after the administration of the ganglioside. When BSA was added to the perfusion liquid, less radioactivity was found in the liver and more in the perfusate at each time tested, for up to 1 h. The recovery of radioactivity in the perfusates followed a complex course which can be described by three pseudo-first-order kinetic constants. The constants, in order of decreasing velocity, are interpreted as: (a) the dilution of the labelled GM1 by the constant influx of perfusion liquid; (b) the washing off of GM1 loosely bound to the surface of liver cells; (c) the release of gangliosides from the liver. Process (b) was found to be faster in the presence of BSA, probably owing to the ability of BSA to bind gangliosides. The [Sph-3H]GM1 in the liver underwent metabolism, leading to the appearance of products of anabolic (GD1a, GD1b) and catabolic (GM2, GM3) origin; GD1a appeared before GM2 and GM3 but, at times longer than 10 min, GM2 and GM3 showed more radioactivity than GD1a. At a given time the distribution of the radioactivity in the perfusates was quite different from that of the liver. In fact, after 60 min GD1a was the only metabolite present in any amount, the other being GM3, the quantity of which was small. This indicates that the liver is able to release newly synthesized gangliosides quite specifically. When a recirculating protocol was used, there were more catabolites and less GD1a than with the non-recirculating protocol. A possible regulatory role of ganglioside re-internalization on their own metabolism in the liver is postulated.

Sign in / Sign up

Export Citation Format

Share Document