scholarly journals CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory

2011 ◽  
Author(s):  
Bruno Barras ◽  
Jean-Pierre Jouannaud ◽  
Pierre-Yves Strub ◽  
Qian Wang
Keyword(s):  
Type Theory ◽  
Order Theory ◽  
Order Type ◽  
Higher Order ◽  
First Order ◽  
First Order Theory

Analysis of three-layer composite plates with a new higher-order layerwise formulation

2014 ◽  
Vol 21 (3) ◽  
pp. 401-404
Author(s):  
Dalal A. Maturi ◽  
Antonio J.M. Ferreira ◽  
Ashraf M. Zenkour ◽  
Daoud S. Mashat
Keyword(s):  
Composite Plates ◽  
Order Theory ◽  
Higher Order ◽  
Basis Functions ◽  
Numerical Accuracy ◽  
First Order ◽  
The Core ◽  
First Order Theory ◽  
Layer Composite ◽  
Vibration Problems

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.

A Simple Higher-Order Theory for Laminated Composite Plates

1984 ◽  
Vol 51 (4) ◽  
pp. 745-752 ◽  
Author(s):  
J. N. Reddy
Keyword(s):  
Shear Deformation ◽  
Deformation Theory ◽  
Shear Deformation Theory ◽  
Laminated Composite ◽  
Composite Plates ◽  
Order Theory ◽  
Higher Order ◽  
Laminated Composite Plates ◽  
First Order ◽  
First Order Theory

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.

scholarly journals HOL-λσ: an intentional first-order expression of higher-order logic

2001 ◽  
Vol 11 (1) ◽  
pp. 21-45 ◽  
Author(s):  
GILLES DOWEK ◽  
THERESE HARDIN ◽  
CLAUDE KIRCHNER
Keyword(s):  
Order Theory ◽  
Higher Order ◽  
Search Method ◽  
Order Logic ◽  
Automated Deduction ◽  
Higher Order Logic ◽  
First Order ◽  
Proof Search ◽  
First Order Theory ◽  
Explicit Substitutions

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.

Effects of higher-order nonlinearity and finite geometry on the propagation of KdV solitons

1988 ◽  
Vol 40 (3) ◽  
pp. 545-552 ◽  
Author(s):  
B. Ghosh ◽  
K. P. Das
Keyword(s):  
Planar Waveguide ◽  
Electron Plasma ◽  
Finite Geometry ◽  
Order Theory ◽  
Higher Order ◽  
Ion Acoustic Wave ◽  
Electron Plasma Wave ◽  
First Order ◽  
First Order Theory ◽  
Ion Acoustic

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.

Decidability and undecidability of extensions of second (first) order theory of (generalized) successor

1966 ◽  
Vol 31 (2) ◽  
pp. 169-181 ◽  
Author(s):  
Calvin C. Elgot ◽  
Michael O. Rabin
Keyword(s):  
Order Theory ◽  
Higher Order ◽  
Second Order ◽  
First Order ◽  
First Order Theory ◽  
Function Constant

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.

scholarly journals Constructing a small category of setoids

2011 ◽  
Vol 22 (1) ◽  
pp. 103-121 ◽  
Author(s):  
OLOV WILANDER
Keyword(s):  
Type Theory ◽  
Order Theory ◽  
Small Category ◽  
First Order ◽  
First Order Theory ◽  
Unique Identity

Consider the first-order theory of a category.d It has a sort of objects, and a sort of arrows (so we may think of it as a small category). We show that, assuming the principle of unique substitutions, the setoids inside a type theoretic universe provide a model for this first-order theory. We also show that the principle of unique substitutions is not derivable in type theory, but that it is strictly weaker than the principle of unique identity proofs.

scholarly journals Ultraproducts and Higher Order Models

2021 ◽  
Author(s):  
◽  
Wilfred Gordon Malcolm
Keyword(s):  
Order Theory ◽  
Higher Order ◽  
Embedding Theorems ◽  
First Order ◽  
First Order Theory ◽  
Higher Order Theory ◽  
Higher Order Models

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

scholarly journals Evaporation and combustion of a slowly moving liquid fuel droplet: higher-order theory

1996 ◽  
Vol 307 ◽  
pp. 135-165 ◽  
Author(s):  
M. A. Jog ◽  
P. S. Ayyaswamy ◽  
I. M. Cohen
Keyword(s):  
Flow Field ◽  
Order Theory ◽  
Higher Order ◽  
Second Order ◽  
Spherical Particles ◽  
General Nature ◽  
Fuel Droplet ◽  
First Order ◽  
First Order Theory ◽  
Higher Order Theory

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.

Computational Models for Multilayered Composite Shells with Application to Tires

1996 ◽  
Vol 24 (1) ◽  
pp. 11-38 ◽  
Author(s):  
G. M. Kulikov
Keyword(s):  
Type Theory ◽  
Computational Models ◽  
Geometrical Nonlinearity ◽  
Higher Order ◽  
Stress Strain ◽  
Strain Fields ◽  
First Order ◽  
Timoshenko Type ◽  
Joint Influence ◽  
Discrete Layer

Abstract This paper focuses on four tire computational models based on two-dimensional shear deformation theories, namely, the first-order Timoshenko-type theory, the higher-order Timoshenko-type theory, the first-order discrete-layer theory, and the higher-order discrete-layer theory. The joint influence of anisotropy, geometrical nonlinearity, and laminated material response on the tire stress-strain fields is examined. The comparative analysis of stresses and strains of the cord-rubber tire on the basis of these four shell computational models is given. Results show that neglecting the effect of anisotropy leads to an incorrect description of the stress-strain fields even in bias-ply tires.

Sign in / Sign up

Export Citation Format

Share Document