Parametric optimization of anisogrid shells of irregular structure

The paper focuses on an approach to solving the problem of parametric optimization of anisogrid mesh shells with an irregular structure. Mesh structures are widely used in building and engineering. This study deals with the optimal design of such structures used in aerospace industry. The problem of optimal design of mesh structures is relevant, as it makes it possible to increase the efficiency of their use, minimizing the weight, provided the strength and stability conditions are met. In our work we formulate the problem of optimal design of mesh structures in general form, and introduce an optimization algorithm based on the simplex search method in which we use a partial predicate of a feasible region to describe the non-convex smooth areas of boundaries. The results of solving the optimization problem for a particular structure with a violation of the regularity of the rib structure are given. Findings of research show that the considered algorithm can be used for optimal design of both regular and non-regular mesh structures.

An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates

Summary In the paper we give a formalization in the Mizar system [2, 1] of the rules of an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions which was proposed in [7, 9]. The rules are formalized on the semantic level. The details of the approach used to implement this formalization are described in [5]. We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions) [5] which is a triple of a pre-condition represented by a partial predicate, a program, represented by a partial function which maps data to data, and a post-condition, represented by a partial predicate, which informally means that if the pre-condition on a program’s input data is defined and true, and the program’s output after a run on this data is defined (a program terminates successfully), and the post-condition is defined on the program’s output, then the post-condition is true. We formalize and prove the soundness of the rules of the inference system [9, 7] for such semantic Floyd-Hoare triples. For reasoning about sequential composition of programs and while loops we use the rules proposed in [3]. The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data [4]. Application of these rules often requires reasoning about partial predicates representing preand post-conditions which can be done using the formalized results on the Kleene algebra of partial predicates given in [8].

On an Algorithmic Algebra over Simple-Named Complex-Valued Nominative Data

Summary This paper continues formalization in the Mizar system [2, 1] of basic notions of the composition-nominative approach to program semantics [14] which was started in [8, 12, 10]. The composition-nominative approach studies mathematical models of computer programs and data on various levels of abstraction and generality and provides tools for reasoning about their properties. In particular, data in computer systems are modeled as nominative data [15]. Besides formalization of semantics of programs, certain elements of the composition-nominative approach were applied to abstract systems in a mathematical systems theory [4, 6, 7, 5, 3]. In the paper we give a formal definition of the notions of a binominative function over given sets of names and values (i.e. a partial function which maps simple-named complex-valued nominative data to such data) and a nominative predicate (a partial predicate on simple-named complex-valued nominative data). The sets of such binominative functions and nominative predicates form the carrier of the generalized Glushkov algorithmic algebra for simple-named complex-valued nominative data [15]. This algebra can be used to formalize algorithms which operate on various data structures (such as multidimensional arrays, lists, etc.) and reason about their properties. In particular, we formalize the operations of this algebra which require a specification of a data domain and which include the existential quantifier, the assignment composition, the composition of superposition into a predicate, the composition of superposition into a binominative function, the name checking predicate. The details on formalization of nominative data and the operations of the algorithmic algebra over them are described in [11, 13, 9].

Kleene Algebra of Partial Predicates

Summary We show that the set of all partial predicates over a set D together with the disjunction, conjunction, and negation operations, defined in accordance with the truth tables of S.C. Kleene’s strong logic of indeterminacy [17], forms a Kleene algebra. A Kleene algebra is a De Morgan algebra [3] (also called quasi-Boolean algebra) which satisfies the condition x ∧¬:x ⩽ y ∨¬ :y (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [8]. The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in [3]. A similar notion of a “normal i-lattice” had been previously studied by J.A. Kalman [16]. More details about the origin of this notion and its relation to other notions can be found in [24, 4, 1, 2]. It should be noted that there is a different widely known class of algebras, also called Kleene algebras [22, 6], which generalize the algebra of regular expressions, however, the term “Kleene algebra” used in this paper does not refer to them. Algebras of partial predicates naturally arise in computability theory in the study on partial recursive predicates. They were studied in connection with non-classical logics [17, 5, 18, 32, 29, 30]. A partial predicate also corresponds to the notion of a partial set [26] on a given domain, which represents a (partial) property which for any given element of this domain may hold, not hold, or neither hold nor not hold. The field of all partial sets on a given domain is an algebra with generalized operations of union, intersection, complement, and three constants (0, 1, n which is the fixed point of complement) which can be generalized to an equational class of algebras called DMF-algebras (De Morgan algebras with a single fixed point of involution) [25]. In [27] partial sets and DMF-algebras were considered as a basis for unification of set-theoretic and linguistic approaches to probability. Partial predicates over classes of mathematical models of data were used for formalizing semantics of computer programs in the composition-nominative approach to program formalization [31, 28, 33, 15], for formalizing extensions of the Floyd-Hoare logic [7, 9] which allow reasoning about properties of programs in the case of partial pre- and postconditions [23, 20, 19, 21], for formalizing dynamical models with partial behaviors in the context of the mathematical systems theory [11, 13, 14, 12, 10].

The Quest for Cognates: A Reconstruction of Oblique Subject Constructions in Proto-Indo-European

The enigma of the origin of non-canonical subject marking in the world’s languages has been met with two competing hypotheses: the Object-to-Subject Hypothesis and the Oblique Subject/Semantic Alignment Hypothesis (cf. Eythórsson and Barðdal, 2005). The present article argues in favor of the Oblique Subject/Semantic Alignment Hypothesis, presenting five sets of cognate predicates in the early/archaic Indo-European daughter languages that occur in the Oblique Subject Construction. These cognate sets have not figured in the earlier literature. Not only are they stem cognates, but they also occur in a cognate compositional predicate and argument structure construction, with a dative subject, the verb ‘be’ and an adjective, a noun, or an adverb. The discovery of these cognate data sets immediately invalidates the axiomatic assumption that non-canonical subject marking must originate in an earlier object status of these arguments. The data, moreover, form the input of a correspondence set, on which basis we reconstruct predicate-specific oblique subject constructions, a partial predicate-specific oblique subject construction, as well as a more abstract schematic dative subject construction for Proto-Indo-European, using the formalism of Sign-based Construction Grammar. The evidence presented here thus suggests that oblique subjects are inherited from an early proto-stage and do not represent an individual development in the Indo-European daughter languages.