ABSTRACT. ASP(Q) extends Answer Set Programming (ASP) with Quantifiers over answer sets. In this paper we focus on the class of ASP(Q) programs with two quantifiers and weak constraints, denoted as 2-ASP(Q)^w. 2-ASP(Q)^w is a practically relevant fragment of ASP(Q) that is expressive enough to capture optimization problems up to the class \Delta^P_3. On the theoretical side, we provide a complete complexity characterization of the main computational tasks for 2-ASP(Q)^w programs, including tight completeness results and the analysis of nontrivial cases that have not been addressed in previous works. On the practical side, we introduce novel strategies for computing (optimal) quantified answer sets in the casper system, that rely on a Counterexample-Guided Abstraction Refinement (CEGAR) technique tailored to ASP(Q). An experimental evaluation on hard benchmarks from different application domains shows that the proposed techniques are effective in practice.

ABSTRACT. In this paper, we explore the concept of modularity in first-order answer set programming (ASP). We introduce a new formalism called parametric modular logic programs, which allows defining subprograms with parameters and intensionality statements. We demonstrate how this formalism can capture the semantics of clingo-programs with collective control, a feature that enables structuring and instantiating subprograms. We provide theoretical foundations for modular ASP, illustrate its usefulness, and connect to traditional non-modular ASP.

ABSTRACT. Constraint Answer Set Programming (CASP) is a hybrid paradigm that enriches Answer Set Programming (ASP) with numerical constraint processing, something required in many real-world applications. The usual specification of constraints in most CASP solvers is closer to the numerical back-end expressiveness and semantics, rather than to standard specification in ASP. In the latter, numerical attributes are represented with predicates, and this allows declaring default values, leaving the attribute undefined, making non-deterministic assignments with choice rules, or using aggregated values. In CASP, most (if not all) of these features are lost once we switch to a constraint-based representation of those same attributes. In this paper, we present the flingo language (and tool) that incorporates the aforementioned expressiveness inside the numerical constraints, and we illustrate its use with several examples. Based on previous work that established its semantic foundations, we also present a translation from the newly introduced flingo syntax to regular CASP programs following the clingcon input format.

ABSTRACT. The propositional abduction problem is a well-known form of non-monotonic reasoning where we are asked to find an explanation of a given manifestation. Recently, there has been an influx of results for other problems on not only finding one solution, but asking more refined questions on the solution space as a whole. For example, we might be interested in finding two solutions that are sufficiently far from each other (diverse solutions) in the solution space. In this paper we consider a related representation question where we ask if a given set of explanations S can represent any other explanation (whether their symmetric difference is smaller than a given k). We first study this problem from classical complexity and obtain a complete classification. While we only obtain a handful of tractable cases the blowup in complexity when compared to the classical abduction problem is often smaller than what one might expect. We continue with a parameterized complexity study (with several different parameters) and obtain new tractable and hard cases. Interestingly, a full parameterized complexity classification would simultaneously need to resolve the parameterized complexity of the covering radius problem from coding theory.

ABSTRACT. Inductive Logic Programming (ILP) originated within the Logic Programming community in the Nineties as a framework for combining symbolic learning with declarative knowledge representation. Nowadays, mature ILP frameworks exist that are capable of learning complex, non-monotonic hypotheses, thus broadening both the modeling capabilities and the scope of real-world applications of ILP. This work is primarily based on the FastLAS2 framework and aims to generate simple, interpretable hypotheses to help clarify the weather bulletins issued by OSMER FVG, the Regional Meteorological Observatory of the Italian region of Friuli Venezia-Giulia. In this paper we present a pipeline which, starting from simulated meteorological raw data and from OSMER's bulletin (used as ground truth) extracts data as ASP facts and generates ILP examples. From such examples an explanatory hypothesis is then inferred via FastLAS2. Such a hypothesis (translated into natural language) explains the weather forecast issued by human experts, and in particular the rationale behind experts’ choices of specific symbols in the bulletin pictogram (the symbol-annotated meteorological map of the forecast). The proposed approach is general, not specific to any particular region, it can equally be applied to bulletins from other sources and to different regions.

ABSTRACT. Neurosymbolic (NeSy) systems integrate neural networks with logical reasoning to achieve both generalization and interpretability, but recent work has shown they are susceptible to shortcut reasoning behaviors. We propose a novel method using matrix-based differentiable logic programming to mitigate reasoning shortcuts in two phenomena: \textit{constraint satisfaction shortcuts}, where constraints are satisfied without achieving the intended task, and \textit{cognition shortcuts}, where biased data leads to semantically incorrect concept mappings despite logically sound inference. Building on recent matrix-based logic programming semantics, we introduce design elements to mitigate shortcuts, including a unified encoding of rules and constraints in a single matrix. We also establish theoretical connections to fuzzy logic t-norms and empirically compare their gradient flow properties. Through carefully designed experiments on MNIST variants, we show that one-to-one grounding of neural outputs to logical atoms significantly reduces both shortcut types compared to previous methods that rely on soft probability distributions. We then confirm that architectural choices in coupling symbolic knowledge with neural learning play a critical role in shortcut mitigation.

ABSTRACT. We model in intuitionistic implicational logic the key enabler of today’s GenerativeAI: the next-token pre- diction in autoregressive causal neural networks. In our framework, next-token prediction corresponds to modus ponens, and sequence processing be- comes constructive proof extension under the Curry–Howard correspondence. Our Prolog-based special- ized theorem provers validate fundamental properties of the neural models, among which relations between commutative vs. non-commutative sequencing and single-token vs. multi-token prediction choices. We derive a neural architecture equivalent to multiplicative RNNs that arises naturally from a proof- theoretic interpretation of next-token prediction as nested intuitionistic implication and position the model relative to transformers, state-space models and recursive LLMs. Keywords: logic-based derivation of neural architectures, intuitionistic implicational logic, token-as- operator neural models, alternatives to transformer-based foundational models.

ABSTRACT. We present the interactions with a LLM (Large Language Model) aiming at proving that sqrt(2) is not a rational number in a LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system written by Robert Stark for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human readable. In our case study, we sketch in LPTP the usual proof showing the irrationality of sqrt(2). Then we describe the interactions we had with the LLM. We end up with a complete formal proof, partially generated by a LLM and fully proof-checked by LPTP.

ABSTRACT. The Single Constant Multiplication problem is a fundamental NP-hard optimization task in hardware design, which seeks to decompose a fixed constant using only additions, subtractions, and bit-shifts. Although dynamic programming methods can produce near-optimal SAT encodings for SCM, their encoding cost remains high for large constants. We propose a neuro-symbolic framework that accelerates SCM SAT encoding by identifying good rules for guiding operator selection during decomposition. Our approach employs a graph neural network model to predict promising operator types from constant decompositions, and exploits the resulting confidence scores to prune no-good choices in the symbolic search. Experimental results on unseen 17--32 bit constants demonstrate one to two orders of magnitude reductions in encoding time, over 97\% reduction in memory usage, and an order-of-magnitude decrease in branching, while preserving near-optimal encoding quality in terms of additions. These results show that learning-guided symbolic strategies can significantly improve the scalability and efficiency of SCM encoding. Our codes and data are public available at: https://github.com/Chufeng-Jiang/SCM_MLDP

ABSTRACT. The Traveling Salesperson Problem (TSP) is a very well-known problem in computer science. Many real-world instances belong to the class of Euclidean TSP, in which the nodes to be visited lie on the Euclidean plane, and additional information is available with respect to the generic TSP, i.e. the coordinates of the nodes to be visited are known. In previous publications, we showed that the additional available information can be exploited to speedup the search, both in Constraint Logic Programming (CLP) and in Answer Set Programming (ASP). Constraint Answer Set Programming is a framework that joins CLP and ASP, and it aims at combining the features of both languages. In this article, we address the (Euclidean) TSP in Constraint Answer Set Programming, and more specifically in the clingo[DL] language and solver. We propose new encodings for the TSP in clingo[DL]; the new encodings are applicable to the general TSP (also to instances which are not Euclidean) and show a speedup of several orders of magnitude with respect to previous encodings. A further speedup can be obtained in Euclidean instances by exploiting geometric reasoning.

ABSTRACT. From the moment of their inception, languages for relational data have been described as sublanguages embedded in a host programming language. Rel is a new relational language whose key design goal is to go beyond this paradigm with features that allow for programming in the large, making it possible to fully describe end to end application semantics. The core of Rel is Datalog with first-order queries in rule bodies; this is the principal relevance to ICLP. It is then extended with features that let it model the entire application semantics: variables that range over tuples and sets of tuples; abstraction, and application. With the new approach, we can model the semantics of entire enterprise applications relationally, which helps significantly reduce architecture complexity and avoid the well-known impedance mismatch problem. This paradigm shift is enabled by 50 years of database research, making it possible to revisit the sublanguage/host language paradigm, starting from the fundamental principles. The paper presents the main features of Rel: those that give it the power to express traditional query language operations and those that are designed to grow the language and allow programming in the large. The original paper on Rel appeared in SIGMOD 2025 under the title "Rel: A Programming Language for Relational Data". After receiving a SIGMOD Research Highlights Award, a shorter version under the current title was published in SIGMOD Record. For convenience we include this shorter version here. The URLs for the conference and the SIGMOD Record papers (both open access) are below: - https://dl.acm.org/doi/10.1145/3722212.3724450 - https://sigmodrecord.org/2026/04/01/relational-programming-in-rel Viktor Leis and Thomas Neumann wrote a short technical perspective on the paper: https://sigmodrecord.org/2026/04/01/technical-perspective-rel.

ABSTRACT. The extended abstract, for the recently published research track, introduces a novel approach to the Contrast Sequential Pattern Mining (CSPM) task, which is based on Answer Set Programming (ASP). The MASS-CSP framework provides a concise and versatile ASP encoding that addresses the basic CSPM task as well as several advanced extensions. The framework is implemented in two distinct phases: first, extracting frequent sequential patterns, and second, verifying if they satisfy specified constraints, such as the minimum support and contrast rate thresholds. The research demonstrates the power of ASP modelling features such as choice rules for pattern generation, integrity constraints for filtering, and aggregates for calculating the support of patterns. Furthermore, the framework addresses the practical challenges of Logic Programming, including the grounding phase, which can lead to memory explosion if not carefully managed. The practical utility of the framework is further validated by successfully identifying attack patterns in 4G-LTE cellular network logs, proving its effectiveness for anomaly detection and intrusion prevention.

ABSTRACT. Automating the translation of natural-language specifications into logic programs is a challenging task that affects neurosymbolic engineering. We present ASP-Bench, a benchmark comprising 128 natural language problem instances, 64 base problems with easy and hard variants. It evaluates systems that translate natural-language problems into Answer Set Programs (ASPs), a prominent form of logic programming. It provides systematic coverage of ASP features, including choice rules, aggregates, and optimization. Each problem includes reference validators that check whether solutions satisfy the problem specification. We characterize problems along seven largely independent reasoning aspects (optimization, temporal reasoning, default logic, resource allocation, recursion, spatial reasoning, and quantitative complexity), providing a multidimensional view of modeling difficulty. We test the benchmark using an agentic approach based on the ReAct (Reason and Act) framework, which achieves full saturation, demonstrating that feedback-driven iterative refinement with solver feedback provides a reliable and robust approach for modeling natural language in ASP. Our analysis across multiple agent runs enables us to gain insights into what determines a problem’s modeling hardness. -- This paper is to appear in the Proceedings of the 2nd International Workshop on Neuro-Symbolic Software Engineering (NSE 2026), affiliated with ICSE 2026. https://conf.researchr.org/home/icse-2026/nse-2026