ABSTRACT. Strong equivalence between knowledge bases ensures the possibility of replacing one with the other without affecting reasoning outcomes, in any given context. This makes it a crucial property in nonmonotonic formalisms. In particular, the fields of logic programming and abstract argumentation provide primary examples in which this property has been subject to vast investigations. However, while (classes of) logic programs and abstract argumentation frameworks are known to be semantically equivalent in static settings, this alignment breaks in dynamic contexts due to differing notions of update. As a result, strong equivalence does not always carry over from one formalism to the other. In this paper, we carefully investigate this discrepancy and introduce a new notion of strong equivalence for logic programs. Our approach preserves strong equivalence under translation between certain classes of logic programs and both Dung-style and claim-augmented argumentation frameworks, thus restoring compatibility across these formalisms.

ABSTRACT. Refactoring is a common practice to improve code quality and maintainability while preserving external behavior. In Answer Set Programming, the anthem system supports this process by verifying the external equivalence of two encodings through a translation into first-order formulas, which are subsequently processed by automated theorem provers. However, while theorem proving is often successful for established equivalences, it frequently fails to terminate when programs are non-equivalent, leaving developers without actionable feedback during iterative refactoring. In this paper, we address this shortcoming by developing an approach for the automated generation of counterexamples for external equivalence. We extend an existing transformation for propositional programs to a first-order setting that covers a substantial subset of the clingo language, including non-tight encodings and recursive aggregates. Furthermore, we generalize the transformation to handle private predicates through a novel guess-and-check formulation. Our approach is implemented as an integrated component of the anthem framework, providing developers with concrete witnesses of non-equivalence to facilitate the rapid identification of logical flaws in ASP encodings.

ABSTRACT. Reinforcement Learning (RL) is a highly successful branch of machine learning for training an agent to maximize rewards in a given environment. RL comes in different incarnations and flavors, and is actively advanced. In the recent years, there has been increasing interest in using symbolic AI approaches, including Answer Set Programming (ASP), for improving the expected behaviour of RL trained agents, especially with regard to trustworthiness and guarantees.

In this talk, we review different usages of ASP for RL, where we put a focus on enforcing ethical behavior or norms based on deontic constraints that the agent should adhere to. Notably, such constraints can emerge after the training and require instant action, such as fixing the agent's policy for staying operational, and retraining the agent, possibly on the fly. Real-time requirements and large state spaces make this a challenging application domain for ASP, which needs to be addressed with further advancing ASP technology.

ABSTRACT. We present three problem-independent extensions to clingcon, a hybrid Answer Set Programming solver with finite-domain integer constraints, all operating through its order-literal interface: a theory-level heuristic directive providing declarative variable- and value-selection strategies, including a cooperative mode that defers variable choice to clasp’s VSIDS; a priority operator for minimize supporting lexicographic optimization via multi-shot or weighted single-shot strategies; and a bound-step option for linear, bisection, and hybrid bound-tightening in branch-and-bound search. Empirically, each extension delivers proven optima or strictly better incumbents on hard scheduling problems that the default configuration leaves unsolved. How much a problem benefits depends on how well a strategy fits its search structure, and a poor fit can turn an improvement into a regression.

ABSTRACT. Traffic signal optimisation is a key approach to urban traffic control and aims to mitigate congestion in urban areas by adjusting the green‑light durations of traffic signals. While prior work has shown the viability of Constraint Answer Set Programming (CASP) for this task, specifically with the system clingcon, limitations remain in terms of scalability and solution quality. In this paper, we extend the existing CASP-based approach by incorporating multi‑shot solving to enable incremental reasoning, together with two domain‑specific heuristics designed to guide the search more effectively towards high‑quality solutions. We evaluate our approach on real-world benchmark instances, including more challenging settings that were not addressed in previous work. Overall, our enhancements represent a substantial advancement over the previous clingcon encoding, both in terms of coverage and solution quality, and compare favourably to PDDL+ methods.

ABSTRACT. Translating natural language into formal knowledge representation languages such as Answer Set Programming (ASP) remains a challenging task, particularly with respect to faithful semantic interpretation and robust reasoning. Recent state-of-the-art approaches rely on large, resource-intensive Large Language Models (LLMs), thereby leaving the potential of smaller, more accessible models largely underexplored. In this paper, we investigate the use of compact, open-weight LLMs for this task. We build on prior NL2ASP work, where a transformer generates a controlled natural language (CNL) representation that is then translated into ASP. We replace the original components with fine-tuned small LLMs, and redesign the dataset to support a natural and realistic inputs. Our evaluation spans twelve lighweight models across three LLM families and compares two execution pipelines: one following the NL2ASP paradigm and one that bypasses the CNL intermediate representation. Results show that fine-tuned small LLMs consistently outperform the original NL2ASP approach, offering an effective and cheaper alternative to methods relying on larger, costlier models.

ABSTRACT. ASP Chef is a web platform in which Answer Set Programming (ASP) pipelines are composed by chaining ingredients, each encapsulating a distinct operation. Despite this pipeline paradigm, effective utilization still demands familiarity with both ASP and the available ingredient library. This paper presents two complementary extensions leveraging large language models to lower this barrier. The first extension is an advisory assistant that provides guidance in real time during recipe authoring. It employs a retrieval protocol to fetch ingredient documentation on demand, ensuring that the model remains contextually relevant while operating within tight token limits. This assistant is offered in two configurations: a local version leveraging WebGPU and the MLC framework for private inference directly on the device, and a remote version that connects to external providers such as Ollama or Groq for high performance reasoning. The second extension is an agentic interface via the Model Context Protocol (MCP), which exposes ASP Chef as a structured tool environment for external language model agents such as Claude and Copilot. A dedicated Python bridge maintains a live mirror of the active recipe, provides tools to inspect and manipulate the pipeline, and propagates all changes to the browser in real time via server sent events. Together, these two integrations successfully span interactive assistance during user authoring and fully automated pipeline construction and refinement driven by autonomous agents.

ABSTRACT. Large language models (LLMs) are often viewed as systems that reproduce existing patterns rather than generate new theoretical insights. Recent developments, however, suggest that when combined with formal verification, LLMs may assist in non-trivial theoretical exploration. In this paper, we investigate this possibility in the context of logic programming. Disjunctive logic programs (DLPs) are more expressive than normal logic programs (NLPs) but incur higher computational complexity. A classical research direction therefore seeks syntactically restricted subclasses of DLPs that can be transformed into semantically equivalent NLPs in polynomial time, such as head-cycle-free (HCF) programs via shifting. We present a case study in which LLMs are used as navigators to explore novel solutions. By challenging five state-of-the-art LLMs and rigorously verifying their outputs, we identify three previously unpublished subclasses of DLPs for which shifting preserves the stable model semantics. Beyond the specific subclasses obtained, this work demonstrates that LLM-assisted exploration, when paired with formal verification by humans, can support theoretical discovery in computer science and AI.

ABSTRACT. Large Language Models (LLMs) have demonstrated remarkable performance across a broad spectrum of tasks, including natural language understanding, dialogue systems, and code generation. Despite evident progress, less attention has been paid to their effectiveness in handling declarative paradigms such as Answer Set Programming (ASP), to date. In this paper we introduce BLAST: The first dedicated benchmarking methodology and associated dataset for evaluating the accuracy of LLMs in generating ASP code. BLAST provides a structured evaluation framework featuring two novel semantic metrics tailored to ASP code generation. The paper presents the results of an empirical evaluation involving ten well-established graph-related problems from the ASP literature and a diverse set of eight state-of-the-art LLMs.