ABSTRACT. Reinforcement Learning (RL) enables autonomous agents to learn policies from experience, but realistic problems often involve enormous state spaces, making learning and generalisation challenging. Abstraction and approximation are therefore essential. Relational Reinforcement Learning (RRL) offers a way to reason about objects and their relations, and the CARCASS framework by Martijn van Otterlo demonstrates how logical representations can model Markov Decision Processes (MDPs) in first-order domains. Originally implemented in Prolog, CARCASS leverages domain knowledge to create powerful abstractions. We explore Answer-Set Programming (ASP), which is a rich and, contrary to Prolog, fully declarative modelling language, to realise CARCASS abstractions. We evaluate our ASP-based implementation in case studies of two domains, viz. Blocks World and Minigrid. Our results indicate that CARCASS with ASP provides a promising approach to constructing abstractions for RL, especially when domain knowledge is available.

ABSTRACT. Large Language Models (LLMs) have recently been adopted for semantic data extraction and parsing from unstructured text, enabling the generation of candidate relational facts from natural language. However, while LLMs are effective at extraction, they are not reliable solvers of complex combinatorial reasoning tasks or global consistency constraints, and logic-based extraction pipelines often require issuing multiple queries while coping with incomplete or spurious outputs. In this paper, we propose a logic-guided data extraction framework that combines LLM-based extraction with Answer Set Programming (ASP), delegating fact extraction to the LLM and all validation, inference, and control to ASP, which plays an active role in structuring and guiding the extraction process. In contrast to baseline pipelines that invoke the LLM independently for all target predicates, our approach uses ASP reasoning to determine which predicates are logically admissible at each stage, thereby guiding the selection of extraction queries. The framework interleaves LLM calls with ASP reasoning and derivation, allowing logically implied facts to be inferred without additional extraction and enabling early consistency checks. We formalize the proposed pipeline and show that, under mild assumptions on the extraction oracle, it is equivalent to the baseline approach in terms of the final extracted facts, while reducing the number of LLM calls. We further introduce a caching mechanism for logic-based control queries, exploiting monotonicity properties of conjunctive queries over incrementally constructed fact sets to reduce the number of solver invocations. An experimental evaluation on benchmarks derived from standard Answer Set Programming domains shows that the proposed framework substantially reduces the number of LLM calls and, in practice, improves extraction quality by mitigating spurious outputs. These results demonstrate the effectiveness of using non-monotonic logic programming as a control mechanism for semantic data extraction from text.

ABSTRACT. Neurosymbolic AI combines neural networks with symbolic programs to create robust and explainable predictions. One such framework is NeurASP, which trains a neural network to predict concepts and reasons over them using rules written in answer set programming (ASP) to solve downstream tasks. Crucially, labels are only provided for the downstream prediction produced by the symbolic rules, not for the latent concepts themselves. Backpropagation through the non-differentiable ASP component requires expensive probability and gradient calculations, which has hindered scalability to more sophisticated tasks. In this paper, we address the current limitations of NeurASP by improving its computational performance through vectorization, batch processing and caching of intermediate computations during training. We compare computation speeds between the original and our new implementation of NeurASP and report speedups of multiple orders of magnitude for larger tasks. To this end, we propose a new dataset of difficult tasks involving playing cards, which we use to test the capabilities of NeurASP's enhanced learning function.

ABSTRACT. Generating accurate and executable code using Large Language Models (LLMs) remains a sig- nificant challenge for underrepresented programming languages, such as Prolog and Lisp, due to the scarcity of public training data compared to high-resource languages like Python. This pa- per introduces a generalizable Reinforcement Learning (RL) approach that combines small-scale versions of the Qwen2.5-Coder model with Group Relative Policy Optimization (GRPO) to en- able effective code generation through reasoning. To address the limitations of sparse datasets, we integrate execution-driven feedback directly into the RL loop, utilizing a reward system that exploits both logical correctness and structural formatting. Experimental results on GSM8K dataset demonstrate significant improvements in reasoning quality and code accuracy across underrepresented languages. These findings underscore the potential of our approach to bene- fit a wide range of programming languages lacking extensive training resources by leveraging symbolic reasoning and interpreter-based feedback.

ABSTRACT. One of the most significant achievements of equilibrium logic was the characterization of strong equivalence, a property crucial for program transformation and optimization in Answer Set Programming (ASP). While ASP has recently been extended to a higher-order setting to enhance its expressive power, the lack of a comparable purely logical foundation has made verifying strong equivalence for higher-order programs or even proving the correctness of simple program transformations, a difficult challenge. This paper addresses this gap by developing a logical semantics for higher-order ASP by extending the equilibrium logic framework. Within this extended framework we demonstrate that every stratified higher-order logic program possesses a unique equilibrium model. Moreover, we establish definability results demonstrating that the syntax of our higher-order language is sufficiently expressive to capture its semantic domains. Finally, and most importantly, we generalize the classical theorem of strong equivalence to the higher-order setting: we prove that two programs are strongly equivalent if and only if they share the same higher-order models.

ABSTRACT. The Event Calculus (EC) implemented in answer set programming (ASP) has proven suitable for specifying requirements put on safety-critical systems thanks to its elegant representation of both discrete and continuous changes and its semantic closeness to semi-formal natural language. However, continuous changes and the size (and possible unboundedness) of value domains of time and various system properties (fluents) pose significant challenges. Grounding-based ASP solvers, such as clingo, which only implement Discrete EC (DEC), lead to combinatorial explosion in program size as well as inaccuracies in the representation. On the other hand, the grounding-free s(CASP) does not discretize but struggles with non-termination due to its top-down execution. In this paper, we introduce Hybrid EC, an extended axiomatization of DEC, that tackles the challenges via so-called functional fluents and a mapping of time to abstract steps. We implement it using clingcon and clingo-lpx (Hybrid ASP systems over integers and rationals, respectively) where the (dense) value domains of fluents and time are represented as linear constraints and evaluated by external solvers, while ensuring termination whenever solutions exist. We validate both implementations on a number of examples and observe that, unlike clingo, they are indeed unaffected by the size of the domains and that handling rationals instead of integers does not impact scalability. Most importantly, the ability of clingo-lpx to handle dense domains enables accurate modeling of examples involving continuous change.

ABSTRACT. Grassroots platforms are distributed systems with multiple instances that can (1) operate independently of each other and of any global resource other than the network, and (2) coalesce into ever larger instances, possibly resulting in a single global instance. Here, we present Grassroots Logic Programs (GLP), a multiagent concurrent logic programming language designed for the implementation of grassroots platforms. We introduce the language incrementally: We recall the standard operational semantics of logic programs; introduce the operational semantics of Concurrent (single-agent) GLP as a restriction of that of LP; recall the notion of multiagent transition systems and atomic transactions; introduce the operational semantics of multiagent GLP via a multiagent transition system specified via atomic transactions; and prove multiagent GLP to be grassroots. The accompanying programming example is the grassroots social graph---the fundamental grassroots platform on which all others are based. With the mathematical foundations presented here: a workstation-based implementation of Concurrent GLP was developed by AI, based on the operational semantics of Concurrent GLP; a distributed peer-to-peer smartphone-based implementation of multiagent GLP is being developed by AI, based on the operational semantics of multiagent GLP; a moded type system for GLP was implemented by AI, to facilitate the specification of GLP programs by human and AI designers, for their programming by AI; all reported in detail in companion papers.

ABSTRACT. Event-B is a formal method rooted in predicate logic and set theory. We encoded its over 600 proof rules in Prolog enabling a systematic, comprehensible proof analysis and construction. By integrating the proof rules into the Prolog-based validation tool ProB, we can bring the proof rules to life and obtain an interactive proof system with proof tree visualisation. This has advantages in teaching, enabling students to precisely control the application of proof rules. Our tool can import proof obligations from the Rodin platform and provides multiple exports: a trace file for proof replay in ProB, an interactive HTML document for tool-independent exploration of the proof tree, and an export back to Rodin, allowing the ProB prover to be used as second chain. Compared to the previous implementation of the proof rules in Java, the encoding in Prolog is much more compact, maintainable and extensible. In future we also hope to obtain fast automatic provers; a preliminary iterative deepening prover with simple heuristics is already available and useful for finding short proofs.

ABSTRACT. ProB is a Prolog-based model checker, animator and constraint solver for high-level formal spec ifications. It can also be used to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the existing features of ProB’s Prolog animation mode and its recent extensions. The extended capabilities include sim ulation for statistical checks, more reliable trace replay, transitions with user input and improved state visualisation. We apply the new features to case studies, particularly for evaluating different strategies in game play, such as Connect Four. The features are useful for many other applications, especially for ProB’s new sequent prover for Event-B proof obligations, as well as for demonstration models for teaching in combination with interactive visualisation.

ABSTRACT. Automated feedback tools for logic programming education depend on realistic bug datasets that reflect the mistakes students actually make. However, existing mutation testing frameworks for Prolog treat all mutations as equally likely, producing synthetic faults that diverge from classroom reality. We present an empirical study of 7,201 Prolog submissions from 265 undergraduate students, from which we derive a fine-grained taxonomy of student bugs through manual classification of 200 bug-fixing submissions. Guided by this taxonomy, we develop a data-driven mutation tool whose 17 operators are weighted according to the observed error distribution. The tool enumerates valid mutation sites on the abstract syntax tree, samples operators proportionally, injects faults, delegating to an SMT-based synthesizer when new code fragments are needed, and validates each mutant against a reference test suite. An evaluation of 16,000 generated mutants shows that the synthetic error distribution closely matches the student distribution, with most bug categories agreeing to within two percentage points. We identify cut-related mutations and synthesizer-generated code as the main sources of residual divergence, and outline how combining the SMT back-end with a language model fine-tuned on student code can further improve realism.

ABSTRACT. Providing personalized feedback is essential for effective learning, but delivering it promptly can be challenging in large-scale courses. In this work, we present ProHelp, an automated assessment platform for Prolog built on top of the GitSEED framework, and we evaluate it through a survey of 144 students from a 365-student undergraduate logic programming course. We assessed the perceived usefulness of seven types of automated feedback, including automatic testing, predicate scoring, syntax error highlighting, open choice point warnings, score rankings, solution type validation, and unknown predicate name suggestions. Our results show that 74% of students agreed the feedback helped increase their grade, and the system achieved a System Usability Scale score of 78.5 (grade B+). Among the feedback types, automatic testing was ranked as the most useful, followed by open choice point warnings and predicate scoring, with statistically significant differences. We found no significant effect of students' interest level, engagement with optional exercises, or use of large language models on their perception of feedback usefulness. We also explore student preferences for future feedback features, finding a significant preference for showing the differences between generated and expected test outputs.

ABSTRACT. Chess is a two player strategic game that is embedded in classical AI culture as it was once the frontier for intelligent behaviour. There was the silent assumption that the advent of computer engines that play better than the best humans will extinguish interest in the game. However, the opposite has come to pass, with a growing following for the game. A lot of the computational resources are now centered around training of players, where the engine output is just one aspect. Access to past games is also an essential part, both in knowing what games a specific player has played previously, and also which continuations at a certain position have led to victory more often for each of the two colour players. We present chess db a suit of logic programming tools that can effectively manipulate games both in memory and via creating back end databases. In particular, we provide versatile code that creates databases from PGN game files and explore the suitability of open source key-value databases for storing position tables that provide near- instant access to information pertaining to substantially large number of games.

ABSTRACT. Ninety-Nine Prolog Problems (P-99) is a famous set of Prolog exercises. We solved the first thirty three just by prompting an LLM (Large Language Model). We used Claude from Anthropic. By "solved'' we mean: generate the Prolog code and a test file, run the tests and check whether they pass, then formally prove types, groundness, termination, uniqueness, existence and also sometimes functional correctness with LPTP (Logic Program Theorem prover). Hence our approach is an experiment in vibe-coding/vericoding of P-99. It is a vibe-coding experiment because we started from informal specifications written in English and let Claude generate the Prolog code. It also fits within vericoding because the LLM proved reliability guarantees on the generated Prolog code. Claude wrote 58 logic procedures, 508 tests, 257 lemmas for a total of 11800 proof lines. We manually checked each file generated by the LLM. We checked the Prolog code, ran the tests, examined the logical statements generated by Claude and proof-checked Claude's proofs with LPTP. This paper describes this experiment and provides the main details so that it can be reproduced by the interested reader.

ABSTRACT. Abstract interpretation–based verification is a central component of the Ciao Prolog system, enabling expressive specifications of properties of programs, predicates, and execution states. Independently, the LPTP (Logic Programming Theorem Proving) framework offers a first-order logical formalism for expressing and proving properties of predicates. In this paper, we address the problem of relating these two frameworks by studying the translation of Ciao assertions into LPTP formulae and identify a partial correspondence between assertion-based and logic-based specifications. We introduce a systematic translation scheme, characterize assertion classes according to their logical encodability, and propose approximation strategies and auxiliary constructs for non-translatable cases. We analyze the resulting soundness and completeness trade-offs and demonstrate how the proposed approach enables a tight integration of Ciao’s assertion checking with LPTP-based deductive verification, thereby leveraging their complementary capabilities.