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.
