This study explores the application of Answer Set Programming (ASP) for detecting anomalies in system logs, addressing the challenges posed by evolving cyber threats. We propose a novel framework that leverages ASP's declarative nature and logical reasoning capabilities to encode complex security rules as logical predicates. Our ASP-based system was applied to a real-world Linux system log dataset, demonstrating its effectiveness in identifying various anomalies such as potential brute-force attacks, privilege escalations, frequent network connections from specific IPs, and various system-level issues. Key findings highlight ASP's strengths in handling structured log data, rule flexibility, and event correlation. The approach shows promise in providing explainable alerts from real-world data. This research contributes to computer forensics by demonstrating a logic-based paradigm for log analysis on a practical dataset, opening avenues for more nuanced and adaptive cyber intelligence systems.

Supported models offer a semantics for logic programs that relaxes the minimality constraint of stable models while maintaining logical consistency through a support condition. Despite their theoretical significance since 1988, supported models lack practical computational tools integrated with modern Answer Set Programming (ASP) infrastructure. We present a transformation-based method that enables computation of supported models using standard stable model solvers. Our approach transforms any ground logic program into an equivalent program whose stable models correspond exactly to the supported models of the original program. We implement this transformation as a preprocessor for Clingo and demonstrate applications in software verification, medical diagnosis, and planning where supported models enable valuable exploratory reasoning beyond stable models.

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, and resource usage, as well as 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 on 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.

Given the increased importance of physical AI, reliable planning in dynamic environments remains a critical function of embodied systems. In particular, care must be taken in how they interact with situations outside the boundaries of their training. While planning languages such as PDDL or STRIPS tend to be highly problem-dependent, LLMs can be applied to broader and more general tasks in dynamic environments, but remain prone to hallucinations. Logic-based systems, in contrast, provide frameworks for a wide variety of problems and offer justifications for complete and correct plans, but offer no explanation when they cannot generate a plan. For example, VECSR, a planning system based on the s(CASP) answer set programming system, can create plans for unseen tasks by generalizing from a small number of training tasks. However, this generalization is limited to tasks achievable with actions learned during training. To address this limitation, we propose and build the Counterfactual Generation Module, which exploits the justification framework of s(CASP) to identify counterfactuals for unachievable tasks. These counterfactuals allow us to detect missing actions that should be incorporated into VECSR’s knowledge base to enable task completion. We validate our proposal by asking VECSR to generate action plans for 55 tasks outside the 10 it was trained on. For 16 tasks, VECSR could not produce plans, and the counterfactuals “identified” the actions that need to be learned to complete 13 of them. Next, we evaluated 56 plans generated by GPT-4o, observing that the module’s assessment of plan correctness corresponded to human evaluation, supporting that the module itself is correct.

Solving textual reasoning problems by translating them into logic has proven effective, as it reduces hallucinations and allows the logic solver to handle complex reasoning. However, there is one major challenge that makes this technique difficult to apply to many practical reasoning problems. Arguments presented in text often have implicit rules that are assumed to be part of commonsense knowledge and are therefore omitted. They need to be identified and explicitly added to a logic program for accurate reasoning. This process is typically called argument reconstruction. Discovering these implicit logic rules is a challenging problem that previous text-to-logic translation systems struggle with. In this paper, we present a novel system that reconstructs these implicit rules in 3 stages: (i) Translating the problem from text to First Order Logic (FOL), (ii) Translating FOL to an equivalent s(CASP) answer set program that can compute gap predicates (predicates whose derivation requires implicit rules), and (iii) Using an LLM to generate required implicit rules for these gap predicates. We show that our system generates implicit rules to effectively solve reasoning problems drawn from a popular benchmark designed to be challenging for LLMs.

Static program verification tools are essential for ensuring software correctness and reliability without executing the code. However, their effectiveness relies heavily on precise configuration, which must be tailored to specific project requirements, coding standards, and quality objectives. Selecting appropriate configurations is challenging due to the unique properties of each codebase and the need for an in-depth understanding of the analysis techniques. Current methods often default to standard settings or rely on random exploration, leading to sub-optimal results. In this paper, we introduce ConfigTuneX, a novel rule-based machine learning approach that optimizes configuration settings in static program verification tools through composite FOLD-SE rules. These rules simultaneously address two critical challenges: (1) reducing inconclusive outcomes by distinguishing unresolved cases from resolved outcomes, and (2) improving verification accuracy by separating correct outcomes from incorrect ones. The extracted rules are transformed into stratified answer set program (ASP) compatible with the s(CASP) solver, which systematically generates counterfactual configurations to avoid undesired outcomes. This targeted reasoning narrows the search space to the most promising configurations, reducing computational overhead while enhancing both interpretability and effectiveness. Experimental results show that ConfigTuneX with composite FOLD-SE rules consistently outperforms the state-of-the-art baseline across verification tools. On Jayhorn, CBMC, and Symbiotic, ConfigTuneX improves success rates by 76.34

Event Calculus (EC) implemented in answer set programming (ASP) has proven suitable for specifying requirements 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 of value domains of time and system properties (fluents) pose significant challenges. Grounding-based ASP solvers, e.g., clingo, which implement Discrete EC (DEC), lead to combinatorial explosion in program size and inaccurate representation. The grounding-free s(CASP) does not discretize but struggles with non-termination due to its top-down execution. This paper introduces Hybrid EC, an extended axiomatization of DEC, that tackles the challenges via 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 value (dense) 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 they are unaffected by the size of the domains and that handling rationals does not impact scalability. Most importantly, the ability of clingo-lpx to handle dense domains enables accurate modeling of continuous change.

Autonomous unmanned aerial vehicles (UAVs) must operate safely in dynamic environments and adapt to changing mission conditions. Although deep learning approaches have shown strong performance for navigation and perception, they are often difficult to explain, verify, and modify for safety-critical tasks. We propose a symbolic state-centered UAV agent using the s(CASP) answer set programming system, enabling autonomous task execution with constraint-based commonsense reasoning in a high-fidelity Unreal Engine 5 environment. We fully implement prior work on the VECSR-A system to support multi-step autonomous behaviors including navigation, search, debris detection, precision spraying, object transport, and inspection. The UAV reasons over environmental and spatial constraints, dynamically revising plans when tasks fail or data is insufficient. Because decisions are based on commonsense reasoning, they are guaranteed to be correct and explainable. We evaluate the feasibility of s(CASP) for UAV control in realistic simulated missions. Results show that our framework enables explainable, adaptive autonomy without retraining, handling complex constraint-aware decisions and dynamic task reevaluation.

Creating AI systems that are reliable and trustworthy has long been a challenging field of study. However, the need for trustworthy systems has been exacerbated in recent years by the ubiquitous availability of AI systems to laymen. AIs are no longer used only by specialists well-equipped to understand them, but also by members of the general public with no software training whatsoever. The state-of-the-art AI system is based on deep learning, however deep learning systems have serious deficiencies in explainability that decrease trust. Logic programming solutions have been proposed, both standalone and as augmentations to deep learning systems, as an inherently explainable and therefore trustworthy alternative to deep learning-only AIs. However, the inherent explainability of logic programming has not been verified with participants who have no experience with logic programming. We seek to validate the inherent explainability of logic programming in a user study of members of the general public and evaluate whether explainability tools in logic programming languages lead to improved understanding. We found that only 46.15

Machine learning models increasingly influence decisions in high-stakes settings such as finance, law and hiring, driving the need for transparent, interpretable outcomes. However, while explainable approaches can help understand the decisions being made, they may inadvertently reveal the underlying proprietary algorithm: an undesirable outcome for many practitioners. Consequently, it is crucial to balance meaningful transparency with a form of recourse that clarifies why a decision was made and offers actionable steps following which a favorable outcome can be obtained. Counterfactual explanations offer a powerful mechanism to address this need by showing how specific input changes lead to a more favorable prediction. We propose Model-Agnostic Causally Constrained Counterfactual Generation (MC3G), a novel framework that tackles limitations in the existing counterfactual methods. First, MC3G is model-agnostic: it approximates any black-box model using an explainable rule-based surrogate model. Second, this surrogate is used to generate counterfactuals that produce a favourable outcome for the original underlying black box model. Third, MC3G refines cost computation by excluding the “effort" associated with feature changes that occur automatically due to causal dependencies. By focusing only on user-initiated changes, MC3G provides a more realistic and fair representation of the effort needed to achieve a favourable outcome. We show that MC3G delivers more interpretable and actionable counterfactual recommendations compared to existing techniques all while having a lower cost. Our findings highlight MC3G's potential to enhance transparency, accountability, and practical utility in decision-making processes that incorporate machine-learning approaches.

Answer Set Programming (ASP) with stable model semantics has proven highly effective for knowledge representation and reasoning. However, the minimality requirement of stable models can be restrictive for applications requiring exploration of non-minimal but logically consistent solution spaces. Supported models, introduced by Apt, Blair, and Walker in 1988, relax this minimality constraint while maintaining a support condition ensuring every true atom is justified by some rule. Despite their theoretical significance, supported models lack practical computational tools integrated with modern ASP solvers. We present a novel transformation-based method enabling computation of supported models using standard ASP infrastructure. Our approach transforms any ground logic program into an equivalent program whose stable models correspond exactly to the supported models of the original program. We implement this transformation for Clingo, providing the first practical tool for computing supported models with state-of-the-art ASP solvers. We demonstrate applications in software verification, medical diagnosis, and planning where supported models enable valuable exploratory reasoning capabilities beyond those provided by stable models. We also provide an empirical evaluation to justify the practical utility of our approach compared to established methods. Our implementation is publicly available and compatible with standard ASP syntax.

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.

The advanced machine learning (ML) algorithms in artificial intelligence (AI) are complex, with limited insight into the interpretability of these models. Explainable AI (XAI) is an emerging research field that seeks to clarify the rationale behind the outcomes predicted by ML and AI models. We hypothesized that contemporary XAI tools, such as the FOLD-R++ (Improved First Order Learner of Default with Recursive Rules) algorithm and the s(CASP) (System for Answer Set Programming with Constraints) utility, could achieve accuracy within 5% of those from well-known ML algorithms. FOLD-R++ offers meaningful reasoning through justification trees for predicted outcomes, similar to LIME (Local Interpretable Model-Agnostic Explanations) used with ML algorithms. We employed FOLD-R++, an automated inductive learning algorithm, and s(CASP), a reasoning interpreter utility, on ten binary classification datasets from various domains. FOLD-R++ consistently produced accuracy within 5% of those from ML algorithms across all datasets and did so in less processing time in most of the tests. The rulesets generated by FOLD-R++ were processed in s(CASP), which uses constraints in Answer Set Programming to create easily understandable reasoning trees. Finally, ML models were run through LIME to generate graphical representations highlighting dominant parameters affecting outcomes. This analysis approach can be a standard pattern for gaining insights into binary classification machine learning problems.

It has been argued that Event Calculus (EC) is suitable for modeling high-level specifications of safety-critical cyber-physical systems. The primary advantage lies in the rather small semantic gap between EC models and requirements expressed in a semi-formal natural language. Moreover, its use of continuous time and variables avoids imprecision that stems from discretization. In the past, we have shown that a goal-directed ASP system can be used for implementing these EC models. However, precise representation of time as an infinitesimally divisible continuous quantity leads to Zeno-like behaviors and to non-termination in such a system. In this work, we model a number of well-known example problems from the literature to systematically study various natural EC modeling patterns that yield these Zeno-like behaviors, and propose ways to deal with them. Moreover, we also propose a technique to automatically detect all such cases.

Don't Starve is a non-linear, real-time survival video game where the player's objective is to survive as long as possible. The game is challenging because randomly generated situations and events make it hard to survive this game for a long time. However, the game follows specific rules that can be used to predict future outcomes. We can use these rules to automate its playing. Our preliminary effort reported in this paper uses the answer set programming framework to model the game-playing agent's logic to survive in the game for as long as possible. The agent learns the environment around it and translates the knowledge into facts represented as predicates. A set of commonsense reasoning rules represented in ASP captures the logic that the agent must use to survive. We combined the logic rules with the facts about the environment to compute the best action the agent must take. We use the s(CASP) goal-directed predicate ASP engine and a custom game modification program written in Lua supported by the game environment that can interface with s(CASP). Our results indicate that our preliminary automated game-playing system can outperform novice players. Further refinement should allow our system to survive longer.

As the Large-Language-Model-driven (LLM-driven) Artificial Intelligence (AI) bots became popular, people realized their strong potential in Task-Oriented Dialogue (TOD). However, bots relying wholly on LLMs are unreliable in their knowledge, and whether they can finally produce a correct result for the task is not guaranteed. The collaboration among these agents also remains a challenge, since the necessary information to convey is unclear, and the information transfer is by prompts – unreliable, and malicious knowledge is easy to inject. With the help of logic programming tools such as Answer Set Programming (ASP), conversational agents can be built safely and reliably, and communication among the agents made more efficient and secure. We proposed an Administrator-Assistant Dual-Agent paradigm, where the two ASP-driven bots share the same knowledge base and complete their tasks independently, while the information can be passed by a Collaborative Rule Set (CRS). The knowledge and information conveyed are encapsulated and invisible to the users, ensuring the security of information transmission. We have constructed AutoManager, a dual-agent system for managing the drive-through window of a fast-food restaurant such as Taco Bell in the US. In AutoManager, the assistant bot takes the customer's order while the administrator bot manages the menu and food supply. We evaluated our AutoManager and compared it with the real-world Taco Bell Drive-Thru AI Order Taker, and the results show that our method is more reliable.

There has been significant focus on creating neuro-symbolic models for interpretable image classification using Convolutional Neural Networks (CNNs). These methods aim to replace the CNN with a neuro-symbolic model consisting of the CNN, which is used as a feature extractor, and an interpretable rule-set extracted from the CNN itself. While these approaches provide interpretability through the extracted rule-set, they often compromise accuracy compared to the original CNN model. In this paper, we identify the root cause of this accuracy loss as the post-training binarization of filter activations to extract the rule-set. To address this, we propose a novel sparsity loss function that enables class-specific filter binarization during CNN training, thus minimizing information loss when extracting the rule-set. We evaluate several training strategies with our novel sparsity loss, analyzing their effectiveness and providing guidance on their appropriate use. Notably, we set a new benchmark, achieving a 9 average, compared to the previous SOTA, while coming within 3 CNN's accuracy. This highlights the significant potential of interpretable neuro-symbolic models as viable alternatives to black-box CNNs.

Since the first conference In Marseille in 1982, the International Conference on Logic Programming (ICLP) has been the premier international event for presenting research in logic programming. These proceedings include technical communications about, and abstracts for presentations given at the 40th ICLP held October 14-17, in Dallas Texas, USA. The papers and abstracts in this volume include the following areas and topics. Formal and operational semantics: including non-monotonic reasoning, probabilistic reasoning, argumentation, and semantic issues of combining logic with neural models. Language design and programming methodologies such as answer set programming. inductive logic programming, and probabilistic programming. Program analysis and logic-based validation of generated programs. Implementation methodologies including constraint implementation, tabling, Logic-based prompt engineering, and the interaction of logic programming with LLMs.

The development of autonomous agents has seen a revival of enthusiasm due to the emergence of LLMs, such as GPT-4o. Deploying these agents in environments where they coexist with humans (e.g., as domestic assistants) requires special attention to trustworthiness and explainability. However, the use of LLMs and other deep learning models still does not resolve these key issues. Deep learning systems may hallucinate, be unable to justify their decisions as black boxes, or perform badly on unseen scenarios. In this work, we propose the use of s(CASP), a goal-directed common sense reasoner based on Answer Set Programming, to break down the high-level tasks of an autonomous agent into mid-level instructions while justifying the selection of these instructions. To validate its use in real applications we present a framework that integrates the reasoner into the VirtualHome simulator and compares its accuracy with GPT-4o, running some of the "real" use cases available in the domestic environments of VirtualHome. Additionally, since experiments with VirtualHome have shown the need to reduce the response time (which increases as the agent's decision space grows), we have proposed and evaluated a series of optimizations based on program analysis that exploit the advantages of the top-down execution of s(CASP).