scholarly journals Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo

2011 ◽  
Vol 7 (1) ◽  
Author(s):  
Guillaume Burel
2014 ◽  
Vol 21 (3) ◽  
pp. 401-404
Author(s):  
Dalal A. Maturi ◽  
Antonio J.M. Ferreira ◽  
Ashraf M. Zenkour ◽  
Daoud S. Mashat

AbstractIn this paper, we combine a new higher-order layerwise formulation and collocation with radial basis functions for predicting the static deformations and free vibration behavior of three-layer composite plates. The skins are modeled via a first-order theory, while the core is modeled by a cubic expansion with the thickness coordinate. Through numerical experiments, the numerical accuracy of this strong-form technique for static and vibration problems is discussed.


1984 ◽  
Vol 51 (4) ◽  
pp. 745-752 ◽  
Author(s):  
J. N. Reddy

A higher-order shear deformation theory of laminated composite plates is developed. The theory contains the same dependent unknowns as in the first-order shear deformation theory of Whitney and Pagano [6], but accounts for parabolic distribution of the transverse shear strains through the thickness of the plate. Exact closed-form solutions of symmetric cross-ply laminates are obtained and the results are compared with three-dimensional elasticity solutions and first-order shear deformation theory solutions. The present theory predicts the deflections and stresses more accurately when compared to the first-order theory.


2001 ◽  
Vol 11 (1) ◽  
pp. 21-45 ◽  
Author(s):  
GILLES DOWEK ◽  
THERESE HARDIN ◽  
CLAUDE KIRCHNER

We give a first-order presentation of higher-order logic based on explicit substitutions. This presentation is intentionally equivalent to the usual presentation of higher-order logic based on λ-calculus, that is, a proposition can be proved without the extensionality axioms in one theory if and only if it can be in the other. We show that the Extended Narrowing and Resolution first-order proof-search method can be applied to this theory. In this way we get a step-by-step simulation of higher-order resolution. Hence, expressing higher-order logic as a first-order theory and applying a first-order proof search method is a relevant alternative to a direct implementation. In particular, the well-studied improvements of proof search for first-order logic could be reused at no cost for higher-order automated deduction. Moreover, as we stay in a first-order setting, extensions, such as equational higher-order resolution, may be easier to handle.


1988 ◽  
Vol 40 (3) ◽  
pp. 545-552 ◽  
Author(s):  
B. Ghosh ◽  
K. P. Das

Using reductive perturbation theory and a planar waveguide geometry, the effects of higher-order nonlinearity and finite boundaries on the propagation of electron plasma and ion-acoustic KdV solitons are investigated by taking into account finite electron and ion temperatures. For an electron plasma wave, the higher-order nonlinearity is found to increase the amplitude of the soliton and slightly decrease the width of the soliton compared with that predicted by the first-order theory. For an ion-acoustic wave the higher-order-nonlinearity and finite-boundary effects give rise to a W-shaped soliton.


1966 ◽  
Vol 31 (2) ◽  
pp. 169-181 ◽  
Author(s):  
Calvin C. Elgot ◽  
Michael O. Rabin

We study certain first and second order theories which are semantically defined as the sets of all sentences true in certain given structures. Let be a structure where A is a non-empty set, λ is an ordinal, and Pα is an n(α)-ary relation or function4 on A. With we associate a language L appropriate for which may be a first or higher order calculus. L has an n(α)-place predicate or function constant P for each α < λ. We shall study three types of languages: (1) first-order calculi with equality; (2) second-order monadic calculi which contain monadic predicate (set) variables ranging over subsets of A; (3) restricted (weak) second-order calculi which contain monadic predicate variables ranging over finite subsets of A.


2021 ◽  
Author(s):  
◽  
Wilfred Gordon Malcolm

<p>The programme of work for this thesis began with the somewhat genenal intention of parallelling in the context of higher order models the ultraproduct construction and its consequences as developed in the literature for first order models. Something of this was, of course, already available in the ultrapower construction of W.A.J. Luxemburg used in Non Standand Analysis. It may have been considered that such a genenal intention was not likely to yield anything of significance oven and above what was already available from viewing the higher order situation as a 'many sorted' first order one and interpreting the first order theory accordingly. In the event, however, I believe this has proved not to be so. In particular the substructure concepts developed in Chapter II of this thesis together with the various embedding theorems and their applications are not immediately available fnom the first order theory and seem to be of sufficient worth to warrant developing the higher order theory in its own terms. This, anyway, is the basic justification for the approach and content of the thesis.</p>


2022 ◽  
Vol 0 (0) ◽  
Author(s):  
Pablo Rivas-Robledo

Abstract In this article I present HYPER-REF, a model to determine the referent of any given expression in First-Order Logic (FOL). I also explain how this model can be used to determine the referent of a first-order theory such as First-Order Arithmetic (FOA). By reference or referent I mean the non-empty set of objects that the syntactical terms of a well-formed formula (wff) pick out given a particular interpretation of the language. To do so, I will first draw on previous work to make explicit the notion of reference and its hyperintensional features. Then I present HYPER-REF and offer a heuristic method for determining the reference of any formula. Then I discuss some of the benefits and most salient features of HYPER-REF, including some remarks on the nature of self-reference in formal languages.


1996 ◽  
Vol 307 ◽  
pp. 135-165 ◽  
Author(s):  
M. A. Jog ◽  
P. S. Ayyaswamy ◽  
I. M. Cohen

The evaporation and combustion of a single-component fuel droplet which is moving slowly in a hot oxidant atmosphere have been analysed using perturbation methods. Results for the flow field, temperature and species distributions in each phase, inter-facial heat and mass transfer, and the enhancement of the mass burning rate due to the presence of convection have all been developed correct to second order in the translational Reynolds number. This represents an advance over a previous study which analysed the problem to first order in the perturbation parameter. The primary motivation for the development of detailed analytical/numerical solutions correct to second order arises from the need for such a higher-order theory in order to investigate fuel droplet ignition and extinction characteristics in the presence of convective flow. Explanations for such a need, based on order of magnitude arguments, are included in this article. With a moving droplet, the shear at the interface causes circulatory motion inside the droplet. Owing to the large evaporation velocities at the droplet surface that usually accompany drop vaporization and burning, the entire flow field is not in the Stokes regime even for low translational Reynolds numbers. In view of this, the formulation for the continuous phase is developed by imposing slow translatory motion of the droplet as a perturbation to uniform radial flow associated with vigorous evaporation at the surface. Combustion is modelled by the inclusion of a fast chemical reaction in a thin reaction zone represented by the Burke–Schumann flame front. The complete solution for the problem correct to second order is obtained by simultaneously solving a coupled formulation for the dispersed and continuous phases. A noteworthy feature of the higher-order formulation is that both the flow field and transport equations require analysis by coupled singular perturbation procedures. The higher-order theory shows that, for identical conditions, compared with the first-order theory both the flame and the front stagnation point are closer to the surface of the drop, the evaporation is more vigorous, the droplet lifetime is shorter, and the internal vortical motion is asymmetric about the drop equatorial plane. These features are significant for ignition/extinction analyses since the prediction of the location of the point of ignition/extinction will depend upon such details. This article is the first of a two-part study; in the second part, analytical expressions and results obtained here will be incorporated into a detailed investigation of fuel droplet ignition and extinction. In view of the general nature of the formulation considered here, results presented have wider applicability in the general areas of interfacial fluid mechanics and heat/material transport. They are particularly useful in microgravity studies, in atmospheric sciences, in aerosol sciences, and in the prediction of material depletion from spherical particles.


2002 ◽  
Vol 67 (2) ◽  
pp. 859-878 ◽  
Author(s):  
L. R. Galminas ◽  
John W. Rosenthal

AbstractWe show that the first order theory of the lattice <ω(S) of finite dimensional closed subsets of any nontrivial infinite dimensional Steinitz Exhange System S has logical complexity at least that of first order number theory and that the first order theory of the lattice (S∞) of computably enumerable closed subsets of any nontrivial infinite dimensional computable Steinitz Exchange System S∞ has logical complexity exactly that of first order number theory. Thus, for example, the lattice of finite dimensional subspaces of a standard copy of ⊕ωQ interprets first order arithmetic and is therefore as complicated as possible. In particular, our results show that the first order theories of the lattice (V∞) of c.e. subspaces of a fully effective ℵ0-dimensional vector space V∞ and the lattice of c.e. algebraically closed subfields of a fully effective algebraically closed field F∞ of countably infinite transcendence degree each have logical complexity that of first order number theory.


Sign in / Sign up

Export Citation Format

Share Document