View: session overviewtalk overview

10:10 | Intuitionistic Propositional Logic in Lean 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. |

10:30 | Unification in Matching Logic — Revisited 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. |

10:50 | Optics, functorially: Extended abstract PRESENTER: Silviu-George Pantelimon 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. |

11:20 | AR and VR for the Casa Romei Museum PRESENTER: Stefano Costantini 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. |

11:40 | A SERIOUS GAME TO LEARN DORIC GREEK ARCHITECTURE 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. |

12:00 | Level Generation Using ChatGPT: A Case Study on the Science Birds Game 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. |

12:20 | Graphic design for architectural serious games PRESENTER: Stefano Costantini 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. |

12:40 | Fostering Agentic Play Between Technology and Democracy 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. |

15:50 | A comparative analysis of Genetic Algorithms and NSGA-II on the Portfolio Optimisation Problem 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). |

16:10 | Assessing Features Importance in the 15-Class Galaxy Classification Problem 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. |

16:30 | Enhanced Anomaly Detection in Automotive Systems Using SAAD: Statistical Aggregated Anomaly Detection PRESENTER: Dacian Goina 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. |

17:30 | Generalized multisets over infinite alphabets with atoms PRESENTER: Andrei Alexandru 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. |