ABSTRACT. Monte Carlo Tree Search is a popular method for dealing with complex, highly branched tree search problems that represent sequences, be it steps to win a game or reactions to make a molecule. However, nearly all available algorithm variants deal with one objective only. But what if we have multiple objectives? Up to now, there are very few methods for this and I report on our attempts to use these methods for retrosynthesis (find ways how to make a specific target molecule according to several criteria) and also in game AI. It seems clear that this is a research area with high potential but little activity as of now.

ABSTRACT. We describe applications of symbolic computation towards automating the formal analysis of while-programs implementing polynomial arithmetic. We combine methods from static analysis, symbolic summation and computer algebra to derive polynomial loop invariants, yielding a finite representation of all polynomial equations that are valid before and after each loop execution. While deriving polynomial invariants is in general undecidable, we identify classes of loops for which we automatically can solve the problem of invariant synthesis. We further generalize our work to the analysis of probabilistic program loops. Doing so, we compute higher-order statistical moments over (random) program variables, inferring this way quantitative invariants of probabilistic program loops. Our results yield computer-aided solutions in support of formal software verification, compiler optimization, and probabilistic reasoning.

ABSTRACT. The talk will address the Gaussian Process Theory and its application to Global Illumination, rendering, regression, etc. Regression can be useful in many applications. For example it allows to perform a precise regression for a BRDF or an environment map for which the sampled data (incident radiance, incident-reflected radiances) are not the most significant. Note that the Gaussian Process theory can be applied to different research fields such as crowd simulation, computer vision, etc.

ABSTRACT. In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between the two analyzed semantical paradigms - Kripke and algebraic. In addition, we prove a large number of theorems and derived deduction rules.

ABSTRACT. Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. This is easily remedied by unification, for which an algorithm has already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language while generalising the unification problem and mechanizing a proven-sound solution in Coq.

ABSTRACT. Optics are valuable categorical constructions encapsulating the general notion of bidirectional data accessors, and extensive research has been dedicated to comprehending these structures in recent years. Profunctor representation is a successful framework for encompassing various types of optics, such as lenses, prisms or traversals, starting from a pair of actions of a monoidal category. We enhance the above framework as to include structure-preserving functors of the two monoidal actions involved. This has the advantage of unifying within a single 2-functorial framework not only optics (which usually are treated as arrows in categories), but also morphisms between them, and makes it convenient to manipulate and to reason about them in a uniform manner. From a more practical perspective, there is potential in developing better suited applications like complex data access schemes.

ABSTRACT. The temporary exhibition "Across Your Senses" at the Casa Romei Museum in Ferrara offered, through a multisensory approach, a new visiting experience not only for the general tourist but also for those who are already familiar with and frequent this monumental building and its assets. This text describes some installations and activities designed in relation to virtual reality and augmented reality.

ABSTRACT. The present contribution aims to describe the development of a serious game designed to disseminate knowledge in the field of architecture and archeology. In recent decades, educational video games, or serious games, have emerged as a significant means of engaging students across various educational disciplines. Notably, some of these games have shown considerable potential in conveying both the tangible and intangible aspects of cultural heritage, particularly within the teaching of historical subjects. The case study under consideration involves the initial phase of a game focused on the reconstruction of one corner of the Zeus Temple in the Archeological Park of Agrigento. Following an evaluative test will be conducted with high school and first year university students, in order to gather data generated by its use.

ABSTRACT. The increasing complexity of video games and development costs have necessitated innovative approaches to content creation. Procedural Content Generation (PCG) and AI tools like ChatGPT offer promising solutions. This paper explores the application of ChatGPT in Procedural Level Generation (PLG) for the game "Science Birds". Through a combination of theoretical exploration and practical experiments, we demonstrate how ChatGPT can be leveraged to automate level design, enhancing both efficiency and creativity in game development.

ABSTRACT. As part of the PhD program in History, Representation, and Restoration of Architecture, a serious game for children based on Palazzo Barberini in Rome has been designed, focusing on its graphic component. This study highlights the role of architects in the gamification of cultural heritage, ensuring accurate architectural representation and enhancing communication.

ABSTRACT. The Knowledge Technologies for Democracy (KT4D) project seeks to produce new mechanisms to support the protection of human agency in the context of tensions between democracy and emerging technologies. Addressing this challenge from the perspectives of education, regulation and innovation, the project has chosen to deliver a number of its interventions through the paradigm of serious games. The place of agency in gaming is contested, however, leading the project to weave multiple mechanisms to foster agency as a collective process across its approaches to critical digital literacy, narrative and co-creation.

ABSTRACT. Medical image segmentation is one of the most developed part of image segmentation and it plays a crucial role in computer-aided diagnosis. U-Net paved the way for a series of variants that took advantage of the key features of the network. In this article, different features proposed in the variants of U-Net are adapted and experimented on to create a new architecture that still leaves the idea of a U-shape structure unchanged. The proposed architecture takes advantage of the efficient depth-wise separable convolution, but with a twist. Instead of using the pointwise convolution as the last step in the depth-wise separable convolution, it uses the so called Ghost Module. This results in a very efficient network with a reduced complexity, while still having a great segmentation performance. We compared SUDS with U-Net and its variants across multiple segmentation tasks: skin lesion segmentation and colonscopy segmentation. Experiments demonstrate that SUDS has similar segmentation accuracy compared to U-Net and its variants, while the parameters and floating-point operations are greatly reduced.

ABSTRACT. Automated machines are widely used in industrial environments for the production of different items and generate lots of data following these processes. The proper execution of the machines influences the production output, thus the detection of anomalous behavior in machines' activity using the generated data must be considered to avoid unpleasant outcomes. This paper presents an ensemble unsupervised anomaly detection method characterized by parameterized prediction. The proposed method consists of 2 stages - the first stage uses statistical-based methods to assign artificial labels to the input data. In the second stage, the artificially labeled instances and a feature bagging technique are employed to construct the model's estimators - each estimator calculates the percentiles of the distances computed between its centroid and each instance from the training subset. The model's prediction function is parameterized by a percentile rank. Each estimator computes the distance between its centroid and the evaluated instance: if this distance exceeds the specified percentile value, the estimator classifies the instance as anomaly. A majority vote is applied to determine the final outcome.

ABSTRACT. The field of machine learning has increasingly focused on incremental learning, enabling systems to continually adapt and improve by integrating new knowledge while retaining previously learned information. One particular area of interest is class-incremental learning, where the learning system sequentially acquires new classes without access to or with limited exposure to past data. The primary challenge in class-incremental learning is catastrophic forgetting, wherein the model tends to overlook previously learned classes when confronted with new tasks. One of the class-incremental learning approaches to mitigate catastrophic forgetting is the Incremental Classifier and Representation Learning (iCaRL) framework. In this paper, we propose three new selection criteria for the iCaRL approach. Our best selection criterion, which uses the K-Means clustering algorithm to create diverse groups and then selects exemplars close to the centroids of the clusters, outperforms the original iCaRL selection criterion by over 16% for the MNIST dataset and by over 12% for the FashionMNIST dataset in terms of average accuracy. The full implementation of the iCaRL approach, along with the three proposed selection criteria and detailed experimental results logs, can be found in our publicly available GitHub repository. By contributing to the ongoing development of class-incremental learning techniques, we aim to support the creation of more effective and robust lifelong machine learning systems.

ABSTRACT. Analysing malicious samples is a lengthy task, and, given a set of hundreds, even thousands of files, a security researcher would have to spend multiple hours looking at each sample. In many cases, this is not a feasible solution, considering that new malware is created every day. The flow of such files will not stop, and therefore a way of greatly reducing analysis time is needed. This paper presents the Malware Analysis and Clustering Engine (MACE), a proposed solution to address this problem. It offers the user a modular framework implementing multiple feature extraction methods and clustering algorithms, which can provide a multitude of clustering configurations. The user can experiment with different configurations and choose one that best suits their scenario, obtaining a clustering result that allows them to only analyse a single sample from each cluster and draw a conclusion both for it and all of its peers. This approach significantly accelerates the analysis process. The engine was tested on four different datasets, each trying to exemplify a scenario that is likely to be encountered when using the tool in real situations. Based on the results, it was concluded that MACE does achieve its goal, providing multiple configurations for each dataset that reach both great accuracies and a number of created clusters that is close to the one that was expected.

ABSTRACT. Induction in saturation-based first-order theorem proving is a new exciting direction in automated reasoning, bringing together inductive reasoning and reasoning with full first-order logic extended with theories. In this tutorial, we dive into our recent results in this area.

Traditional approaches to inductive theorem proving, based on goal-subgoal reduction, are incompatible with saturation algorithms where the search space can simultaneously contain hundreds of thousands of formulas, with no clear notion of a goal. Rather, our approach applies induction by theory lemma generation: from time to time we add to the search space instances of induction axioms, which are valid in the underlying theory but not valid in first-order predicate logic. To formalize this, we introduce new inference rules adding (clausal forms of) such induction axioms within saturation. Applications of these rules are triggered by recognition of formulas in the search space that can be considered as goals solvable by induction.

We also propose additional reasoning methods for strengthening inductive reasoning, as well as for handling recursive function definitions. We implemented our work in the Vampire theorem prover and will demonstrate the practical impact in experiments.

The tutorial will consist of the following parts supported by live demonstrations:

Introduction to saturation-based reasoning and superposition Integration of induction into saturation [1] Case studies: integer induction and recursive definitions [2, 3] How far can we go with induction in saturation? Future outlooks: using automated inductive proving in proof assistants and beyond The tutorial is based on work made with several co-authors and the tutorial content was jointly created with Petra Hozzova.

References: [1] Induction in Saturation-Based Proof Search (2019), G. Reger and A. Voronkov, in Proc. of CADE https://doi.org/10.1007/978-3-030-29436-6_28 [2] Integer Induction in Saturation (2021), P. Hozzová, L. Kovács, and A. Voronkov, in Proc. of CADE https://doi.org/10.1007/978-3-030-79876-5_21 [3] Induction with Recursive Definitions in Superposition (2021), M. Hajdu, P. Hozzová, L. Kovács, and A. Voronkov, in Proc. of FMCAD https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34 For a survey, also see: Getting Saturated with Induction (2022), M. Hajdu, P. Hozzová, L. Kovács, G. Reger, and A. Voronkov, in Principles of Systems Design https://doi.org/10.1007/978-3-031-22337-2_15

ABSTRACT. The aim of this paper is threefold: first, we present a few relevant facts about the way in which the technique of enriching contractive mappings was introduced; secondly, we expose the main contributions in the area of enriched mappings established by the authors and their collaborators by using this technique; and third, we survey some related developments in the very recent literature which were authored by other researchers.

ABSTRACT. In this talk we will use the notion of nonlinear multi-value Feng-Liu operator in order to prove some fixed point theorems in the context of a set endowed with two metrics. An application to an integral inclusion is also given.

ABSTRACT. We establish new fixed point theorems for Maia’s fixed point theorem in the setting of a space with a distance, more precisely when one of the metrics is replaced with a distance. We also present some examples to illustrate the theoretical results.

ABSTRACT. This paper deals with the notion of f-metric space, a genuine generalization of the concept of b-metric space. We present Matkowski, Kannan and Chatterjea type fixed point theorems in the context of f-metric spaces.

ABSTRACT. Let $(X,d)$ be a metric space, $P(X)$ be the set of all nonempty subsets of $X$ and $T:X\to P(X)$ be a a multi-valued operator. Then, the pair $(x^*,y^*)\in X\times X$ is called a coupled fixed point for $T$ if \begin{equation}\label{ecfp} \left\{\begin{array}{lll} x^*\in T(x^*,y^*)\\ y^*\in T(y^*,x^*). \end{array}\right. \end{equation} It is easy to observe that $z^*:=(x^*,y^*)$ is a coupled fixed point of $T$ if and only if $z^*$ is a fixed point of the multi-valued operator $$F_T:X\times X\to P(X\times X), \ F_T(x,y)=T(x,y)\times T(y,x).$$

Exploiting this remark, in this paper we will give some existence and approximations results for the coupled fixed point problem. Several extensions and some open questions are also considered.

ABSTRACT. In this paper, we present some results about the aproximation of fixed points of enriched nonexpansive operators. There are numerous works in this regard (for example [3], [4], [5] [6], [26], [30] and references to them). Of course, the bibliografical references are extensive and they are mentioned at the end of this paper. In order to approximate the fixed points of enriched nonexpansive mappings, we use the Krasnoselskii-Mann iterative algorithm and a modified Krasnoselskii-Mann iterative algorithm for which we prove weak and strong convergence theorems. Also, in this paper, we make a comparative study about some classical convergence theorems from the literature in the class of enriched nonexpansive mappings using the two algorithms.

ABSTRACT. The main purpose of this paper is to extend some results of fixed point theorems from the general class of nonexpansive mappings, introduced by Vasile Berinde, denoted b-enriched nonexpansive mappings to multivalued mappings in Hilbert space

ABSTRACT. Abstract. We introduce common fixed point theorems using the technique of enriched Banach contractions for single-valued mappings under the assumption of Rweakly commuting condition, R-weakly commuting of type (Ag) and R-weakly commuting of type (Af): We give examples for each theorem in turn to suport our results. We obtained related results of Pant [3], H. K. Pathak, Y. J. Cho and S. M. Kang [2] and V. Berinde and M. Pacurar [1].

ABSTRACT. This paper contains a comparison between a Genetic Algorithm (GA) and a Non-dominated Sorting Genetic Algorithm II (NSGA-II) on the Portfolio Optimisation Problem, based on the Modern Portfolio Theory proposed by Markowitz (1952, 1956).

We use the real-world data of the S&P 500 index (quarterly returns of top 200 stocks from 2019 to 2024, and top 442 stocks from 2004 to 2016), and show that both algorithms can yield returns above the index, in mixed bull and bear market conditions.

N-point Crossover accelerates algorithm convergence, and by using the Sharpe Ratio, the NSGA-II outperformed most models based on Stochastic Dominance we tested, according to the metrics in Bruni el. al. (2017).

ABSTRACT. This study explores feature selection for classifying galaxy morphology using the extensive Galaxy Zoo 2 dataset. We investigate supervised and unsupervised learning methods to group galaxies based on key features, aiming to replicate supervised learning results. We evaluate various feature selection methods and compare them to an existing classification approach. Our results demonstrate that a reduced set of features based on adjusted vote fractions improves classification accuracy and potentially reduces computational complexity. While unsupervised clustering partially groups galaxies by morphology, further optimization is required. This work suggests that feature selection and unsupervised learning are promising techniques for the efficient classification of large galaxy datasets in upcoming astronomical surveys.

ABSTRACT. This paper presents a novel anomaly detection methodology termed Statistical Aggregated Anomaly Detection (SAAD). The SAAD approach integrates advanced statistical techniques with machine learning, and its efficacy is demonstrated through validation on real sensor data from a Hardware-in-the-Loop (HIL) environment within the automotive domain. The key innovation of SAAD lies in its ability to significantly enhance the accuracy and robustness of anomaly detection when combined with Fully Connected Networks (FCNs) augmented by dropout layers. Comprehensive experimental evaluations indicate that the standalone statistical method achieves an accuracy of 72.1%, whereas the deep learning model alone attains an accuracy of 71.5%. In contrast, the aggregated method achieves a superior accuracy of 88.3% and an F1 score of 0.921, thereby outperforming the individual models. These results underscore the effectiveness of SAAD, demonstrating its potential for broad application in various domains, including automotive systems.

ABSTRACT. A multiset over X is a function from a set X to the set N of positive integers, indicating that each element of X has associated a positive multiplicity. This notion was generalized by introducing the hybrid sets which also allow negative multiplicities. Since the set of all integers are denoted by Z, the hybrid sets can be named Z-multisets. The set Z of integers is a group under the operation of addition. Starting from this observation, we introduce a generalization of the hybrid sets by defining the group-valued multisets. These multisets over a set X are functions from X to an arbitrary group G, ensuring an inverse for each multiplicity (not necessarily a number) of the elements of X (together with other features derived from the group properties). We denote them by G-multisets. In particular, Z-multisets are G-multisets; in general, Z can be replaced by any group G, and this aspect allows to get deeper relationships and correlations among the quantitative attributes (multiplicities) for elements of X, useful for various models and optimizations (e.g., in economy). For instance, whenever we use elements of X having certain (quantitative) attributes, we can precisely describe and use the elements of X having the inverse (quantitative) attributes. In our books [Springer 2016, Springer 2020], we studied the multisets allowing negative multiplicities both in the Zermelo-Fraenkel framework and in the finitely supported framework (where only finitely supported sets are allowed), analyzing the correspondence between some properties of these generalized multisets obtained in finitely supported framework and those obtained in the classical ZermeloFraenkel framework. Finitely supported sets are related to the permutation models of Zermelo-Fraenkel set theory with atoms. These models were introduced in 1930s by Fraenkel, Lindenbaum and Mostowski to prove the independence of the axiom of choice from the other axioms of Zermelo-Fraenkel set theory with atoms (ZFA). More recently, finitely supported sets have been developed in Zermelo-Fraenkel (ZF) set theory by equipping ZF sets with actions of a group of one-to-one and onto transformations of some basic elements called atoms. Sets with permutation actions were used to investigate the variables binding, renaming and choosing fresh names in the theory of programming since the notions of structural recursion and structural induction can be adequately transferred into this new framework, as well as in describing automata, languages and Turing machines that operate over infinite alphabets. The notions of invariant set and finitely supported structure are introduced and described in previous papers of the authors. An invariant set is defined as a usual ZF set endowed with a group action of the group of all one-to-one and onto transformations of certain fixed infinite ZF set A of basic elements (called atoms) satisfying a finite support requirement. This requirement states that any element in an invariant set has to be finitely supported, i.e. for any such element x there should exist a finite set of atoms S_x such that any permutation of atoms fixing S_x pointwise also leaves the element x invariant under the related group action. A finitely supported set is defined as a finitely supported element in the powerset of an invariant set. A finitely supported structure is defined as a finitely supported set equipped with a finitely supported internal algebraic law or relation (which should be finitely supported as a subset of a Cartesian product of finitely supported sets). The theory of finitely supported structures allows a discrete representation of possibly infinite sets containing enough symmetries to be concisely handled. More specifically, this theory allows us to treat as equivalent the objects that have a certain degree of similarity and to focus only on those objects that are “really different” by involving the notion of finite support. The framework of finitely supported structures contains both the family of non-atomic ZF structures which are proved to be trivially invariant (i.e. all their elements are empty supported) and the family of atomic structures with f inite (possibly non-empty) supports. We have to analyze whether a ZF result preserves its validity when reformulating it by replacing ‘non-atomic ZF structure’ with ‘atomic and finitely supported structure’. The meta-theoretical technique for the translation of ZF results into the framework of atomic finitely supported structures is based on a closure property for finite supports in an hierarchical construction, called ‘S-finite support principle’ claiming that “for any finite set S of atoms, anything that can be defined in higher-order logic from structures supported by S, by using each time only constructions supported by S, is also supported by S”. The formal involvement of the related S-finite support principle implies a step-by-step construction of the support of a structure by using, at every step, the previously constructed supports of the substructures of the related structure. However, there are ZF results that cannot be translated into an atomic framework as we proved in [Springer 2020]. In this tutorial, by extending the results in [Springer 2016] and [Springer 2020], we define and investigate the group-valued multisets, also in the framework of finitely supported sets. By involving the theory of finitely supported sets, we are able to study group-valued multisets over infinite sets X in a finitary manner. We introduce finitely supported groups and provided some relevant examples of these structures. The finitely supported groups are finitely supported sets equipped with finitely supported internal group laws. We prove that the set of all finitely supported bijections of a finitely supported set, the set of all finitely supported automorphisms of a finitely supported group, the set of all finitely supported inner automorphisms of a finitely supported group, and the set of all equivalence classes of finite words with letters belonging to a finitely supported set, all are finitely supported groups. We prove an isomorphism theorem for finitely supported groups and a result showing that the finitely supported group of all finitary permutations of atoms coincide with the finitely supported group of all bijections of atoms. We also prove some counting properties for the supports of free groups. Then we introduce and study finitely supported group-valued multisets (called G-multisets). For each G-multiset we provide a relationship result between its support and its algebraic support (formed by the family of elements with a non-empty multiplicity). The set of all G-multisets on a finitely supported universe of discourse X can be organized as a finitely supported group and satisfies some (Cayley-type) embedding results, as well as isomorphism and universality theorems. We provide some examples of infinite finitely supported groups that are Dedekind finite (i.e. they do not contain infinite, finitely supported countable subsets). Finally, we connect the concepts of G-multiset, free group and hybrid set (Z-multiset with finite algebraic support) via some universality properties.

[Springer 2016] A. Alexandru, G. Ciobanu. Finitely Supported Mathematics: An Introduction, Springer-Nature, 185 pages, 2016.

[Springer 2020] A. Alexandru, G. Ciobanu. Foundations of Finitely Supported Structures: A set theoretical viewpoint, Springer-Nature, 210 pages, 2020.

ABSTRACT. In this paper, there are studied some strict fixed-point results and stability properties for multi-valued operators satisfying some contraction type conditions. The main purpose of this work is to analyse under which conditions imposed on the admissible perturbation of a multivalued operator, the strict fixed-point results and stability properties still hold true.

ABSTRACT. The purpose of this paper is to present some examples of ordered rectangular b-metric spaces.

ABSTRACT. In this paper we discuss some local fixed point theorems of the Banach contraction principle which are adapted to provide local convergence theorems for Picard iteration in the class of Fredholm inegral equations of the second kind. Several examples are discussed.

References

[1] Ezquerro J. A. and Hernandez-Veron, M. A. On the application of some fixed-point techniques to Fredholm integral equations of the second kind, J. Fixed Point Theory Appl. (2024) 26:29 https://doi.org/10.1007/s11784-024-01119-6 [2] Granas, A.; Dugundji, J. Fixed point theory. Springer Monographs in Mathematics. Springer-Verlag, New York, 2003. [3] Rus, I. A.; Petruşel, A.; Petruşel, G. Fixed point theory. Cluj University Press, Cluj-Napoca, 2008.

ABSTRACT. Our aim is to present recent results regarding best proximity point theory. To arouse interest in this field we present recent applications of best proximity and we propose a new direction of study in the case of a cyclic operator.