17 research outputs found

    The Logic of Discrete Qualitative Relations

    No full text
    We consider a modal logic based on mathematical morphology which allows the expression of mereotopological relations between subgraphs. A specific form of topological closure between graphs is expressible in this logic, both as a combination of the negation ¬ and its dual , and as modality, using the stable relation Q, which describes the incidence structure of the graph. This allows to define qualitative spatial relations between discrete regions, and to compare them with earlier works in mereotopology, both in the discrete and in the continuous space

    A Theorem Prover Based Approach for SAT-Based Model Checking Certification

    No full text
    In the field of formal verification, certifying proofs serve as compelling evidence to demonstrate the correctness of a model within a deductive system. These proofs can be automatically generated as a by-product of the verification process and are key artifacts for high-assurance systems. Their significance lies in their ability to be independently verified by proof checkers, which provides a more convenient approach than certifying the tools that generate them. Modern model checking algorithms adopt deductive methods and usually generate proofs in terms of inductive invariants, assuming that these apply to the original system under verification. Model checkers, though, often make use of a range of complex pre-processing simplifications and transformations to ease the verification process, which add another layer of complexity to the generation of proofs. In this paper, we present a novel approach for certifying model checking results exploiting a theorem prover and a theory of temporal deductive rules that can support various kinds of transformations and simplification of the original circuit. We implemented and experimentally evaluated our contribution on invariants generated using two state-of-the-art model checkers, nuXmv and PdTRAV, and by defining a set of rules within a theorem prover, to validate each certificate

    Graph Granularity through Bi-intuitionistic Modal Logic

    No full text
    This thesis concerns the use of a bi-intuitionistic modal logic, UBiSKt, in the field of Knowledge Representation and Reasoning. The logic is shown to be able to represent qualitative spatial relations between subgraphs at different levels of detail, or granularity. The level of detail is provided by the modal accessibility relation R defined on the set of nodes and edges. The connection between modal logic and mathematical morphology is exploited to study notions of granulation on subgraphs, namely the process of changing granularity, and to define qualitative spatial relations between these “granular” regions. In addition, a special case of graph and hypergraph granularity is analysed, namely when the accessibility relation gives rise to a partition of the underlying set of nodes and edges. Different S5 extensions of intuitionistic modal logic are considered and compared in the thesis. It is shown that these logics, and their associated semantics, provide different ways of partitioning a graph, a hypergraph, or, more generally, a partially ordered set

    Frontiere educative e formative nei bambini e negli adolescenti di carta di Simona Vinci = Educational and self educational frontier's in simona vinci's children and adolescents

    No full text
    I romanzi di Simona Vinci si confrontano in modo inedito con il territorio dell’età bambina e adolescente, mettendo a nudo senza sconti, né riserve le frontiere della ricerca identitaria. L’autrice discende nelle profondità più tenebrose a cui conduce tale avventura iniziatica, misurandosi anche con le pieghe più fosche dell’itinerario educativo e formativo delle giovani coscienze alla prova del mondo. Proprio quelle soglie, che sono crepe in cui è necessario transitare per rinascere nella maturità, nel romanzo Dei bambini non si sa niente, si fanno baratro in cui precipita il microcosmo infantile di cinque bambini. Con l’irruzione della logica adulta e delle sue perversioni, essi resteranno inghiottiti in quello squarcio che da frontiera diviene voragine.Simona Vinci's novels are confronted in an unprecedented way with the territory of the child and adolescent age, exposing unreservedly the frontiers of identity research. The author descends into the darkest depths to which this initiatory adventure leads, also measuring herself with the most sinister folds of the educational and training itinerary of young consciences. Precisely those thresholds, which are cracks through which it is necessary to pass in order to be reborn into maturity, in the novel Dei bambini non si sa niente, become an abyss into which the infantile microcosm of five children falls. With the irruption of adult logic and its perversions, they will remain swallowed up in that gash, which is no longer a border but a chasm

    Axiomatizing Discrete Spatial Relations

    No full text
    Qualitative spatial relations are used in artificial intelligence to model commonsense notions such as regions of space overlapping, touching only at their boundaries, or being separate. In this paper we extend earlier work on qualitative relations in discrete space by pre- senting a bi-intuitionistic modal logic with universal modalities, called UBiSKt. This logic has a semantics in which formulae are interpreted as subgraphs. We show how a variety of qualitative spatial relations can be defined in UBiSKt. We make essential use of a sound and complete axiomatisation of the logic and an implementation of a tableau based theorem prover to establish novel properties of these spatial relations. We also explore the role of UBiSKt in expressing spatial relations at more than one level of detail. The features of the logic allow it to rep- resent how a subgraph at a detailed level is approximated at a coarser level

    Il Preside Vito Mercadante. Un pioniere dell’educazione alla legalità nella scuola siciliana del secondo Novecento

    No full text
    Vito Mercadante was headmaster at two mafia-dense schools: Montelepre and Palermo. A man of multifaceted interests, he was first and foremost an educator, a promoter of many initiatives aimed at building an anti-Mafia culture in Palermo's schools. He understood that in order to achieve genuine democracy in Sicily, it was necessary to study the mafia phenomenon from its origins and counter the ‘disvalues’ of the mafia subculture with targeted educational practices. The author of many letters published in newspapers, books of fiction and essays on the mafia, his commitment was constantly directed towards the school as a laboratory of education to legality where to transform the living conditions of the humble and create a more just society

    Expressing discrete spatial relations under granularity

    No full text
    The logic UBiSKt is a bi-intuitionistic modal logic with universal modalities having a semantics in which formulae are interpreted as subgraphs. We use the logic to formalize the idea of looking at subgraphs at different levels of detail. We show how the logic can be used to define various spatial relations between subgraphs. These relations are considered with respect to change in level of detail. We use an existing formulation of generalized partitions on graphs and hypergraphs in terms of relations to give a novel generalization of the classical modal logic S5 to a bi-intuitionistic modal logic we call UBiSKtS5

    L’isola che non c’è: storia della scuola di Carloforte tra Otto e Novecent

    No full text
    Carloforte è l’unico comune di San Pietro, una piccola isola della Sardegna sudoccidentale. Se geograficamente la località è sarda, da un punto di vista culturale e linguistico non lo è: nel 1738 sull’isola si insedia una comunità connotata da una forte autonomia culturale di matrice ligure, che parla una lingua diversa dal sardo, che non rinuncerà mai alla propria identità culturale, linguistica e imprenditoriale. La distruzione dell’archivio comunale di Carloforte nel 1955 a causa di un incendio rende difficile la ricostruzione della storia della sua scuola elementare. È stato però possibile ricostruirne l’organigramma nel 1916 attraverso la documentazione conservata presso l’Archivio comunale di Oristano e, di conseguenza reperire i fascicoli personali degli insegnanti nel fondo Provveditorato dell’Archivio di Stato di Cagliari. La documentazione prodotta dal comune di Carloforte, dai maestri e dagli ispettori scolastici permette quindi una riflessione storica sulla scuola locale tra Otto e Novecento. Nell’articolo si prova a ricostruire una storia che si pensava impossibile, per una località che è dentro i confini geografici della Sardegna, ma è fuori dai confini della cultura sarda; un comune di frontiera per la sua posizione, ma florido e integrato nell’economia non solo isolana

    Combination of novel systemic agents and radiotherapy for solid tumors – part I: An AIRO (Italian association of radiotherapy and clinical oncology) overview focused on treatment efficacy

    No full text
    Over the past century, technologic advances have promoted the evolution of radiation therapy into a precise treatment modality allowing for the maximal administration of dose to tumors while sparing normal tissues. In parallel with this technological maturation, the rapid expansion in understanding the basic biology and heterogeneity of cancer has led to the development of several compounds that target specific pathways. Many of them are in advanced steps of clinical development for combination treatments with radiotherapy, and can be incorporated into radiation oncology practice for a personalized approach to maximize the therapeutic gain. This review describes the rationale for combining novel agents with radiation, and provides an overview of the current landscape focused on treatment efficacy
    corecore