The examination timetabling (exam-timeslot-room assignment) problem involves assigning exams to a specific or limited number of timeslots and rooms, with the aim of satisfying the hard constraints and the soft constraints as much as possible. Most of the techniques reported in the literature have been applied to solve simplified examination benchmark datasets, available within the scientific literature. In this research we bridge the gap between research and practice by investigating a problem taken from the Universiti Malaysia Pahang (UMP), a real world capacitated examination timetabling problem. This dataset has several novel constraints, in addition to those commonly used in the literature. Additionally, the invigilator scheduling problem (invigilator assignment) was also investigated as it has not received the same level of research attention as the examination scheduling (although it is just as important to educational institutions). The formal models are defined, and constructive heuristics was developed for both problems in which the overall problems are solved with a two-phase approach which involves scheduling the exam to timeslot and room, and follows with scheduling the invigilator. During the invigilator assignment, we assume that there is already an examination timetable in place (i.e. previously generated). It reveals that the invigilator scheduling solution dependent on the number of rooms selected from the exam-timeslot-room assignment phase (i.e. a lesser number of used rooms would minimises the invigilation duties for staff), this encourages us to further improve the exam-timeslot-room timetable solution. An improvement on the result was carried out using modified extended great deluge algorithm (modified-GDA) and multi-neighbourhood GDA approach (that use more than one neighbourhood during the search). The modified-GDA uses a simple to understand parameter and allows the boundary that acts as the acceptance level, to dynamically change during the search. The propose approaches able to produce good quality solution when compared to the solutions from the proprietary software used by UMP. In addition, our solutions adhere to all hard constraints which the current systems fail to do. Finally, we extend our research onto investigating the Second International Timetabling Competition (ITC2007) dataset as it also contains numerous constraints much similar to UMP datasets. Our propose approach able to produce competitive solutions when compared to the solutions produced by other reported works in the literature.

This thesis investigates the feasibility of establishing a generalised approach for defining similarity metrics between 3D shapes for the casting design problem in Case-Based Reasoning (CBR). This research investigates a new approach for improving the quality of casting design advice achieved from a CBR system using casting design knowledge associated with past cases. The new approach uses enhanced similarity metrics to those used in previous research in this area to achieve improvements in the advice given. The new similarity metrics proposed here are based on the decomposition of casting shape cases into a set of components. The research into metrics defines and uses the Component Type Similarity Metric (CTM) and Maximum Common Subgraph (MCS) metric between graph representations of the case shapes and are focused on the definition of partial similarity between the components of the same type that take into account the geometrical features and proportions of each single shape component. Additionally, the investigation extends the scope of the research to 3D shapes by defining and evaluating a new metric for the overall similarity between 3D shapes. Additionally, this research investigates a methodology for the integration of the CBR cycle and automation of the feature extraction from target and source case shapes. The ShapeCBR system has been developed to demonstrate the feasibility of integrating the CBR approach for retrieving and reusing casting design advice. The ShapeCBR system automates the decomposition process, the classification process and the shape matching process and is used to evaluate the new similarity metrics proposed in this research and the extension of the approach to 3D shapes. Evaluation of the new similarity metrics show that the efficiency of the system is enhanced using the new similarity metrics and that the new approach provides useful casting design information for 3D casting shapes. Additionally, ShapeCBR shows that it is possible to automate the decomposition and classification of components that allow a case shape to be represented in graph form and thus provide the basis for automating the overall CBR cycle. The thesis concludes with new research questions that emerge from this research and an agenda for further work to be pursued in further research in the area.

L'algorithme Branch-and-Bound (B&B) est une méthode de recherche arborescente fréquemment utilisé pour la résolution exacte de problèmes d'optimisation combinatoire (POC). Néanmoins, seules des petites instances peuvent être effectivement résolues sur une machine séquentielle, le nombre de sous-problèmes à évaluer étant souvent très grand. Visant la resolution de POC de grande taille, nous réexaminons la conception et l'implémentation d'algorithmes B&B massivement parallèles sur de larges plateformes hétérogènes de calcul, intégrant des processeurs multi-coeurs, many-cores et et processeurs graphiques (GPUs). Pour une représentation compacte en mémoire des sous-problèmes une structure de données originale (IVM), dédiée aux problèmes de permutation est utilisée. En raison de la forte irrégularité de l'arbre de recherche, l'équilibrage de charge dynamique entre processus d'exploration parallèles occupe une place centrale dans cette thèse. Basés sur un encodage compact de l'espace de recherche sous forme d'intervalles, des stratégies de vol de tâches sont proposées pour processeurs multi-core et GPU, ainsi une approche hiérarchique pour l'équilibrage de charge dans les systèmes multi-GPU et multi-CPU à mémoire distribuée. Trois problèmes d'optimisation définis sur l'ensemble des permutations, le problème d'ordonnancement Flow-Shop (FSP), d'affectation quadratique (QAP) et le problème des n-dames sont utilisés comme cas d'étude. La resolution en 9 heures d'une instance du FSP dont le temps de résolution séquentiel est estimé à 22 ans demontre la capacité de passage à l'échelle des algorithmes proposés sur une grappe de calcul composé de 36 GPUs. / Branch-and-Bound (B&B) is a frequently used tree-search exploratory method for the exact resolution of combinatorial optimization problems (COPs). However, in practice, only small problem instances can be solved on a sequential computer, as B&B generates often generates a huge amount of subproblems to be evaluated. In order to solve large COPs, we revisit the design and implementation of massively parallel B&B on top of large heterogeneous clusters, integrating multi-core CPUs, many-core processors and GPUs. For the efficient storage and management of subproblems an original data structure (IVM) dedicated to permutation problems is used. Because of the highly irregular and unpredictable shape of the B&B tree, dynamic load balancing between parallel exploration processes is one of the main issues addressed in this thesis. Based on a compact encoding of the search space in the form of intervals, work stealing strategies for multi-core and GPU are proposed, as well as hierarchical approaches for load balancing in distributed memory multi-CPU/multi-GPU systems. Three permutation problems, the Flowshop Scheduling Problem (FSP), the Quadratic Assignment Problem (QAP) and the n-Queens puzzle problem are used as test-cases. The resolution, in 9 hours, of a FSP instance with an estimated sequential execution time of 22 years demonstrates the scalability of the proposed algorithms on a cluster composed of 36 GPUs.

A problem of emotion and cognition is considered within a unified theory of cognition. There is a strong case for modern cognitive models to take arousal component of emotion into account because of its significant influence on performance (e.g. the inverted-U effect). Several hypotheses have been proposed to explain this effect, but they have not been integrated into cognitive architectures. Based on the analysis of the ACT-R (Anderson & Lebiere, 1998) cognitive architecture the mechanisms that can be used to model this effect are identified. Then a model of the classical Yerkes and Dodson experiment is introduced. The model matches the data by modifying several parameters, particularly noise and goal value in the conflict resolution strategy. Thus, the model supports the idea that the character of decision making changes for different arousal and motivational states. The effect of these changes on learning is analysed using information theory. In particular, randomness in behaviour due to a noise increase leads to a faster entropy reduction. Thus, noise can improve learning in the initial stage of problem exploration or upon changes in the environment. Furthermore, dynamic motivation can optimise the expenditure of effort. Therefore, emotion may play an important role in adaptation of cognitive processes. It is argued that the current conflict resolution mechanism in ACT-R does not explain the dynamics suggested by the model. A new theory and algorithm are proposed that use posterior estimation of expected costs. There are three main contributions of the thesis: 1) Ways of including the effects of emotion and motivation into cognitive models; 2) The analysis of the role of emotion in learning and intelligence; and 3) The introduction of a new machine learning algorithm suitable for applications not only in cognitive modelling, but in other areas of computer science.

In the real world, many problems are continuous in nature. In some cases, finding the global solutions for these problems is di±cult. The reason is that the problem's objective function is non convex, nor concave and even not differentiable. Tackling these problems is often computationally too expensive. Although the development in computer technologies are increasing the speed of computations, this often is not adequate, particularly if the size of the problem's instance are large. Applying exact methods on some problems may necessitate their linearisation. Several new ideas using heuristic approaches have been considered particularly since they tackle the problems within reasonable computational time and give an approximate solution. In this thesis, the variable neighbourhood search (VNS) metaheuristic (the framework for building heuristic) has been considered. Two variants of variable neighbourhood search metaheuristic have been developed, continuous variable neighbourhood search and reformulation descent variable neighbourhood search. The GLOB-VNS software (Drazic et al., 2006) hybridises the Microsoft Visual Studio C++ solver with variable neighbourhood search metaheuristics. It has been used as a starting point for this research and then adapted and modified for problems studied in this thesis. In fact, two problems have been considered, censored quantile regression and the circle packing problem. The results of this approach for censored quantile regression outperforms other methods described in the literature, and the near-optimal solutions are obtained in short running computational time. In addition, the reformulation descent variable neighbourhood search variant in solving circle packing problems is developed and the computational results are provided.

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS / This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

Pouvoir se déplacer intelligemment dans un environnement inconnu est primordial pour des robots mobiles (Évitement d’Obstacle (EO)). Ceci est nécessaire pour explorer et construire une carte de l’environnement (CArtographie Active (CAA)), carte qui servira à d’autres tâches comme la patrouille (COuverture Active (COA)). Cette thèse se focalise sur la prise de décision pour planifier les déplacements de robots autonomes afin de naviguer, couvrir ou explorer l’environnement. Ainsi, nous nous basons sur la Prise de Décision Séquentielle (PDS) en Intelligence Artificielle et proposons deux contributions concernant : (1) les processus décisionnels de CAA et COA, et (2) la planification à long terme pour la COA. De plus, récemment, les robots mobiles ont commencé à partager l’espace physique avec les humains en fournissant des services comme du ménage à la maison. Dans ces cas, le comportement du robot doit s’adapter à la dynamique du monde. Par conséquent, nous proposons deux autres contributions pour : (3) la CAA en environnements de foule, et (4) l’EO par chemin clairsemé en environnements ambiants / The ability to intelligently navigate in an unknown environment is essential for mobile robots (Obstacle Avoidance (OA)). This is needed to explore and build a map of the environment (Active Mapping (AM)); this map will then support other tasks such as patrolling (Active Coverage (AC)). In this thesis, we focus on decision-making to plan the moves of autonomous robots in order to navigate, cover, or explore the environment. Therefore, we rely on the framework of Sequential Decision-Making (SDM) in Artificial Intelligence to propose two contributions that address: (1) decision processes for AC and AM and (2) long-term planning for AC. Furthermore, mobile robots recently started sharing physical spaces with humans to provide services such as cleaning the house. In such cases, robot behavior should adapt to dynamic aspects of the world. In this thesis, we are interested in deploying autonomous robots in such environments. Therefore, we propose two other contributions that address: (3) short-term AM in crowded environments and (4) clearest path OA in ambient environments

Στη διπλωματική λύνουμε το πρόβλημα του sudoku με χρήση του εκπαιδευτικού ρομπότ της Lego, το LEGO Mindstorm NXT. Το εκπαιδευτικό ρομπότ αυτό δεν έχει συγκεκριμένη μορφή αλλά αποτελείται από αλληλοσυνδεόμενα μεταξύ τους πλαστικά μέρη. Με χρήση αυτών κατασκευάσαμε ένα όχημα που αποτελεί παραλλαγή οχήματος από άλλη εργασία. Το όχημα αυτό μπορεί να κινείται μόνο μπροστά και πίσω. Διαθέτει έναν βραχίονα που μπορεί να κινεί δεξιά-αριστερά και στον οποίο εφαρμόζεται ένας αισθητήρας φωτεινότητας. Τέλος, στον βραχίονα υπάρχει θέση για στυλό. Το πρόβλημα του sudoku που δίνεται στο ρομπότ είναι εκτυπωμένο σε ένα χαρτί Α4. Το ρομπότ αναλαμβάνει να το αναγνωρίσει με τον αισθητήρα, να το επιλύσει και να το αποτυπώσει με τη χρήση του στυλό. Για την επίτευξη αυτού του στόχου επιστρατεύονται αλγόριθμοι ρομποτικής και αλγόριθμοι τεχνητής νοημοσύνης. Συγκεκριμένα για την πλοήγηση του οχήματος εφαρμόζεται μετρική και τοπολογική πλοήγησης, στη συνέχεια για την αναγνώριση του προβλήματος και την ταυτοποίηση κάθε εικόνας που λαμβάνεται υλοποιήσαμε αλγόριθμους μορφολογικής επεξεργασία και τέλος για την επίλυση του προβλήματος sudoku υλοποιήσαμε και συγκρίναμε δύο αλγόριθμους, την αναζήτησης κατά βάθος και την αναζήτηση κατά βάθος με διάδοση περιορισμών. Οι τελικοί αλγόριθμοι που αναπτύχθηκαν διαπιστώσαμε ότι πετυχαίνουν το σκοπό τους αφού το όχημα αναγνωρίζει τους αριθμούς του δοσμένου προβλήματος με ποσοστό επιτυχίας 95%, λύνει τα περισσότερα προβλήματα σε λιγότερο από ένα δευτερόλεπτο και συμπληρώνει επιτυχώς τα κελιά του sudoku με τους σωστούς αριθμούς. Πέρα από αυτές τη σύγκριση των αλγορίθμων θεωρούμε ότι η μελέτη ενός τέτοιου συστήματος είναι ιδανική για εισαγωγή σε θέματα ρομποτικής και μπορεί να χρησιμοποιηθεί ως εκπαιδευτικό εργαλείο πειραματισμού. Μάλιστα ο κώδικας μας σχολιάζεται επαρκώς σε αυτή την εργασία για να είναι ευκολότερη η κατανόηση του. Εκτός αυτού έχουμε αναπτύξει και πρόγραμμα αλληλεπίδρασης χρήστη-ρομπότ μέσω κονσόλας. / We solve the problem of sudoku using the educational robot LEGO Mindstorm NXT, made by LEGO. This educational robot doesn't have specific form but consists of interlinked plastics. We constructed a vehicle that is a variant from another work. This vehicle can move only forward and back. It has an arm that can move side to side and is equipped with a light sensor and a marker. The problem of sudoku is given to the robot in printed form on a A4 paper. The robot at first recognize the problem with the sensor, then it resolves it and finally writes the solution down by using the pen. To achieve this goal we implemented various algorithms. Specifically, we studied robotic algorithms such as metric and topological navigation. Moreover, to identify the printed problem we processed every captured image morphologically and finally to solve the sudoku instance we implemented and compared two methods, first-depth search and first-depth search with constraint propagation. We should mention that our code is written in Java for the lejOS firmware. The final code is capable of recognizing the numbers of the given problem with a success rate of 95%, solving most problems in less than a second and completing the cells on the paper with the correct numbers. Finally, we have developed an accompanying program that is usable for debugging purposes and for calibrating the robot. Even more, it can be used as education tool.

Text in English with abstracts in English, Afrikaans and isiZulu / The formalisation of first-order logic and axiomatic set theory in the first half of the 20th century—along with the advent of the digital computer—paved the way for the development of automated theorem proving. In the 1950s, the automation of proof developed from proving elementary geometric problems and finding direct proofs for problems in Principia Mathematica by means of simple, human-oriented rules of inference. A major advance in the field of automated theorem proving occurred in 1965, with the formulation of the resolution inference mechanism. Today, powerful Satisfiability Modulo Theories (SMT) provers combine SAT solvers with sophisticated knowledge from various problem domains to prove increasingly complex theorems. The combinatorial explosion of the search space is viewed as one of the major challenges to progress in the field of automated theorem proving. Pioneers from the 1950s and 1960s have already identified the need for heuristics to guide the proof search effort. Despite theoretical advances in automated reasoning and technological advances in computing, the size of the search space remains problematic when increasingly complex proofs are attempted. Today, heuristics are still useful and necessary to discharge complex proof obligations. In 2000, a number of heuristics was developed to aid the resolution-based prover OTTER in finding proofs for set-theoretic problems. The applicability of these heuristics to next-generation theorem provers were evaluated in 2009. The provers Vampire and Gandalf required respectively 90% and 80% of the applicable OTTER heuristics. This dissertation investigates the applicability of the OTTER heuristics to theorem proving in the hybrid theorem proving environment Rodin—a system modelling tool suite for the Event-B formal method. We show that only 2 of the 10 applicable OTTER heuristics were useful when discharging proof obligations in Rodin. Even though we argue that the OTTER heuristics were largely ineffective when applied to Rodin proofs, heuristics were still needed when proof obligations could not be discharged automatically. Therefore, we propose a number of our own heuristics targeted at theorem proving in the Rodin tool suite. / Die formalisering van eerste-orde-logika en aksiomatiese versamelingsteorie in die eerste helfte van die 20ste eeu, tesame met die koms van die digitale rekenaar, het die weg vir die ontwikkeling van geoutomatiseerde bewysvoering gebaan. Die outomatisering van bewysvoering het in die 1950’s ontwikkel vanuit die bewys van elementêre meetkundige probleme en die opspoor van direkte bewyse vir probleme in Principia Mathematica deur middel van eenvoudige, mensgerigte inferensiereëls. Vooruitgang is in 1965 op die gebied van geoutomatiseerde bewysvoering gemaak toe die resolusie-inferensie-meganisme geformuleer is. Deesdae kombineer kragtige Satisfiability Modulo Theories (SMT) bewysvoerders SAT-oplossers met gesofistikeerde kennis vanuit verskeie probleemdomeine om steeds meer komplekse stellings te bewys. Die kombinatoriese ontploffing van die soekruimte kan beskou word as een van die grootste uitdagings vir verdere vooruitgang in die veld van geoutomatiseerde bewysvoering. Baanbrekers uit die 1950’s en 1960’s het reeds bepaal dat daar ’n behoefte is aan heuristieke om die soektog na bewyse te rig. Ten spyte van die teoretiese vooruitgang in outomatiese bewysvoering en die tegnologiese vooruitgang in die rekenaarbedryf, is die grootte van die soekruimte steeds problematies wanneer toenemend komplekse bewyse aangepak word. Teenswoordig is heuristieke steeds nuttig en noodsaaklik om komplekse bewysverpligtinge uit te voer. In 2000 is ’n aantal heuristieke ontwikkel om die resolusie-gebaseerde bewysvoerder OTTER te help om bewyse vir versamelingsteoretiese probleme te vind. Die toepaslikheid van hierdie heuristieke vir die volgende generasie bewysvoerders is in 2009 geëvalueer. Die bewysvoerders Vampire en Gandalf het onderskeidelik 90% en 80% van die toepaslike OTTER-heuristieke nodig gehad. Hierdie verhandeling ondersoek die toepaslikheid van die OTTER-heuristieke op bewysvoering in die hibriede bewysvoeringsomgewing Rodin—’n stelselmodelleringsuite vir die formele Event-B-metode. Ons toon dat slegs 2 van die 10 toepaslike OTTER-heuristieke van nut was vir die uitvoering van bewysverpligtinge in Rodin. Ons voer aan dat die OTTER-heuristieke grotendeels ondoeltreffend was toe dit op Rodin-bewyse toegepas is. Desnieteenstaande is heuristieke steeds nodig as bewysverpligtinge nie outomaties uitgevoer kon word nie. Daarom stel ons ’n aantal van ons eie heuristieke voor wat in die Rodin-suite aangewend kan word. / Ukwenziwa semthethweni kwe-first-order logic kanye ne-axiomatic set theory ngesigamu sokuqala sekhulunyaka lama-20—kanye nokufika kwekhompyutha esebenza ngobuxhakaxhaka bedijithali—kwavula indlela ebheke ekuthuthukisweni kwenqubo-kusebenza yokufakazela amathiyoremu ngekhomyutha. Ngeminyaka yawo-1950, ukuqinisekiswa kobufakazi kwasuselwa ekufakazelweni kwezinkinga zejiyomethri eziyisisekelo kanye nasekutholakaleni kobufakazi-ngqo bezinkinga eziphathelene ne-Principia Mathematica ngokuthi kusetshenziswe imithetho yokuqagula-sakucabangela elula, egxile kubantu. Impumelelo enkulu emkhakheni wokufakazela amathiyoremu ngekhompyutha yenzeka ngowe-1965, ngokwenziwa semthethweni kwe-resolution inference mechanism. Namuhla, abafakazeli abanohlonze bamathiyori abizwa nge-Satisfiability Modulo Theories (SMT) bahlanganisa ama-SAT solvers nolwazi lobungcweti oluvela kwizizinda zezinkinga ezihlukahlukene ukuze bakwazi ukufakazela amathiyoremu okungelula neze ukuwafakazela. Ukukhula ngesivinini kobunzima nobunkimbinkimbi benkinga esizindeni esithile kubonwa njengenye yezinselelo ezinkulu okudingeka ukuthi zixazululwe ukuze kube nenqubekela phambili ekufakazelweni kwamathiyoremu ngekhompyutha. Amavulandlela eminyaka yawo-1950 nawo-1960 asesihlonzile kakade isidingo sokuthi amahuristikhi (heuristics) kube yiwona ahola umzamo wokuthola ubufakazi. Nakuba ikhona impumelelo esiyenziwe kumathiyori ezokucabangela okujulile kusetshenziswa amakhompyutha kanye nempumelelo yobuchwepheshe bamakhompyutha, usayizi wesizinda usalokhu uyinkinga uma kwenziwa imizamo yokuthola ubufakazi obuyinkimbinkimbi futhi obunobunzima obukhudlwana. Namuhla imbala, amahuristikhi asewuziso futhi ayadingeka ekufezekiseni izibopho zobufakazi obuyinkimbinkimbi. Ngowezi-2000, kwathuthukiswa amahuristikhi amaningana impela ukuze kulekelelwe uhlelo-kusebenza olungumfakazeli osekelwe phezu kwesixazululo, olubizwa nge-OTTER, ekutholeni ubufakazi bama-set-theoretic problems. Ukusebenziseka kwalawa mahuristikhi kwizinhlelo-kusebenza ezingabafakazeli bamathiyoremu besimanjemanje kwahlolwa ngowezi-2009. Uhlelo-kusebenza olungumfakazeli, olubizwa nge-Vampire kanye nalolo olubizwa nge-Gandalf zadinga ama-90% kanye nama-80%, ngokulandelana kwazo, maqondana nama-OTTER heuristics afanelekile. Lolu cwaningo luphenya futhi lucubungule ukusebenziseka kwama-OTTER heuristics ekufakazelweni kwamathiyoremu esimweni esiyinhlanganisela sokufakazela amathiyoremu esibizwa nge-Rodin—okuyi-system modelling tool suite eqondene ne-Event-B formal method. Kulolu cwaningo siyabonisa ukuthi mabili kuphela kwayi-10 ama-OTTER heuristics aba wusizo ngenkathi kufezekiswa isibopho sobufakazi ku-Rodin. Nakuba sibeka umbono wokuthi esikhathini esiningi ama-OTTER heuristics awazange abe wusizo uma esetshenziswa kuma-Rodin proofs, amahuristikhi asadingeka ezimweni lapho izibopho zobufakazi zingazenzekelanga ngokwazo ngokulawulwa yizinhlelo-kusebenza zekhompyutha. Ngakho-ke, siphakamisa amahuristikhi ethu amaningana angasetshenziswa ekufakazeleni amathiyoremu ku-Rodin tool suite. / School of Computing / M. Sc. (Computer Science)