This paper introduces ALIGHIERoo (Advanced Literary and Iconographic Graph for Hermeneutics of Interconnected Editions and Resources - object-oriented), an ontological framework currently under development within the Naples Dante Project. Drawing upon CIDOC CRM and LRMoo, ALIGHIERoo focuses on the representation of intricate textual and iconographic elements within Dante's Commedia, though it aims for a high level of scalability. By prioritizing semantic granularity and inferential reasoning, ALIGHIERoo is envisioned as a versatile and expandable framework for digital philology and heritage studies. The project constitutes a structured proposal for future refinement and collaborative validation.
We present a proof search procedure for the minimal coreflection logic iCK4, an intuitionistic modal logic with the normality axiom and the coreflection principle. The procedure is based on a sequent calculus Gbu-iCK4 that ensures strong termination of backward proof search. Gbu-iCK4 is shown to be complete via a dual refutation calculus that enables the extraction of countermodels when the proof search fails. To support practical experimentation, we provide an implementation of the proof search and the countermodel extraction procedures.
Urban Air Mobility (UAM) promises to revolutionize transportation in metropolitan areas by introducing "air taxis" for passenger and cargo transport. However, the envisioned dense operations of UAM vehicles in lowaltitude airspace pose unprecedented challenges for air traffic management (ATM). The Strategic Deconfliction (SD) problem in UAM is about designing the pre-flight "air traffic plan" for potentially hundreds or thousands of simultaneous urban flights, allocating routes, times, and resources in a way that guarantees separation and operational feasibility before any aircraft even leaves the ground. This short paper presents an approach based on Answer Set Programming (ASP) to solve the SD problem in UAM and reports preliminary results on a use case. In particular, the modelling choices will be described with regard to the air network topology, the fleet of drones to be scheduled and the SD problem.
This paper investigates the evolution from a medical appointment scheduling framework based on Answer Set Programming (ASP) integrated with Blueprint Personas to a more cognitively rich, agent-based scheduling system employing the L-DINF epistemic logic framework. We illustrate how agent-oriented models incorporating beliefs, intentions, and dynamic reasoning capabilities can effectively enhance or replace the persona-based constraint optimization traditionally used. Key advantages of the L-DINF model, such as improved adaptability, enhanced explainability, and more human-like decision-making, are emphasized. Furthermore, a structured translation methodology from static personas into dynamic epistemic agents is proposed, accompanied by a modular logical architecture supporting real-time, responsive scheduling.
Large Language Models (LLMs) have shown impressive capabilities but still struggle in reasoning. Even with advanced prompting techniques such as Chain-of-thought, they often make reasoning mistakes. A recent approach to overcome this difficulty consists in integrating an LLM with an external reasoner, realizing a form of neuro-symbolic integration. The LLM in this case is used to translate the multi-modal unstructured description of the problem (text, images) into a formal representation, often based on logic, which is then provided to the reasoner that computes the answer. Closed source models such as ChatGPT 4o have impressive performance for this task but they are expensive and require the data to be uploaded in the cloud, which poses privacy problems. In this paper we investigate the performance of smaller open source models on the problem of describing images using Prolog facts, to be used by a downstream reasoner.
This paper presents our work in progress about the integration of Probabilistic Logic Programming (PLP) with Declarative Process Mining (DPM) to address uncertainty in business process management. Traditional DPM approaches, such as DECLARE, use deterministic constraints to permit/forbid activities, but real-world processes often involve incomplete or unreliable data. To bridge this gap, we recap our previous work on introducing in a separate way probabilistic extensions for events, traces, and constraints inspired by PLP's Distribution Semantics. We present here an extension to our formal semantics to take into account at the same time uncertain events and uncertain constraints in order to perform compliance of a trace versus a process model. Preliminary experiments on a healthcare process demonstrate the approach's feasibility but highlight scalability challenges due to exponential complexity, that will be addressed in future work.
We present a novel methodology for extracting and interpreting feature interactions from tree-based machine learning models using logic programming. While traditional machine learning techniques often act as black boxes, offering limited insight into the role of individual features in classification outcomes, our framework leverages the inherently explainable nature of Answer Set Programming (ASP) to investigate the dependencies among features encoded in decision structures. Rather than extracting explicit rules, we employ an arc-consistency-like reasoning mechanism to constrain feature values in a way that explains the classification in a symbolic and interpretable form. Our approach preserves the original predictive accuracy, while significantly enhancing transparency. We demonstrate the effectiveness of the method on the task of classifying malicious Portable Executable (PE) files, a challenging domain for explainability due to the opaque and low-level nature of its input features. Experimental results highlight the potential of our ASP-based framework to advance explainable AI in cybersecurity contexts.
This paper explores the integration of the Digital Twins Definition Language (DTDL) with ASP Chef, a web-based platform for Answer Set Programming (ASP). The goal of the research is to take advantage of the capabilities of ASP Chef to query, analyze, and visualize digital twins. As a first step in this direction, we introduce a method for mapping DTDL-defined digital twin models into ASP facts. This approach enables a seamless transition from high-level digital twin specifications to declarative reasoning and interactive visualization, offering a flexible framework for interpreting and exploring digital twin configurations.
It has long been established that the set Th of theorems in an axiomatic formal theory is recursively enumerable (r.e.). Building upon the Davis-Putnam-Robinson-Matiyasevich theorem, which states that every r.e. set is Diophantine, this paper explores the complexity of representing Th through a Diophantine equation D - 0. We contend that a good trade-off between two primary measures of the complexity of the representation, which are the number of unknowns and the degree of the polynomial D, should aim at the transparency of the representation. Our work builds on a previous construction, notably that of M. Carl and B.Z. Moroz, who have provided a Diophantine representation of the sentences provable in the Godel-Bernays class theory (NBG) within first-order predicate calculus. In contrast, our Diophantine representation of NBG relies on a modernized version of Schroder's algebra of relations, specifically the L-x equational calculus proposed by A. Tarski and S. Givant. Additionally, we replace NBG's traditional axioms with an alternative axiomatization by H. Friedmann. These changes reduce the complexity of the Diophantine representation of NBG's provability, while maintaining equivalence to more classical formalizations. While we provide only preliminary insights into this novel equational axiomatization, we report on initial experiments with these axioms using the Vampire theorem prover.
The Nurse Scheduling Problem (NSP) is a well-known combinatorial optimization problem with significant practical implications in healthcare workforce management. In this paper, we investigate the use of Answer Set Programming (ASP) to model and solve realistic nurse scheduling scenarios in two Italian healthcare institutions: the Mariano Santo and the Annunziata hospitals. We design ASP encodings capable of handling both general and institution-specific constraints, including shift coverage requirements, rotation rules, and personal unavailability. We analyze the impact of solver configurations and optimization strategies, comparing the performance of clingo and wasp across multiple solving modes. Our experimental results show that unsatisfiable core-based strategies are able to find optimal solutions for the tested instances within a few seconds.
We present a tool generating and executing logical tests of the same kind of those administered by the Italian Universities for a sort of admission tests. They are developed by CISIA, usually referred to as TOLC. A set of benchmarks drawn from official repositories has been encoded into ASP and the solutions have been verified. Other tests have been invented starting from them and checked in ASP. Tests have been then parametrized with names of people involved, actions, environments, and so on. This way an exponential number of different tests, w.r.t. the initial collection, can be obtained, basically with random grounding, and their solutions verified by ASP. Furthermore, a set of explanations of why an answer is wrong has been added for didactical purposes. The tool has been tested with students of the first year of the Degree in Computer Science.
In Artificial Intelligence, defeasible reasoning has been studied as one of the key features of common-sense reasoning and consequently various kinds of non-monotonic logics have been developed to model it formally. We recently developed a non-monotonic logic in the Description Logic (DL) framework based on a combination of ideas from prototype theory, weighted DLs (aka "tooth logic"), and earlier work on justifiable exceptions. A central ingredient in the new framework is the notion of a prototype description, weighted characterisations of concepts denoting the typical features of its members. In this paper, we develop an initial ASP translation for this system which allows to reason on instance level queries in the preferred models of a knowledge base. In particular, under reasonable conditions on the form of the input knowledge base, we show that preference reasoning on answer sets can be encoded via standard ASP constructs. We show that the translation is complete with respect to the preferential semantics of our system.
We study the verification of coverability for Positive Interactive Datalog Programs (posIDP), a fragment of Communicating Datalog Programs (CDPs) where the programs are positive, i.e., make no use of negation. CDPs are a message passing system model grounded in logic programming, where nodes update their configuration by running a Datalog(not equal) program while sharing database tuples and receiving information from external services and/or users. While CDP verification has been extensively studied in the last few years, studies on CDP formal verification disregarded the role of negation in the node programs. In this paper, we study the impact on verification of positive programs when no meaningful use of negation is made. We show that the coverability problem remains undecidable despite the monotonicity of Datalog. We discuss the results in the framework of the Well Structured Transition System theory, motivating the introduction of novel semantics for data-aware processes that arguably enjoy better verification properties.
Research related to automated contradiction processing is a hot topic in several scientific communities. Many solutions offer limited explainability due to the exclusive usage of neural models or machine learning approaches. Also, although reproducibility can be achieved by controlling randomness in these models, their inherent complexity and lack of transparency often hinder adoption in domains that require high levels of determinism and some elaboration tolerance. This problem can be addressed with the introduction of neuro-symbol approaches, where part of the problem can be solved by exploiting logical formalisms. In this paper, we propose a neuro-symbolic pipeline whose purpose is to identify simple contradictions within sentences expressed in natural language. The contribution of the non-explainable side of the pipeline is confined to the conversion from natural language, and to the extraction of commonsense knowledge, while reasoning and knowledge derivation is delegated to a symbolic reasoner based on Answer Set Programming. We describe the proposed architecture and present a simplified implementation. We then report about early experiments.
Deep learning models excel in complex classification tasks but often lack interpretability, limiting their adoption in domains where explainability is critical, such as medicine and veterinary science. This work presents a hybrid approach that combines deep learning and symbolic reasoning to classify bull spermatozoa morphology in an explainable manner. We utilise YOLOv8 for object detection and morphological and viability classification of bull's spermatozoa from microscope-acquired images, achieving high accuracy. To tackle explainability, FastLAS was employed to learn human-readable classification rules. These rules, coupled with the xASP2 framework, enable traceable justifications for each classification, addressing the black-box nature of deep learning. Experimental evaluation demonstrates that, while FastLAS does not match YOLO's performance, it outperforms traditional machine learning models and offers significant benefits in explainability. This approach provides a practical solution for integrating explainable AI in reproductive biology, with implications for medical AI systems where transparency is essential.
The Stable Marriage Problem (SMP) consists of finding a stable matching between two equally sized disjoint sets, typically referred to as men and women, based on individual preference lists. A matching is stable if no man and woman prefer each other over their assigned partners. The Gale-Shapley algorithm is the classical polynomial-time solution to this problem. In Constraint Programming (CP), the Stable Marriage Constraint (SMC) encapsulates this problem as a global constraint, with a consistency-enforcing propagator derived from an extended version of the Gale-Shapley algorithm. In this paper, we present a GPU-accelerated propagator for the SMC and its integration into a CP solver. Experimental results against the sequential version demonstrate the potential of GPU acceleration in handling large instances of the stable marriage constraint.
In this work we present a tool for the automatic attribution of emotions to astronauts speeches obtained from the NASA Mission Transcript Collection. While, at the current state of affairs, we do not have yet a quantitative evaluation of such tool, we present - as a proof of concept - some qualitative analysis showing the potential usefulness of our approach. The broader objective of this work is providing an intelligent system for monitoring the psycho-physical condition of an astronaut during an aerospace missions. This system exploits a commonsense reasoning framework based on the logic T-CL, a probabilistic extension of Description Logics of typicality able to deal with the conceptual combination of prototypical descriptions, i.e. commonsense representations of given concepts. Starting from an ontological formalization of emotions based on the Plutchik model, known as ArsEmotica, the system exploits the logic T-CL to automatically generate novel commonsense semantic representations of compound emotions (e.g. Love as derived from the combination of Joy and Trust according to Plutchik). The generated emotions have then been applied for emotion attribution in the context of aerospace missions, in order to classify transcriptions of astronaut's speeches in the corresponding emotions.
Hilbert's epsilon-operator, a foundational device for forming indefinite descriptions, has long been overshadowed by standard quantifiers in first-order logic. However, its capacity to eliminate quantifiers and reframe logical derivations makes it a compelling tool for alternative proof strategies and automated reasoning. This paper revisits the epsilon-calculus, offering a streamlined proof of completeness adapted from Hasenjaeger's 1953 approach. Building on earlier work by Leisenring, Davis, and Fechter, we present a variant of the epsilon-calculus that omits all predicate symbols aside from equality. The development follows the conventional structure of logical systems-syntax, semantics, and deductive calculus-culminating in a soundness and completeness result. The aim is to reaffirm the epsilon-operator's relevance in the foundations of logic through a simplified and accessible formal treatment.
Visualizing security policies is no easy task, especially when they come from the labyrinthine world of SELinux. In this article, we explore how ASP Chef, a logic programming platform for structured reasoning and templated output, can be enhanced with tree visualization capabilities via the integration of the ApexTree framework. By introducing a new tree/2 functor within the Mustache-based templating system of ASP Chef, we enable logicbased generation of structured tree data, seamlessly translatable into the JSON format of ApexTree. As a concrete and security-relevant use case, we focus on SELinux policy rules, which define access control through 4-tuples of subjects, objects, classes, and permissions. We demonstrate how to extract, filter, and interpret meaningful fragments of these policies using ASP and Lua scripting within ASP Chef. Nodes and links are programmatically generated to construct readable trees, enabling intuitive inspection of policy paths from user roles to allowed actions. We further enhance interpretability by integrating LLMs into the workflow, automatically generating natural language descriptions of the policy logic. The result is an expressive and interactive visualization of SELinux permissions.
Water quality monitoring is a critical task in environmental protection and climate change adaptation. In this paper, we present the use of ASP Chef, a lightweight web-based environment for exploring and transforming ASP answer sets, in the context of the Tech4You project. ASP Chef enables intuitive pipelines over arrays of interpretations, supporting data-driven analysis without requiring low-level programming or complex tooling. Inspired by CyberChef, ASP Chef has recently been extended with a novel mechanism for content generation based on Mustache templates. This feature allows answer sets to be transformed into JSON and other structured formats, enabling seamless integration with JavaScript-based visualization frameworks such as @vis.js/Network, Tabulator, and ApexCharts. We demonstrate how ASP Chef is used to visualize and analyze water quality data collected by multisensory buoys, which monitor a wide range of chemical and physical parameters. Raw data is preprocessed using Python libraries such as NumPy, Pandas, and TensorFlow for cleaning and neural network-based modeling. Selected portions of the cleaned data are then explored via ASP Chef recipes, launched directly through dumbo-asp, a tool that opens the browser and executes the recipe with the given input. Our results show that ASP Chef enables effective visual exploration of parameter trends, detection of critical values through logic queries, and the creation of interactive dashboards for domain experts. This work illustrates how declarative logic programming can be combined with modern front-end technologies to build practical tools for environmental monitoring and decision support.
