This thesis presents a framework for understanding first-order theories by investigating their models. A common application is to help users, who are not necessarily experts in formal methods, analyze software artifacts, such as access-control policies, system configurations, protocol specifications, and software designs. The framework suggests a strategy for exploring the space of finite models of a theory via augmentation. Also, it introduces a notion of provenance information for understanding the elements and facts in models with respect to the statements of the theory. The primary mathematical tool is an information-preserving preorder, induced by the homomorphism on models, defining paths along which models are explored. The central algorithmic ideas consists of a controlled construction of the Herbrand base of the input theory followed by utilizing SMT-solving for generating models that are minimal under the homomorphism preorder. Our framework for model-exploration is realized in Razor, a model-finding assistant that provides the user with a read-eval-print loop for investigating models.

Thesis. 1978. M.S.--Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. / MICROFICHE COPY AVAILABLE IN ARCHIVES AND ENGINEERING. / Bibliography: leaf 99. / M.S.

We have investigated several monomial and permutation progenitors, including 2*8 : [8 : 2], 2*18 : [(22 x 3) : (3x2)], 2*16 : [22 : 4], and 2*16 : 24, 5*2 :m [4•22], 5*2 :m [(4x2) :• 2], 103∗2 :m [17 : 2] and 103∗4 :m [17 : 4]. We have discovered original, to the best of our knowledge, symmetric presentations of a number of finite groups, including PSL(2, 7), M12 , A6 : 2, A7 , PSL(2, 25), 25 :• S4, 24 : S3, PSL(2, 271), 12 x PSL(2, 13), and U(3, 7) : 2. We will present our construction of several of these images, including the Mathieu sporadic simple group M12 over the maximal subgroup PSL(2, 11), PSL(2, 17) over D9, PSL(2, 16) : 2 over [24 : 5] and PGL(2, 7) over S3. We will also give our method of finding isomorphism classes of images.

Mixed-format tests containing both multiple-choice (MC) items and constructed-response (CR) items are used in many testing programs. The use of multiple formats presents a number of measurement challenges, one of which is how to adequately equate mixed-format tests under the common-item nonequivalent groups (CINEG) design, especially when, due to practical constraints, the common-item set contains only MC items. The purpose of this dissertation was to evaluate how equating properties were preserved for mixed-format tests under the CINEG design. Real data analyses were conducted on 22 equating linkages of 39 mixed-format tests from the Advanced Placement (AP) Examination program. Four equating methods were used: the frequency estimation (FE) method, the chained equipercentile (CE) method, item response theory (IRT) true score equating, and IRT observed score equating. In addition, cubic spline postsmoothing was used with the FE and CE methods. The factors of investigation were the correlation between MC and CR scores, the proportion of common items, the proportion of MC-item score points, and the similarity between alternate forms. Results were evaluated using three equating properties: first-order equity, second-order equity, and the same distributions property. The main findings from this dissertation were as follows: (1) Between the two IRT equating methods, true score equating better preserved first-order equity than observed score equating, and observed score equating better preserved second-order equity and the same distributions property than true score equating. (2) Between the two traditional methods, CE better preserved first-order equity than FE, but in terms of preserving second-order equity and the same distributions property, CE and FE produced similar results. (3) Smoothing helped to improve the preservation of second-order equity and the same distributions property. (4) A higher MC-CR correlation was associated with better preservation of first-order equity for both IRT methods. (5) A higher MC-CR correlation was associated with better preservation of second-order equity for IRT true score equating. (6) A higher MC-CR correlation was associated with better preservation of the same distributions property for IRT observed score equating. (7) The proportion of common items, the proportion of MC score points, and the similarity between forms were not found to be associated with the preservation of the equating properties. These results are interpreted in the context of research literature in this area and suggestions for future research are provided.

<p>For random waves the free surface elevation can be described by a number of individual wave parameters. The main objective of this work has been to study the statistical properties of individual parameters in successive waves; the wave crest height, the wave height and the wave period.</p><p>In severe sea states the wave crest heights exhibit a nonlinear behavior, which must be reflected in the models. An existing marginal distribution that uses second order Stokes-type nonlinearity is transformed to a two-dimensional distribution by use of the two–dimensional Rayleigh distribution. This model only includes sum frequency effects. A two-dimensional distribution is also established by transforming a second order model including both sum and different frequency effects. Both models are based on the narrow-band assumption, and the effect of finite water depth is included. A parametric wave crest height distribution proposed by Forristall (2000) has been extended to two dimensions by transformation of the two-dimensional Weibull distribution. </p><p>Two successive wave heights are modeled by a Gaussian copula, which is referred to as the Nataf model. Results with two initial distributions for the transformation are presented, the Næss (1985) model and a two-parameter Weibull distribution, where the latter is in best agreement with data. The results are compared with existing models. The Nataf model has also been used for modeling three successive wave heights. Results show that the Nataf transformation of three successive wave heights can be approximated by a first order autoregression model. This means that the distribution of the wave height given the previous wave height is independent of the wave heights prior to the previous wave height. The simulation of successive wave heights can be done directly without simulating the time series of the complete surface elevation. </p><p>Successive wave periods are modeled with the Nataf transformation by using a two-parameter Weibull distribution and a generalized Gamma distribution as the initial distribution, where the latter is in best agreement with data. Results for the marginal and two-dimensional distributions are compared with existing models. In practical applications, it is often of interest to consider successive wave periods with corresponding wave heights exceeding a certain threshold. Results show that the distribution for successive wave periods when the corresponding wave heights exceed the root-mean-square value of the wave heights can be approximated by a multivariate Gaussian distribution. When comparing the results with data, a long time series is needed in order to obtain enough data cases. Results for three successive wave periods are also presented. </p><p>The models are compared with field data from the Draupner field and the Japan Sea, and with laboratory data from experiments at HR Wallingford. In addition, data from numerical simulations based on second order wave theory, including both sum and frequency effects, are included.</p>

For random waves the free surface elevation can be described by a number of individual wave parameters. The main objective of this work has been to study the statistical properties of individual parameters in successive waves; the wave crest height, the wave height and the wave period. In severe sea states the wave crest heights exhibit a nonlinear behavior, which must be reflected in the models. An existing marginal distribution that uses second order Stokes-type nonlinearity is transformed to a two-dimensional distribution by use of the two–dimensional Rayleigh distribution. This model only includes sum frequency effects. A two-dimensional distribution is also established by transforming a second order model including both sum and different frequency effects. Both models are based on the narrow-band assumption, and the effect of finite water depth is included. A parametric wave crest height distribution proposed by Forristall (2000) has been extended to two dimensions by transformation of the two-dimensional Weibull distribution. Two successive wave heights are modeled by a Gaussian copula, which is referred to as the Nataf model. Results with two initial distributions for the transformation are presented, the Næss (1985) model and a two-parameter Weibull distribution, where the latter is in best agreement with data. The results are compared with existing models. The Nataf model has also been used for modeling three successive wave heights. Results show that the Nataf transformation of three successive wave heights can be approximated by a first order autoregression model. This means that the distribution of the wave height given the previous wave height is independent of the wave heights prior to the previous wave height. The simulation of successive wave heights can be done directly without simulating the time series of the complete surface elevation. Successive wave periods are modeled with the Nataf transformation by using a two-parameter Weibull distribution and a generalized Gamma distribution as the initial distribution, where the latter is in best agreement with data. Results for the marginal and two-dimensional distributions are compared with existing models. In practical applications, it is often of interest to consider successive wave periods with corresponding wave heights exceeding a certain threshold. Results show that the distribution for successive wave periods when the corresponding wave heights exceed the root-mean-square value of the wave heights can be approximated by a multivariate Gaussian distribution. When comparing the results with data, a long time series is needed in order to obtain enough data cases. Results for three successive wave periods are also presented. The models are compared with field data from the Draupner field and the Japan Sea, and with laboratory data from experiments at HR Wallingford. In addition, data from numerical simulations based on second order wave theory, including both sum and frequency effects, are included.

We develop the method of Fischer-Riesz equations for general boundary value problems elliptic in the sense of Douglis-Nirenberg. To this end we reduce them to a boundary problem for a (possibly overdetermined) first order system whose classical symbol has a left inverse. For such a problem there is a uniquely determined boundary value problem which is adjoint to the given one with respect to the Green formula. On using a well elaborated theory of approximation by solutions of the adjoint problem, we find the Cauchy data of solutions of our problem.

The probabilistic design of dynamic systems with degrading components is difficult. Design of dynamic systems typically involves the optimization of a time-invariant performance measure, such as Energy, that is estimated using a dynamic response, such as angular speed. The mechanistic models developed to approximate this performance measure are too complicated to be used with simple design calculations and lead to lengthy simulations. When degradation of the components is assumed, in order to determine suitable service times, estimation of the failure probability over the product lifetime is required. Again, complex mechanistic models lead to lengthy lifetime simulations when the Monte Carlo method is used to evaluate probability. Based on these problems, an efficient methodology is presented for probabilistic design of dynamic systems and to estimate the cumulative distribution function of the time to failure of a performance measure when degradation of the components is assumed. The four main steps include; 1) transforming the dynamic response into a set of static responses at discrete cycle-time steps and using Singular Value Decomposition to efficiently estimate a time-invariant performance measure that is based upon a dynamic response, 2) replacing the mechanistic model with an approximating function, known as a “metamodel” 3) searching for the best design parameters using fast integration methods such as the First Order Reliability Method and 4) building the cumulative distribution function using the summation of the incremental failure probabilities, that are estimated using the set-theory method, over the planned lifetime. The first step of the methodology uses design of experiments or sampling techniques to select a sample of training sets of the design variables. These training sets are then input to the computer-based simulation of the mechanistic model to produce a matrix of corresponding responses at discrete cycle-times. Although metamodels can be built at each time-specific column of this matrix, this method is slow especially if the number of time steps is large. An efficient alternative uses Singular Value Decomposition to split the response matrix into two matrices containing only design-variable-specific and time-specific information. The second step of the methodology fits metamodels only for the significant columns of the matrix containing the design variable-specific information. Using the time-specific matrix, a metamodel is quickly developed at any cycle-time step or for any time-invariant performance measure such as energy consumed over the cycle-lifetime. In the third step, design variables are treated as random variables and the First Order Reliability Method is used to search for the best design parameters. Finally, the components most likely to degrade are modelled using either a degradation path or a marginal distribution model and, using the First Order Reliability Method or a Monte Carlo Simulation to estimate probability, the cumulative failure probability is plotted. The speed and accuracy of the methodology using three metamodels, the Regression model, Kriging and the Radial Basis Function, is investigated. This thesis shows that the metamodel offers a significantly faster and accurate alternative to using mechanistic models for both probabilistic design optimization and for estimating the cumulative distribution function. For design using the First-Order Reliability Method to estimate probability, the Regression Model is the fastest and the Radial Basis Function is the slowest. Kriging is shown to be accurate and faster than the Radial Basis Function but its computation time is still slower than the Regression Model. When estimating the cumulative distribution function, metamodels are more than 100 times faster than the mechanistic model and the error is less than ten percent when compared with the mechanistic model. Kriging and the Radial Basis Function are more accurate than the Regression Model and computation time is faster using the Monte Carlo Simulation to estimate probability than using the First-Order Reliability Method.

Recently, various approximate design problems for low-degree trigonometric regression models on a partial circle have been solved. In this paper we consider approximate and exact optimal design problems for first-order trigonometric regression models without intercept on a partial circle. We investigate the intricate geometry of the non-convex exact trigonometric moment set and provide characterizations of its boundary. Building on these results we obtain a complete solution of the exact D-optimal design problem. It is shown that the structure of the optimal designs depends on both the length of the design interval and the number of observations.

In this work minimally supported D-optimal designs for response surface models with spatially correlated errors are studied. The spatially correlated errors describe the correlation between two measurements depending on their distance d through the covariance function C(d)=exp(-rd). In one dimensional design space, the minimally supported D-optimal designs for polynomial models with spatially correlated errors include two end points and are symmetric to the center of the design region. Exact solutions for simple linear and quadratic regression models are presented. For models with third or higher order, numerical solutions are given. While in two dimensional design space, the minimally supported D-optimal designs are invariant under translation¡Brotation and reflection. Numerical results show that a regular triangle on the experimental region of a circle is a minimally supported D-optimal design for the first-order response surface model.