Unity, a widely used game development platform, offers tools like the WheelCollider for simulating vehicle dynamics. However, the built-in WheelCollider has limitations in accurately simulating realistic vehicle behavior, particularly due to its reliance on a single raycasting approach for ground detection. This method often results in unrealistic vehicle movement, especially on complex terrains where multi-dimensional interaction between the vehicle’s wheels and the ground is critical for achieving a true-to-life simulation. Our primary objective is to design a test suite for a Unity package that overcomes the limitations of the built-in WheelCollider. The test suite contains realistic scenes, like a staircase. We also have a preliminary implementation which uses ConfigurableJoint components, and advanced steering mechanisms such as Ackermann and Skid steering. The focus is to achieve a high level of realistic movement and precision in vehicle movement, which is crucial for applications ranging from racing games to robot simulations.

This paper presents some key outcomes of the European project AiRobo, a collaborative initiative involving five universities from Romania, Germany, Greece, Hungary, and France. This is an educational project targeting higher education students, academic staff, and industry professionals. This paper presents four real-world AI-based robotic applications designed to serve as engaging teaching support materials, particularly for theoretical courses that students often find challenging to grasp. These practical applications are designed to bridge the gap between theory and practice, simplifying complex concepts and making them more accessible. They also aim to enhance the learning and teaching process, making it more engaging, motivating, and appealing for both students and academic staff. We present four real-world AI-based robotic applications: two applications integrating ChatGPT in Pepper and NAO robots are designed to serve as learning assistants for students, and two applications (one with the simulation of an agriculture robot in Unity and an AI-based underwater robot controller) are designed to serve as engaging teaching materials on AI-related subjects, but also for theoretical courses that students often find challenging to grasp. For each application, we outline its scope, model, and implementation code. In addition, the implementation code will be openly accessible in the final version of the paper, enabling academic staff and researchers to easily use and adapt these case studies for their own educational or research tasks.

Algorithm certification or program verification have an increasing importance in the current technological landscape, due to the sharp increase in the complexity of software and software using systems and the high potential of adverse effects in case of failure. For instance robots constitute a particular class of systems that can present high risks of such failures. Sorting on the other hand has a growing area of applications, in particular the ones where organizing huge data collections is critical, as for instance in environmental applications.We present an experiment in formal certification of an original version of the Bubble- Sort algorithm that is functional and tail recursive. The certification is performed in parallel both in Theorema and in Coq, this allows to compare the characteristics and the performance of the two systems. In Theorema the proofs are produced automatically in natural style (similar to human proofs), while in Coq they are based on scripts. However, the background theory, the algorithms, and the proof rules in Theorema are composed by the user without any restrictions – thus error prone, while in Coq one can only use the theories and the proof rules that are rigurously checked by the system, and the algorithms are checked for termination.The goal of our experiments is to contribute to a better understanding and estimation of the complexity of such certification tasks and to create a basis for further increase of the level of automation in the two systems and for their possible integration.

Sorting is an operation that has very important practical applications, in particular for instance in the storage and analysis of data related to the environment, climat change, etc. We describe experiments of automated certification of various sorting algorithms by using the Theorema as well as Coq and we compare the two techniques. The sorting algorithms are: Quick–Sort, Patience–Sort, Min–Sort, Max–Sort, and Min–Max–Sort. In both systems we construct the appropriate underlying theory, we define the algorithms in functional style, we run them on examples and we produce the proof of their correctness together with proofs of various lemmas that are necessary. In Theorema the proofs are almost completely automatic, are presented in natural style, and the underlying theory uses multisets in order to express the fact that the input and the output have the same elements. Moreover the proofs use a generalized induction scheme based on the well-founded ordering on lists defined by strict inclusion of multisets. In Coq the proofs are based on scripts, they require more additional lemmas, and they use element counts to compare the contents of the list. However, both the algorithm definitions as well as the proofs are absolutely rigurous as Coq cannot accept any elements that are not theoretically correct.

We introduce the project Artificial Intelligence based Robotics (AiRobo), a partnership of universities from France, Germany, Greece, Hungary, and Romania. AiRobo’s aim is to significantly raise the level of competence and skills of academic staff in the field of artificial intelligence (AI) based robotics, thereby also increasing the attractivity and reputation of the related departments at the partner universities. We further address the European priority in national contexts regarding inclusion in higher education, covering social inclusion and outreach to people with less opportunities, e.g. people with disabilities or with migrant background. The project partners will collaboratively write a comprehensive book on AI-based robotics, provide tools and video tutorials to support the construction and analysis of robotic systems, develop robotic applications in various fields of high interest to the industry, implement trainings for academic staff of the partners, organize an international summer school and an international conference, and disseminate the project results through various channels.The outcomes of the project will include the training of 25 academic staff from partner universities in teaching AI-based robotic courses, a comprehensive set of teaching materials including the above-mentioned book, 7 robotic applications in different fields, tools and video tutorials, as well as scientific publications.

This research presents a case study on the creation of detailed 3D maps using the Agilex Scout Mini robot equipped with a 3D LiDAR, aimed at improving autonomous navigation in indoor environments. ROS (Robot Operating System) is employed for real-time data acquisition and processing, and the DBSCAN clustering algorithm for segmenting point cloud data. These maps were subsequently integrated into the humanoid robot Pepper, developed by Aldebaran Robotics, enabling Pepper to navigate autonomously and deliver location-based services at the West University of Timisoara. Our results show a point cloud density of approximately 5,000 points per cubic meter, highlighting the LiDAR sensor's capability to capture fine environmental details. Efficient clustering was achieved with an average computation time of 3 seconds per chunk, and path planning demonstrated a high smoothness score of 0.8, improving navigation efficiency. These findings contribute to the field by demonstrating the effectiveness of combining 3D mapping with autonomous robotics for reliable, real-time navigation. Moreover, the integration of Intel RealSense cameras is proposed as a future enhancement to improve object recognition and colour mapping, further expanding the system's potential applications. This case study not only advances academic understanding of autonomous robotic systems but also presents practical and scalable solutions for real-world navigation challenges, offering significant improvements in both accuracy and efficiency.

We present the formalization and the automated verification of the list sorting algorithms Insert-Sort and Merge-Sort in the Coq system and we compare it with the formalization and verification of the same algorithms in the Theorema system, which have been performed in our previous work. This represents a case study in verification of complex al-gorithms, sorting being particularly important because it plays a crucial role in various applications that handle large data amounts, as for instance in environmental modelling and re-search. This is part of our research on using Automated Rea-soning - one of the oldest and most important field of Artificial Intelligence - for formal verification of complex systems, whose safe behaviour must be insured, as for instance in robotic systems that interact with people. Concretely, the specification of correctness of these two al-gorithms, as well as the definition of the algorithms are very similar in the two systems, however the proof styles and the number of necessary lemmas are quite different. Coq needs more lemmas and the proof is constructed via a proof script, and the necessary domain properties are imported from Coq libraries. In Theorema the proof is based on domain-specific inferences and strategies, is presented in natural style, and most of the domain specific properties are embedded in the inference rules and proof strategies. However the Theorema system is in principle error prone, because there is no requirement for algorithm termination, for the consistency of inference rules, and for the proof of the properties. In contrast, in Coq everything is rigorously checked, thus it is guarantied to be correct.

One important characteristic of environment re-search 1 is the handling of very large amounts of data, which can be only be achieved by organizing it in a highly efficient way, in particular by keeping various indexing lists in a sorted way and maintaining them efficiently. Therefore sorting algorithms that are specifically tailored to the various situations occurring in data acquisition, storage, and maintenance are crucial for systems that support advanced environment research, and they are useful only to the extent that they are correct. Checking the correctness of sorting algorithms, especially automatically, is a quite complex task. This paper introduces some special proof-based techniques for the automatic generation of correctness proofs of the algorithms Insert-Sort and Merge-Sort, including their auxiliary subfunctions, in the Theorema system. The proofs are described as they are generated by the system. This case study contributes in discovering novel proof-based techniques for algorithm verification and to the generalization of the techniques that authors have used for proof-based algorithm synthesis.

I. Dramnesc 1, T. Jebelean 2 1West University of Timisoara (ROMANIA) 2Johannes Kepler University (AUSTRIA)

The European Erasmus+ project ARC – Automated Reasoning in the Class aims at improving the academic education in disciplines related to Computational Logic by using Automated Reasoning tools. We present the technical aspects of the tools as well as our education experiments, which took place mostly in virtual lectures due to the COVID pandemics. Our education goals are: to support the virtual interaction between teacher and students in the absence of the blackboard, to explain the basic Computational Logic algorithms, to study their implementation in certain programming environments, to reveal the main relationships between logic and programming, and to develop the proof skills of the students. For the introductory lectures we use some programs in C and in Mathematica in order to illustrate normal forms, resolution, and DPLL (Davis-Putnam-Logemann-Loveland) with its Chaff version, as well as an implementation of sequent calculus in the Theorema system. Furthermore we developed special tools for SAT (propositional satisfiability), some based on the original methods from the partners, including complex tools for SMT (Satisfiability Modulo Theories) that allow the illustration of various solving approaches. An SMT related approach is natural-style proving in Elementary Analysis, for which we developed and interesting set of practical heuristics. For more advanced lectures on rewrite systems we use the Coq programming and proving environment, in order on one hand to demonstrate programming in functional style and on the other hand to prove properties of programs. Other advanced approaches used in some lectures are the deduction based synthesis of algorithms and the techniques for program transformation.

: The international Erasmus+ European Project: “ARC – Automated Reasoning in the Class”, running from 2019 to 2022 is a partnership of universities from Austria, France, Germany, Hungary, and Romania, and has the purpose of developing advanced material for teaching subjects related to Computational Logic by using Automated Reasoning. The material includes a comprehensive textbook treating the necessary theoretical background (selected topics in Mathematical Logic), but mostly the practical methods from Automated Theorem Proving, as well as the description of the basic programming paradigms and the associated languages, in relation to their logical aspects. Furthermore, we address the most important applications, like program verification and testing, semantic representation of information, algorithm synthesis, etc. One of the main goals of the approach is to improve the logical background of the software professionals in order to motivate them to use formal methods for certification of complex systems and thus to avoid costly failures.

We present the principles and the experiments of deduction based synthesis of merging algorithms for binary trees. Merging is an auxiliary function used in certain algorithms for sorting of binary trees, however we also address concatenation of unsorted trees (the result will also be in general not sorted) as well as merging of sorted trees (both inputs as well as the output are sorted). We follow the classical approach to deductive synthesis: the algorithm is extracted from the proof of a synthesis conjecture, which asserts that the merged object exists. The novelty of our approach consists in using multisets for expressing the fact that two trees have the same content, which also allows us to develop new powerful proof techniques, mostly by using induction based on the Noetherian ordering among trees induced by the strict inclusion of the corresponding multisets. As the synthesis proofs proceed on different alternatives, several versions of the algorithms are produced. The experiments result in 24 concatenation algorithms, 4 merging algorithms, as well as some sub-auxiliary algorithms for insertion of an element into the tree and for splitting a tree into two sub-trees having the elements smaller, respectively bigger, than a certain value.

We demonstrate the automatic proof–based synthesis of merging and inserting algorithms for [sorted] binary trees, using the notion of multisets, in the Theorema system. Each algorithm is extracted from the proof of the conjecture based on the specification of the desired function, in the form of a list of [conditional] equalities, which can be directly executed. The proofs are performed in natural style, using general techniques, but most importantly efficient inference rules and strategies specific for the domains involved. In particular we present specific techniques for the construction of arbitrarily nested recursive algorithms by general Noetherian induction, as well as a systematic method for the generation of the conjectures and consequently of the algorithms for the auxiliary functions needed in the main function.

We demonstrate the possibility of automated synthesis of the Bubble–Sort algorithm as a rewrite program, a functional program, and an iterative program, starting from the specification. First a rewrite set of clauses for the algorithm Max–Sort is generated from the automatic proof of the synthesis conjecture, representing the main algorithm as well as the necessary auxiliary functions. This is then transformed into a tail recursive Bubble–Sort and by logical analysis the possibility of adding a flag for avoiding unnecessary recursions is identified. This new, more efficient algorithm is then transformed into a functional program, and finally into an imperative program. The practical experiments are performed using the Theorema system.

We demonstrate the deductive synthesis of the Min-Max-Sort algorithm using multisets in the frame of the Theorema system. Starting from the logical specification of the sorting function (input and output conditions), we show how to construct a synthesis conjecture, from whose proof the algorithm can be constructed. For the proof we choose those inference methods and induction principles such that the synthesized algorithm consists of selecting at each step the minimum and the maximum of the list, and moving them at the ends of the list. We also show how to add, on a logical basis, a specific flag in order to stop the recursion as soon as the list is already sorted. During the main proof new conjectures are produced for the synthesis of auxiliary algorithms, and this process repeats in a cascading fashion until all necessary algorithms are produced. Our proof techniques, which are in natural style, include a novel approach using multisets and the use of cover sets for realizing Noetherian induction. The later has the advantage that the concrete induction hypotheses are created dynamically during the proof of the corresponding induction conclusion, thus no concrete induction principle or algorithm scheme is needed in advance. The synthesis mechanism is implemented in the frame of the Theorema system which allows the construction of mathematical theories, proving in natural style, and computing with the synthesized algorithms.

Using multisets, we develop novel techniques for mechanizing the proofs of the synthesis conjectures for list–sorting algorithms, and we demonstrate them in the Theorema system. We use the classical principle of extracting the algorithm as a set of rewrite rules based on the witnesses found in the proof of the synthesis conjecture produced from the specification of the desired function (input and output conditions). The proofs are in natural style, using standard rules, but most importantly domain specific inference rules and strategies. In particular the use of multisets allows us to develop powerful strategies for the synthesis of arbitrarily structured recursive algorithms by general Noetherian induction, as well as for the automatic generation of the specifications of all necessary auxiliary functions (insert, merge, split), whose synthesis is performed using the same method. The proof techniques are implemented in the Theorema system and generate 8 sorting algorithms and 19 auxiliary functions.

We develop logic and combinatorial methods for automating the generation of sorting algorithms for binary trees, starting from input-output specifications and producing conditional rewrite rules. The main approach consists in proving (constructively) the existence of an appropriate output from every input. The proof may fail if some necessary sub-algorithms are lacking. Then, their specifications are suggested and their synthesis is performed by the same principles. Our main goal is to avoid the possibly prohibitive cost of pure resolution proofs by using a natural-style proving in which domain specific strategies and inference steps lead to a significant increase of efficiency. In addition to classical techniques for natural-style proving, we introduce novel ones (priority of certain types of assumptions, transformation of elementary goals into conditions, special criteria for decomposition of the goal and of the assumptions), as well as methods based on the properties of domain specific relations and functions. In particular, we use combinatorial techniques in order to generate possible witnesses, which in certain cases lead to the discovery of new induction principles. From the proof, the algorithm is extracted by transforming inductive proof steps into recursions, and case-based proof steps into conditionals. The approach is demonstrated in parallel using the Theorema system, by developing the theory, implementing the prover, and performing the proofs of the necessary properties and synthesis conjectures. It is also validated in the Coq system, which allows to compare the facilities of the two systems from the point of view of our application. (C) 2018 Elsevier Ltd. All rights reserved.