The Mukhin-Tarasov-Varchenko Theorem (previously the Shapiro Conjecture) asserts that a Schubert problem has all solutions distinct and real if the Schubert varieties involved osculate a rational normal curve at real points. When conjectured, it sparked interest in real osculating Schubert calculus, and computations played a large role in developing the surrounding theory. Our purpose is to uncover generalizations of the Mukhin-Tarasov-Varchenko Theorem, proving them when possible. We also improve the state of the art of computationally solving Schubert problems, allowing us to more effectively study ill-understood phenomena in Schubert calculus. We use supercomputers to methodically solve real osculating instances of Schubert problems. By studying over 300 million instances of over 700 Schubert problems, we amass data significant enough to reveal generalizations of the Mukhin-Tarasov- Varchenko Theorem and compelling enough to support our conjectures. Combining algebraic geometry and combinatorics, we prove some of these conjectures. To improve the efficiency of solving Schubert problems, we reformulate an instance of a Schubert problem as the solution set to a square system of equations in a higher- dimensional space. During our investigation, we found the number of real solutions to an instance of a symmetrically defined Schubert problem is congruent modulo four to the number of complex solutions. We proved this congruence, giving a generalization of the Mukhin-Tarasov-Varchenko Theorem and a new invariant in enumerative real algebraic geometry. We also discovered a family of Schubert problems whose number of real solutions to a real osculating instance has a lower bound depending only on the number of defining flags with real osculation points. We conclude that our method of computational investigation is effective for uncovering phenomena in enumerative real algebraic geometry. Furthermore, we point out that our square formulation for instances of Schubert problems may facilitate future experimentation by allowing one to solve instances using certifiable numerical methods in lieu of more computationally complex symbolic methods. Additionally, the methods we use for proving the congruence modulo four and for producing an

Computation with large-scale heterogeneous data typically requires universal traversal to search for all occurrences of a substructure that matches a possibly complex search pattern, whose context may be different in different places within the data. Both aspects cause difficulty for existing general-purpose programming languages, because these languages are designed for homogeneous data and have problems typing the different substructures in heterogeneous data, and the complex patterns to match with the substructures. Programmers either have to hard-code the structures and search patterns, preventing programs from being reusable and scalable, or have to use low-level untyped programming or programming with special-purpose query languages, opening the door to type mismatches that cause a high risk of program correctness and security problems. This thesis invents the concept of pattern structures, and proposes a general solution to the above problems - a programming technique using pattern structures. In this solution, well-typed pattern structures are defined to represent complex search patterns, and pattern searching over heterogeneous data is programmed with pattern parameters, in a statically-typed language that supports first-class typing of structures and patterns. The resulting programs are statically-typed, highly reusable for different data structures and different patterns, and highly scalable in terms of the complexity of data structures and patterns. Adding new kinds of patterns for an application no longer requires changing the language in use or creating new ones, but is only a programming task. The thesis demonstrates the application of this approach to, and its advantages in, two important examples of computation with heterogeneous data, i.e., XML data processing and Java bytecode analysis. / Thesis (Ph.D, Computing) -- Queen's University, 2007-08-27 09:43:38.888

In this thesis we study the physical properties of the manifold in general relativity that admits a conformal motion. The results obtained are general as the metric tensor field is not specified. We obtain the Lie derivative along a conformal Killing vector of the kinematical and dynamical quantities for the general energy-momentum tensor of neutral matter. Equations obtained previously are regained as special cases from our results. We also find the Lie derivative of the energy-momentum tensor for the electromagnetic field. In particular we comprehensively study conformal symmetries in the Bianchi I spacetime. The conformal Killing vector equation is integrated to obtain the general conformal Killing vector and the conformal factor subject to integrability conditions. These conditions place restrictions on the metric functions. A particular solution is exhibited which demonstrates that these conditions have a nonempty solution set. The solution obtained is a generalisation of the results of Moodley (1991) who considered locally rotationally symmetric spacetimes. The Killing vectors are regained as special cases of the conformal solution. There do not exist any proper special conformal Killing vectors in the Bianchi I spacetime. The homothetic vector is found for a nonvanishing constant conformal factor. We establish that the vacuum Kasner solution is the only Bianchi I spacetime that admits a homothetic vector. Furthermore we isolate a class of vectors from the solution which causes the Bianchi I model to degenerate into a spacetime of higher symmetry. / Thesis (M.Sc.)-University of KwaZulu-Natal, 1992.

In this dissertation we study conformal symmetries in the Stephani universe which is a generalisation of the Robertson-Walker models. The kinematics and dynamics of the Stephani universe are discussed. The conformal Killing vector equation for the Stephani metric is integrated to obtain the general solution subject to integrability conditions that restrict the metric functions. Explicit forms are obtained for the conformal Killing vector as well as the conformal factor . There are three categories of solution. The solution may be categorized in terms of the metric functions k and R. As the case kR - kR = 0 is the most complicated, we provide all the details of the integration procedure. We write the solution in compact vector notation. As the case k = 0 is simple, we only state the solution without any details. In this case we exhibit a conformal Killing vector normal to hypersurfaces t = constant which is an analogue of a vector in the k = 0 Robertson-Walker spacetimes. The above two cases contain the conformal Killing vectors of Robertson-Walker spacetimes. For the last case in - kR = 0, k =I 0 we provide an outline of the integration process. This case gives conformal Killing vectors which do not reduce to those of RobertsonWalker spacetimes. A number of the calculations performed in finding the solution of the conformal Killing vector equation are extremely difficult to analyse by hand. We therefore utilise the symbolic manipulation capabilities of Mathematica (Ver 2.0) (Wolfram 1991) to assist with calculations. / Thesis (M.Sc.)-University of Natal, Durban, 1992.

The research for this thesis has followed two main paths: the one of probability logics and the other of type systems and logical frameworks, bringing them together through interactive theorem proving. With the development of computer technology and the need to capture real-world dynamics, situations, and problems, reasoning under uncertainty has become one of the more important research topics of today, and one of the tools for formalizing this kind of knowledge are probability logics. Given that probability logics, serving as decision-making or decision-support systems, often form a basis for expert systems that find their application in fields such as game theory or medicine, their correct functioning is of great importance, and formal verification of their properties would add an additional level of security to the design process. On the other hand, in the field of logical frameworks and interactive theorem proving, attention has been directed towards a more natural way of encoding formal systems where derivation rules are subject to side conditions which are either rather difficult or impossible to encode naively, in the Edinburgh Logical Framework \LF or any other type-theory based Logical Framework, due to their inherent limitations, or to the fact that the formal systems in question need to access the derivation context, or the structure of the derivation itself, or other structures and mechanisms not available at the object level. The first part of the thesis deals with the development and formal verification of probability logics. First, we introduce a Probability Logic with Conditional Operators - LPCP, its syntax, semantics, and a sound and strongly-complete axiomatic system, featuring an infinitary inference rule. We prove the obtained formalism decidable, and extend it so as to represent evidence, making it the first propositional axiomatization of reasoning about evidence. Next, we show how to encode probability logics LQI and LQnI in the Proof Assistant Coq. Both of these logics extend classical logic with modal-like probability operators, and both feature an infinitary inference rule. LQI allows iterations of probability operators, while LQnI does not. We proceed to formally verify their key properties - soundness, strong completeness, and non-compactness. In this way, we formally justify the use of probabilistic SAT-solvers for the checking of consistency-related questions. In the second part of the thesis, we present LFP - a Logical Framework with External Predicates, by introducing a mechanism for locking and unlocking types and terms into LF, allowing the use of external oracles. We prove that LFP satisfies all of the main meta-theoretical properties (strong normalization, confluence, subject reduction, decidability of type checking). We develop a corresponding canonical framework, allowing for easy proofs of encoding adequacy. We provide a number of encodings - the simple untyped lambda-calculus with a Call-by-Value reduction strategy, the Design-by-Contract paradigm, a small imperative language with Hoare Logic, Modal Logics in Hilbert and Natural Deduction style, and Non-Commutative Linear Logic (encoded for the first time in an LF-like framework), illustrating that in LFP we can encode side-conditions on the application of rules elegantly, and achieve a separation between derivation and computation, resulting in cleaner and more readable proofs. We believe that the results presented in this thesis can serve as a foundation for fruitful future research. On the one hand, the obtained formal correctness proofs add an additional level of security when it comes to the construction of expert systems constructed using the verified logics, and pave way for further formal verification of other probability logics. On the other hand, there is room for further improvement, extensions, and deeper analysis of the LFP framework, as well as the building of a prototype interactive theorem prover based on LFP and discovering its place in the world of proof assistants.

On présente une Logique Probabiliste avec des Operateurs Conditionnels - LPCP, sa syntaxe, sémantique, axiomatisation correcte et fortement complète, comprenant une règle de déduction infinitaire. On prouve que LPCP est décidable, et on l'étend pour qu'il puisse représenter l'évidence, en créant ainsi la première axiomatisation propositionnelle du raisonnement basé sur l'évidence. On codifie les Logiques Probabilistes LPP1Q et LPPQ2 dans l'Assistant de Preuve Coq, et on vérifie formellement leurs propriétés principales: correction, complétude fort et non-compacité. Les deux logiques étendent la Logique Classique avec des opérateurs de probabilité, et présentent une règle de déduction infinitaire. LPPQ1 permet des itérations des opérateurs de probabilité, lorsque LPPQ2 ne le permet pas. On a formellement justifié l'utilisation des solveurs SAT probabilistes pour vérifier les questions liées à la cohérence. On présente LFP, un Cadre Logique avec Prédicats Externes, en introduisant un mécanisme pour bloquer et débloquer types et termes dans LF, en permettant l'utilisation d'oracles externes. On démontre que LFP satisfait tous les principales propriétés et on développe un cadre canonique correspondant, qui permet de prouver l'adéquation. On fournit diverses encodages - le λ-calcul non-typé avec la stratégie de réduction CBV, Programmation-par-Contrats, un langage impératif avec la Logique de Hoare, des Logiques Modales et la Logique Linéaire Non-Commutative, en montrant que en LFP on peut codifier aisément des side-conditions dans l'application des règles de typage et atteindre une séparation entre vérification et computation, en obtenant des preuves plus claires et lisibles.

The attitude determination and control subsystem (ADCS) is a critical part of any satellite conducting scientific experiments that require accurate positioning (such as Earth observation and solar spectroscopy). The engineering design process of this subsystem has a long heritage; yet, it is surrounded by several limitations due to the stringent physical constraints imposed on small satellites. These limitations (e.g., limited computational capabilities, power, and volume) require an improved approach for the purpose of attitude determination (AD) and control. Previous space missions relied mostly on the extended Kalman filter (EKF) to estimate the relative orientation of the spacecraft because it yields an optimal estimator under the assumption that the measurement and process models are white Gaussian processes. However, this filter suffers from several limitations such as a high computational cost. This thesis addresses all the limitations found in small satellites by introducing a computationally efficient algorithm for AD based on a fuzzy inference system with a gradient decent optimization technique to calculate and optimize the bounds of the membership functions. Also, an optimal controller based on a fractional proportional-integral-derivative controller has been implemented to provide an energy-efficient control scheme. The AD algorithm presented in this thesis relies on the residual information of the Earth magnetic field. In contrast to current approaches, the new algorithm is immune to several limitations such as sensitivity to initial conditions and divergence problems. Additionally, its computational cost has been reduced. Simulation results illustrate a higher pointing stability, while maintaining satisfying levels of pointing accuracy and increasing reliability. Moreover, the optimal controller designed provides a shorter time delay, settling time, and steady-state error. This demonstrates that accurate attitude determination and control can be conducted in small spacecraft.

Calculus at the university level is taken by thousands of undergraduate students each year. However, a significant number of students struggle with the subject, resulting in poor problem solving, low achievement, and high failure rates in the calculus courses overall (e.g., Kaput, 1994; Szydlik, 2000; Tall, 1985; Tall & Ramos, 2004; White & Mitchelmore, 1996). This is cause for concern as the lack of success in university calculus creates further barriers for students who require the course for their programs of study. This study examines this issue from the perspective of Tall’s Three Worlds of Mathematics (Tall, 2004a, 2004b, 2008), a theory of mathematics and mathematical cognitive development. A fundamental argument of Tall’s theory suggests that connecting between the different mathematical worlds, named the Embodied-Conceptual, Symbolic-Proceptual, and Formal-Axiomatic worlds, is essential for full cognitive development and understanding of mathematical concepts. Working from this perspective, this research examined, through the use of calculus task questions and semi-structured interviews, how fifteen undergraduate calculus students made connections between the different mathematical worlds for the calculus topics of limits and derivatives. The analysis of the findings suggests that how the students make connections can be described by eight different Response Categories. The study also found that how the participants made connections between mathematical worlds might be influenced by the type of questions that are asked and their experience in calculus courses. I infer that these Response Categories have significance for this study and offer potential for further study and educational practice. I conclude by identifying areas of further research in regards to calculus achievement, the Response Categories, and other findings such as a more detailed study of the influence of experience.

Geodätische Messabweichungen werden oft gut durch Wahrscheinlichkeitsverteilungen beschrieben, die steilgipfliger als die Gaußsche Normalverteilung sind. Das gilt besonders, wenn grobe Messabweichungen nicht völlig ausgeschlossen werden können. Neben einigen in der Geodäsie bisher verwendeten Verteilungen (verallgemeinerte Normalverteilung, Hubers Verteilung) diskutieren wir hier die skalenkontaminierte Normalverteilung, die für die praktische Rechnung einige Vorteile bietet. / Geodetic measurement errors are frequently well described by probability distributions, which are more peak-shaped than the Gaussian normal distribution. This is especially true when gross errors cannot be excluded. Besides some distributions used so far in geodesy (generalized normal distribution, Huber’s distribution) we discuss the scale contaminated normal distribution, which offers some advantages in practical calculations.

This paper was presented in WCSMO-9, Shizuoka.