The main purpose of this thesis is to develop a search strategy for space debris that are in the geosynchronous orbit (GEO) region. The search strategy is not an effort to find the object initially but rather if found one time to aid in finding it again within a small time frame. This was a request from NASA Johnson Space Center Orbital Debris Program Office through the MODEST, Michigan Orbital Debris Survey Telescope, program. A single definitive search pattern was not found, however depending on the COEs of the orbit specific search strategy can be employed. These search strategies are far from perfect and can be improved upon with more rigorous testing as well as a larger data sample. Another goal is to look for correlation between the orbital parameters and the errors in the predicted right ascension (RA) and the declination (DEC). This was accomplished by varying the different orbital parameters by ±10% individually while holding the other parameters constant. This showed some correlation existed between some parameters and their errors, in particular there was correlation between a variation in right ascension of ascending node (RAAN) and the value of RAAN itself. The correlation found was that with the higher the value of RAAN the larger the RMS error.

The importance of search partnerships has grown as a mode to search for innovations. However, in spite of this development, notions of open innovation combined with new propositions to change the search process in favour of sustainability have unravelled a need to take stock of the existing literature of search partnerships and the aims that these partnerships follow. This review addresses this shortcoming and synthesises the literature on search partnerships to analyse the current state of knowledge to deliver future research opportunities. A systematic review process was adopted by means of a set a set of pre-defined stages. These stages included the formulation and positioning of the review question within the larger literature domains, a systematic research process which included the adoption of search strings, relevance and quality appraisal criteria, as well as a stock-taking process of descriptive and thematic features, which followed the logic of prescriptive synthesis. This process led to a representative sample of 73 articles which were analysed subsequently. The tentative findings reveal that the literature is underpinned by a combination of theories linking to evolutionary or transaction-based understandings of search partnerships. Also, six conditions were found to drive search partnerships and when they are likely to form. Moreover five interventions were identified that relate to the use of search methods, boundary spanning activities, and the number, type and involvement levels with the partner. Finally search partnerships have been found to yield five outcomes: partnerships, and various types of innovations, higher social goals, as well as market knowledge. By combining contexts, interventions, and outcomes, research opportunities are identified that should inform future reviews, including the need for more research in sustainability-led search partnership contexts and a better understanding of search strategy configurations in relation interventions used and anticipated search partnership outcomes obtained.

Inference systems Τ and search strategies E for T are distinguished from proof procedures β = (T,E) The completeness of procedures is studied by studying separately the completeness of inference systems and of search strategies. Completeness proofs for resolution systems are obtained by the construction of semantic trees. These systems include minimal α-restricted binary resolution, minimal α-restricted M-clash resolution and maximal pseudo-clash resolution. Certain refinements of hyper-resolution systems with equality axioms are shown to be complete and equivalent to refinements of the pararmodulation method for dealing with equality. The completeness and efficiency of search strategies for theorem-proving problems is studied in sufficient generality to include the case of search strategies for path-search problems in graphs. The notion of theorem-proving problem is defined abstractly so as to be dual to that of and" or tree. Special attention is given to resolution problems and to search strategies which generate simpler before more complex proofs. For efficiency, a proof procedure (T,E) requires an efficient search strategy E as well as an inference system T which admits both simple proofs and relatively few redundant and irrelevant derivations. The theory of efficient proof procedures outlined here is applied to proving the increased efficiency of the usual method for deleting tautologies and subsumed clauses. Counter-examples are exhibited for both the completeness and efficiency of alternative methods for deleting subsumed clauses. The efficiency of resolution procedures is improved by replacing the single operation of resolving a clash by the two operations of generating factors of clauses and of resolving a clash of factors. Several factoring methods are investigated for completeness. Of these the m-factoring method is shown to be always more efficient than the Wos-Robinson method.

No description available.

An understanding of the spatio-temporal dynamics of marine predator populations is essential for the sustainable management of marine resources. Tagging studies are providing ever more information about the movements and migrations of marine predators and much has been learned about where these predators spend their time. However little is known about their underlying motivations, making it difficult to make predictions about how apex predators will respond to changing environments. While much progress has been made in behavioural ecology through the use of optimality models, in the marine environment the necessary costs and benefits are difficult to quantify making this approach less successful than with terrestrial studies. One aspect of foraging behaviour that has proved tractable however is the optimisation of random searches. Work by statistical physicists has shown that a specialised movement, known as Lévy flight, can optimise the rate of new prey patch encounters when new prey patches are beyond sensory range. The resulting Lévy flight foraging (LFF) hypothesis makes testable predictions about marine predator search behaviour that can be addressed with the theoretical and empirical studies that form the basis of this thesis. Results presented here resolve the controversy surrounding the hypothesis, demonstrating the optimality of Lévy searches under a broader set of conditions than previously considered, including whether observed Lévy patterns are innate or emergent. Empirical studies provide robust evidence for the prevalence of Lévy search patterns in the movements of diverse marine pelagic predators such as sharks, tunas and billfish as well as in the foraging patterns of albatrosses, overturning a previous study. Predictions from the LFF hypothesis concerning fast moving prey are confirmed leading to simulation studies of ambush predator’s activity patterns. Movement analysis is then applied to the assessment of by-catch mitigation efforts involving VMS data from long-liners and simulated sharks.

In the present work I compare the search strategies for solving scheduling problems from the view of constraint programming. The thesis is focused on scheduling problems containing alternative activities. An analysis of previously published various ways of modelling the problems is provided, next description and experimental comparison of search strategies targetting these models is provided. The influence of strategies on the speed of the solver is studied primarily. As a sideeffect the work studies the ways how Choco solver, which was utililized for implementation of the experiments, can be used to solve the scheduling problems with alternative activities.

In a search game, a seeker searches for a hider in some space. The seeker wishes to find the hider as quickly as possible, and the hider wishes to avoid capture as long as possible. In this paper, I will focus on the case where the search space is a star, and the only information the seeker has is the speed of the hider. I will provide algorithms for some cases where the seeker is guaranteed to find the hider and prove optimality for some of these cases. Also, I will look at some cases where the hider can avoid capture indefinitely. I will also present some results for searching on trees.

Learning from Demonstration (LfD) has been used in robotics research for the last decades to solve issues pertaining to conventional programming of robots. This framework enables a robot to learn a task simply from a human demonstration. However, it is unfeasible to teach a robot all possible scenarios, which may lead to e.g. the robot getting stuck. In order to solve this, a search is necessary. However, no current work is able to provide a search approach that is both simple and general. This thesis develops and evaluates a new framework based on LfD that combines both of these aspects. A single demonstration of a human search is made and a model of it is learned. From this model a search trajectory is sampled and optimized. Based on that trajectory, a prediction of the encountered environmental forces is made. An impedance controller with feed-forward of the predicted forces is then used to evaluate the algorithm on a Peg-in-Hole task. The final results show that the framework is able to successfully learn and reproduce a search from just one single human demonstration. Ultimately some suggestions are made for further benchmarks and development.

La vérification des programmes est un enjeu majeur pour les applications critiques comme l'aviation, l'aérospatiale ou les systèmes embarqués. Les approches Bounded model checking (e.g., CBMC) et de programmation par contraintes (e.g., CPBPV, …) reposent sur la recherche de contre-exemples qui violent une propriété du programme à vérifier. La recherche de tels contre-exemples peut être très longue et coûteuse lorsque les programmes à vérifier contiennent des calculs en virgule flottante. Ceci est dû en grande partie au fait que les stratégies de recherche existantes ont été conçues pour des domaines finis et, dans une moindre mesure, pour des domaines continus. Dans cette thèse, nous proposons un ensemble de stratégie de recherche dédié à la vérification de programme avec du calcul sur les flottants. Les stratégies proposées pour les choix de variables et de choix de valeur se basent sur des propriétés propres aux flottants. Ces propriétés utilisent des caractéristiques des domaines des variables, ou de la structure des contraintes. Certaines propriétés qui portent sur les domaines des variables sont classiques comme la taille et la cardinalité et d'autres beaucoup plus spécifiques comme la densité. Les notions de taille et cardinalité sont équivalentes sur les entiers, mais ne le sont pas sur les flottants. Ainsi la densité capture une variabilité qui est très spécifique aux flottants dont la moitié se trouve entre [-1,1]. De manière similaire les propriétés qui portent sur la structure des contraintes sont, pour certaines tels que le degré ou le nombre d’occurrences, issues des domaines finis, et pour d’autres beaucoup plus spécifiques, comme l’absorption, et la cancellation; ces deux propriétés capturent des phénomènes qui sont généralement la cause de fortes déviations du programme flottant vis-à-vis son interprétation sur les réels et donc de l’existence même de beaucoup de contre-exemples. Pour chaque propriété, deux stratégies de choix de variables sont proposées. La première choisit la variable qui minimise la propriété, alors que la seconde choisit la variable qui la maximise. Les stratégies de choix de valeurs essaient quant à elles de tirer profit des phénomènes d'absorption et de cancellation. L'évaluation de ces stratégies sur un ensemble de programmes réalistes est très encourageante : ces stratégies sont plus efficaces que les stratégies standards. / Program verification is a major issue for critical applications such as aviation, aerospace or embedded systems. Bounded model checking (e.g., CBMC) and constraint programming (e.g., CPBPV,...) approaches are based on the search for counter-examples that violate a property of the program to verify. The search for such counter-examples can be very time-consuming and costly when the programs to be verified contain floating point calculations. This is largely due to the fact that existing research strategies have been designed for finite domains and, to a lesser extent, for continuous domains. In this thesis, we propose a set of search strategies dedicated to program verification with floating point computation. The proposed strategies for variable and value selection are based on specific floating properties. These properties use characteristics of the variable domains, or the constraint structure. Some properties that focus on the domains of the variables are classic such as size and cardinality and others much more specific like density. The notions of size and cardinality are equivalent on the integers, but not on the floats. Density captures a variability that is very specific to the floats, half of which are between[-1.1]. Similarly, the properties that concern the structure of constraints are, for some such as the degree or number of occurrences, derived from finite domains, and for others much more specific, such as absorption, and cancellation; these two properties capture phenomena that are generally the cause of strong deviations of the floating point program from its interpretation on the reals and hence the existence of many counterexamples. For each property, two variable selection strategies are proposed. The first one chooses the variable that minimizes the property, while the second one chooses the variable that maximizes it. Value choice strategies try to take advantage of the phenomena of absorption and cancellation.

After school, Kenyan graduates struggle in a labour market that does not offer enough employment opportunities. Some graduates search for years, get disillusioned, and give up ever finding formal employment. Some find jobs, but not necessarily in the field of their profession, and possibly below their qualification. Kenya invests in and accumulates human capital that is untapped or even lost. One way to improve one’s job search is the use of personal social networks. By applying social network and social distance theories, this study explores the conditions under which networks can become helpful to a jobseeker. Personal experiences of young Kenyan graduates were used to find out about their job search strategies and their social networks. Insights from recruiters’ perspectives about recruitment processes offered a wholesome view on how jobseekers get connected to jobs. The main data sources were online interviews and an online survey. The findings suggest that a network’s willingness to help might depend on level of reciprocity, that many jobseekers do not have access to helpful networks, and that the ability of a network to help might be restricted due to level of influence or applicability. The study concludes that a combination of various job search strategies offers the best chances to connect a jobseeker to a job, but also that companies need to adapt their recruitment processes in include people who are less connected.