ABSTRACT. Metric temporal equilibrium logic (MEL) extends temporal equilibrium logic (TEL) by incorporating quantitative timing constraints, enabling the specification and analysis of deadlines and durations. MEL is particularly suited for domains where time-bound properties are crucial, such as embedded systems, cyber-physical systems, and real-time software. It facilitates the precise expression of timing behaviors, such as the requirement that an event must occur within 5 milliseconds of a trigger, which often elude traditional qualitative temporal logics. In this paper, we present a Tseitin-like translation that maps any metric temporal formula into a logic programming fragment restricted to past operators. This translation provides a formal bridge to leverage existing Answer Set Programming (ASP) solvers for reasoning about metric temporal constraints. By restricting the target fragment to past operators, we enable more effective evaluation and integration with current ASP-based toolchains for multi-shot solving.

ABSTRACT. The development of temporal extensions to Answer Set Programming (ASP) has led to the emergence of linear-time (TEL), dynamic (DEL), and metric (MEL) temporal logics. However, the inherent rigidity of highly optimized ASP systems often hinders the rapid exploration and implementation of alternative logical designs. In this work, we propose a flexible meta-programming framework that operationalizes the semantics of varied temporal logics through a unified, declarative framework. Our approach extends standard ASP meta-programming by augmenting clingo’s theory grammar with formal type specifications and nesting capabilities. To ensure semantic correctness, we introduce a transformation pipeline that protects nested modalities from stable- model-based simplifications during grounding. We demonstrate the extensibility of our framework by implementing meta-encodings for TEL, MEL, and DEL. We provide a comprehensive account of TEL and highlight the key features for for managing the interval constraints of MEL and the Fischer-Ladner closure in DEL. Finally, we introduce the metasp system, a versatile tool that encapsulates workflow.

ABSTRACT. The Power grid is a critical infrastructure underpinning all aspects of modern society and its services. Maintaining its effectiveness requires continuous adaptations. In particular, addressing sustainability targets, demand patterns, and urbanisation trends requires implementing changes to the network. Actual developments can potentially span over a decade, with supply continuity and service quality that must be preserved throughout by ensuring conformance to several topological and combinatorial invariants. Long-term power grid planning deals with the above process, and although planning languages could be a natural choice, the kind of properties and invariants needed are cumbersome to express in such languages; on the contrary, they can be elegantly and succinctly encoded in Answer Set Programming (ASP). In this paper, we propose the first approach to automate and optimise the long-term power grid planning process using ASP. Experimental evaluations conducted on synthetic and real‑world grid data confirm the expressive power of the proposed ASP‑based approach and demonstrate its effectiveness.

ABSTRACT. We consider a fragment of Higher-Order Datalog with negation and argue that it generalizes the familiar and important fragment of Linear Datalog. We investigate the expressive power of this fragment, establishing a tight connection with the hierarchy of space complexity classes. In particular, we demonstrate that for all k >= 1, the (k+1)-order fragment of Stratified Linear Higher-Order Datalog$^\neg$ captures (k-1)-EXPSPACE. This result suggests that restricting programs to linear recursion shifts the expressive power of the corresponding fragments from time to space, generalizing the classical result that (Stratified) Linear Datalog captures NL. Unlike the first-order setting where an ordering assumption is required to capture NL, our results hold without any such assumption on the input database. The proof relies on simulating space-bounded Turing machines using Stratified Linear Higher-Order Datalog$^\neg$ programs and providing a space-efficient evaluation of the query program. We argue that identifying such computationally well-behaved fragments is a crucial step towards paving the way for practical implementations of Higher-Order Datalog.

ABSTRACT. In the field of static analysis of logic programs, the optimality of abstract operators is a valuable theoretical property, as it provides insight into the structure of abstract domains and the maximum precision that can be achieved. However, implementing optimal operators is often complex and may significantly impact performance, giving rise to a trade-off between precision and efficiency. We experimentally investigate this trade-off in the context of sharing and linearity analysis of logic programs. Our experiments build on previous work that proposed several optimal operators for unification and matching. We have implemented these abstract operators and the corresponding abstract domains within the PLAI analyzer, part of the CiaoPP preprocessor, and we report the impact of increasing operator precision on the accuracy and performance of the overall analysis.

ABSTRACT. In strongly-typed languages, types are verified at compile time, while dynamically typed languages, such as Prolog, perform type consistency checks entirely at run-time. Extending dynamic languages with assertions allows expressing both classical types and more general properties, providing high expressiveness, but at the cost of run-time overhead. Abstract interpretation allows safely approximating such program properties at compile time, which has been used to reduce the number of properties that require run-time checks, while still reporting unverified properties that can guide further static analyses, testing, or domain refinement. In this work, we first study how to selectively integrate the run-time semantics of assertion properties into a multivariant, top-down, goal-directed abstract interpretation algorithm. We then show how multiple inferred calling patterns can be exploited to reduce the number of properties that must be checked at run-time, thus minimizing the overhead. Finally, we report on an implementation of our approach in the Ciao system and provide performance results supporting that better results can be obtained than with the previously reported techniques.

ABSTRACT. Streamliner constraints reduce the search space of combinatorial problems by ruling out portions of the solution space. We adapt the StreamLLM approach, which uses Large Language Models to generate streamliners for Constraint Programming, to Answer Set Programming (ASP). Given an ASP encoding and a few small training instances, we prompt multiple LLMs to propose candidate constraints. Candidates that cause syntax errors render satisfiable instances unsatisfiable, or degrade performance on all training instances are discarded. The surviving streamliners are deployed in a parallel portfolio alongside the original encoding, ensuring correctness even if a streamliner is unsound. On three ASP Competition benchmarks (Partner Units Problem, Sokoban, Towers of Hanoi), the portfolio achieves speedups of up to 4-5x over the original encoding. Different LLMs produce semantically diverse constraints, not mere syntactic variations, indicating that the approach captures genuine problem structure.

ABSTRACT. The growing demand for Urban Air Mobility (UAM) introduces significant challenges in airspace management, particularly within densely populated metropolitan regions. As the number of aerial vehicles---such as drones, air taxis, and helicopters---continues to rise, so does the risk of mid-air collisions and conflicts with existing air traffic and obstacles. Ensuring safe and efficient UAM operations requires robust strategic deconfliction mechanisms. We propose an Answer Set Programming (ASP) based approach for strategic deconfliction, focusing on time synchronization and route optimization for conflict-free flight plans. The solution is benchmarked against Constraint Programming (CP), emphasizing scalability and resource use. Results show ASP offers faster execution and better scalability for small to medium cases, while CP maintains stable memory but degrades with complexity.

ABSTRACT. This article presents ASPIC, a new proof-of-concept library that converts extended syntax ASP-Core-2 programs to Picat predicates that can be solved right away with the integrated Picat SAT solver, or embedded in larger Picat programs (``ASP in Picat''), and that can in turn make use of various Picat predicates and functions (``Picat in ASP''). The first tests prove good compatibility with clingo (when the special Picat features are not used). With the embedded Picat, it touches the application field of clingcon as well, by being able to efficiently model with both ASP atoms and with finite domain variables, but goes beyond that by being able to model also non-linear constraints.

ABSTRACT. Answer Set Programming (ASP) is a declarative programming language used for modeling and solving complex combinatorial problems. It has been successfully applied to a number of different real-world problems. However, learning its usage can prove challenging as the declarative language, from a conceptual perspective, differs substantially from imperative programming, and programs are not required to adhere to any particular structure, offering arguably almost too much freedom for a beginner. Recently, a new methodology called Easy Answer Set Programming (Easy ASP) has been introduced that aims to aid in this learning process by focussing on a well-defined fragment of the ASP language and introducing additional structure to the programs. However, while this methodology can indeed be employed, to the best of our knowledge, no tool integrates its features currently. In this paper, we present EZASP, a Visual Studio Code extension designed to support the development of ASP programs following the Easy ASP methodology. It covers and extends the language fragment of Easy ASP and provides the user with warnings in the case of deviations from the methodology as well as the possibility to automatically reorder the program. Complementarily, it also adds syntax error highlighting, including detection of non-safe variables directly while editing, and configurability, as all features can be optionally disabled. A small user study in the context of university teaching suggests that these features are benefitial for both new and experienced users.

ABSTRACT. An effective examination and test schedule for patients plays a crucial role in hospital resource management. In this work, we formulate a new reactive patient-flow scheduling problem in multi-department hospitals where walk-in patients arrive over time and each patient requires multiple examinations per visit. Upon each arrival, the scheduler computes a feasible examination pathway---both the sequence of examinations and the room assignment---for the incoming patient only, while previously scheduled assignments remain fixed. This process is subject to medical precedence constraints and room capacity limitations. We model the problem declaratively in Answer Set Programming (ASP) with clingo, and optimize a two-part cost: travel time between consecutive examination locations and queue-induced waiting time, weighted by the duration of the upcoming examination. To assess robustness under stochastic service times, we propose a Discrete-Event Simulation (DES) evaluation layer and a baseline greedy policy for comparison. On large-scale synthetic datasets across various capacity regimes and patient loads, the ASP approach reduces median stay time and increases the proportion of zero-wait patients compared to DES-based baselines. These improvements are most pronounced under heavy load, while the approach still outperforms baselines across all capacity settings, with smaller gains at higher capacities.

ABSTRACT. Grounding, the translation of high-level models into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certified, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level specification and the solver's low-level input by introducing a novel certifying grounding framework for first-order logic model expansion (FOX) over finite domains. We present CertiFOX, a certified grounding framework consisting of: (1) a proof format for grounding derivations, (2) GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)—a new normal form designed for compact, domain-aware grounding—and (3) CheckFOX, an independent proof checker. Our approach guarantees that the grounder's output is equivalent to the input specification, setting the stage for trustworthy end-to-end certified solving pipelines for declarative languages. Experimental evaluation confirms that CertiFOX is a feasible approach. The GroundFOX grounder is competitive with other grounders, and proof checking with CheckFOX remains within a constant factor of grounding time.

ABSTRACT. We consider the problem of implementing deontic modal logic. We show how (deontic) modal operators can be elegantly and directly expressed using default negation (negation-as-failure) and strong negation present in answer set programming (ASP). We propose using global constraints of ASP to represent obligations, prohibitions, and permissions in deontic modal logic. We show that our proposed representation results in the various decades-old paradoxes of deontic modal logic being simply and elegantly resolved. Our method also serves as a means for modeling conditional obligations and conditional prohibitions in knowledge representation.

ABSTRACT. Abstract Interpretation infers and verifies program properties by over-approximating program semantics. It has been highly successful for (Constraint) Logic Programming, enabling the analysis of determinism, types, aliasing, costs, and its application in verification and program optimization. However, Abstract Interpretation has not yet been studied in the context of Goal Directed Answer Set Programming (ASP). In this work we take a first step in this direction. We present a top-down algorithm based in the PLAI fixpoint, implemented in the abstract interpreter of the Ciao Prolog Preprocessor, to perform abstract interpretation of goal-directed ASP. We also introduce the Shared-Constraints abstract domain, designed to capture potential relations among variables induced by constraints. Finally, we study the practicality of the approach in s(CASP) through three applications: detection of false odd loops over negation, efficient forall evaluation enabled by the Shared-Constraints domain, and abstract specialization (including the simplification of required global constraints). Our results show that compile-time static analysis can improve the evaluation of goal-directed ASP programs.