ABSTRACT. Reinforcement learning is famously about learning by trial and error, the agent getting feedback from the environment in the form of rewards. However, it is often quite difficult to specify a reward function to ensure that the learned behaviour is what the designer intended. It is also difficult to ensure that the agent’s behaviour is always safe, especially when training is on- rather than offline. I will talk about using logic to provide declarative specification of desired/safe behaviours and ensuring that the learned behaviour conforms to those specifications. In particular, I will talk about how to block unsafe actions both during training and after deployment of the agent.

ABSTRACT. Declarative languages are widely used for reasoning about actions and planning, with semantics and extensions for catering different needs. In this work, we introduce the rule-based action language deon-B, which builds on an extension of the well-founded semantics by incorporating deontic operators, allowing one to reason about obligations, prohibitions, and permissions in a non-monotonic setting. To further enhance its applicability in dynamic environments, we integrate a mechanism for action choice inspired by answer set-based action languages, enabling reasoning about transitions between states, and for expressing the evolution of normative goals. Our approach provides a computationally efficient approximation of answer-set-based deontic reasoning while preserving key expressiveness. We evaluate the proposed formalism against well-known deontic challenges, including contrary-to-duty obligations and the distinction between prima facie and actual obligations, demonstrating its ability to capture and resolve normative conflicts within dynamic domains.

ABSTRACT. This paper presents the first systematic study of how similarity between arguments influences their evaluation under extension-based semantics. We show that in coherent argumentation graphs—where similar arguments share identical attackers—similarity has no impact on the acceptability status of arguments. In contrast, in more general graphs, disregarding similarity between attackers can lead to distorted evaluations of their targets.

To address this, we introduce a broad family of parameterized extension semantics, which selectively disregard redundant attacks as determined by a selection function. This family subsumes all standard extension semantics, including grounded, complete, stable, and preferred semantics, while allowing instances that may assign more appropriate statuses to arguments. We characterize the conditions under which an instance of the new semantics improves the acceptability status of an argument or coincides with the semantics it generalizes. Finally, we explore and compare different choices of selection functions.

ABSTRACT. Argumentation frameworks (AFs) are a foundational tool in artificial intelligence for modeling structured reasoning and conflict. SCC-recursiveness is a well-known design principle in which the evaluation of arguments is decomposed according to the strongly connected components (SCCs) of the attack graph, proceeding recursively from "higher" to "lower" components. While SCC-recursive semantics such as \cft and \stgt have proven effective for finite AFs, Baumann and Spanring showed the failure of SCC-recursive semantics to generalize reliably to infinite AFs due to issues with well-foundedness.

We propose two approaches to extending SCC-recursiveness to the infinite setting. We systematically evaluate these semantics using Baroni and Giacomin’s established criteria, showing in particular that directionality fails in general. We then examine these semantics' behavior in finitary frameworks, where we find some of our semantics satisfy directionality. These results advance the theory of infinite argumentation and lay the groundwork for reasoning systems capable of handling unbounded or evolving domains.

ABSTRACT. In their daily use, arguments are usually not completely enunciated. That is, we oftentimes rely on implicit parts, for example unstated premises, sometimes referred to as enthymemes. Possible completions of partially stated arguments can favor knowledge engineering processes, where the work load of an engineer can be reduced by suggesting such completions. In this work we focus on an integral aspect in completing arguments: valid argument structure of a completion. We phrase our results in the formal model of assumption-based argumentation (ABA). Based on an alternative characterization of tree-based arguments in ABA, we provide declarative algorithms for computing completions of incomplete arguments, including the possibility of preferential reasoning in completions. We empirically evaluate a resulting prototype.

ABSTRACT. We study how linear orders can be employed to realise choice functions for which the set of potential choices is restricted, i.e., the possible choice is not possible among the full powerset of all alternatives. In such restricted settings, constructing a choice function via a relation on the alternatives is not always possible. However, we show that one can always construct a choice function via a linear order on sets of alternatives, even when a fallback value is encoded as the minimal element in the linear order. The axiomatics of such choice functions are presented for the general case and the case of union-closed input restrictions. Restricted choice structures have applications in knowledge representation and reasoning, and here we discuss their applications for theory change and abstract argumentation.

ABSTRACT. Planning as SAT is, in addition to explicit and symbolic search, one of the main approaches for solving planning problems. Such planners proved very successful, especially in combinatorially complex domains. SAT-based planning has to date focused on the core formalisms of planning. Notably, there is no SAT-based planner that supports axioms and derived predicates. In this paper, we present our new planner AxSAT that supports axioms as well as conditional effects. Furthermore, we show how to allow for action parallelism using the ∃-step encoding in the presence of axioms. Our empirical evaluation shows that AxSAT performs favorably compared to state-of-the-art approaches for satisficing classical planning with axioms, and provides complementary capabilities.

ABSTRACT. In this paper, we explore preprocessing techniques designed to enhance the efficiency of accessing the models of propositional formulas. Specifically, we focus on three key tasks: uniform sampling, direct access, and model enumeration for formulas represented in this format. Our analysis highlights that state-of-the-art preprocessors that fail to preserve equivalence are generally unsuitable for these tasks. However, we show that preprocessors preserving the model count can be effectively applied, provided that certain preprocessing information is retained. To evaluate our approach, we conducted extensive experiments using a diverse set of benchmarks from various domains. The results demonstrate that our preprocessing methods are both efficient and robust, significantly improving the performance of answering these queries when the formula is compiled into a decision-DNNF representation.

ABSTRACT. The analysis of unsatisfiable propositional formulas is crucial across a wide range of application domains. While minimal unsatisfiability subsets (MUSes) are standard explanations in this setting, gaining a clear understanding of the underlying reasons for unsatisfiability is often difficult when relying solely on them. As an alternative form of explanation, this paper investigates the practical application of power indices to measure the importance of clauses and variables in the inconsistency of a formula. Power indices were originally proposed in game theory to quantify the relative importance of voters in weighted voting games, and their use has been proposed in a variety of areas, including explainability and as measures of inconsistency for knowledge bases. To enable practical computation, this paper introduces a SAT-based approach to approximate the Shapley-Shubik power index. Our approach leverages a probabilistic algorithm with theoretical guarantees and incorporates optimization techniques to significantly improve performance. Experimental results demonstrate the suitability of the proposed algorithm.

ABSTRACT. Counting the number of solutions of true and false quantified Boolean formulas (QBFs) is a research area that has received increased interest in recent years. However, the explicit enumeration of all solutions for a QBF is almost unexplored so far. For QBF solution counting, it has been shown that enumeration-based counting as employed in SAT solving is not complete for QBF. To also count solutions that were not covered by the enumeration-based approach, propositional model counters can be employed for true QBFs. Solution enumeration runs into the same problem.

In this paper, we propose a refinement-based approach to enumerate all solutions of true and false QBFs. To this end, we develop a novel framework to characterize the enumeration problem at quantifier level two and present a complete enumeration algorithm. We implemented the presented approach together with several optimizations in a tool called QEnum which we evaluated in three different case studies.

ABSTRACT. Usually, two quantified Boolean formulas (QBFs) are said to be equivalent if they have the same truth value for every assignment to the free variables. This notion of equivalence is very coarse-grained in the sense that it considers only assignments to the free variables, but it does not take the models or counter-models of the two QBFs into account. In this paper, we investigate refined notions of equivalences on the solution level to obtain a more fine-grained comparison of two formulas. We show that the problem of checking solution equivalence is PSPACE complete.

ABSTRACT. First Order Team Semantics is a generalization of Tarskian Semantics in which formulas are satisfied with respect to sets of assignments. In Team Semantics, it is possible to extend First Order Logic via new types of atoms that describe dependencies between variables; some of these extensions are strictly more expressive than First Order Logic, while others are reducible to it.

Many of the atoms studied in Team Semantics are inspired by Database Theory and belong in particular to the class of Disjunctive Embedded Dependencies, a very general family of dependencies that contains most of the dependencies of practical interest in the study of databases.

In this work, I provide a characterization for the (domain-independent) Disjunctive Embedded Dependencies that fail to increase the expressive power of First-Order Team Semantics when added to it.

ABSTRACT. We provide a generalisation of Kripke semantics for an extension of intuitionistic Lukasiewicz logic (LLi) with weak excluded middle (LLiw). This analogises the situation with intuitionistic logic (IL) extended by weak excluded middle (WEM). This paper extends the insights of Ronbinson et al. regarding LLi to LLiw.

ABSTRACT. This paper investigates the sequential logics for modal Ockham algebras, which are Ockham algebras with normal modal operators $\Box,\Diamond$ satisfying the interaction axioms. Relational semantics are established for this logic, and discrete duality is shown using star semantics. We then obtain the Kripke-completeness for this logic and some common modal extensions by the canonical model method. Furthermore, we extend existing results, which are based on modal Ockham algebra, to each modal Berman variety.

ABSTRACT. Definite descriptions are first-order expressions that denote unique objects satisfying certain properties. In this paper, we propose a second-order counterpart, designed to refer to unique relations between objects. We investigate this notion within the framework of Russell's theory of definite descriptions. While full second-order logic is incomplete, its fragment defined by Henkin's general models admits completeness. We develop our theory within this fragment and formalize it using a cut-free sequent calculus.

ABSTRACT. Non-Fregean logics reject Frege's Principle according to which sentences are names of their truth values. Instead, the non-Fregean framework assumes the existence of a universe of semantic correlates of sentences in the semantics and introduces into the language a non-truth-functional propositional connective of non-Fregean equivalence, ≡, which enables referring to and reasoning about the denotations of sentences. It turns out that many nonclassical logics - including modal, many-valued, intuitionistic, relevant, and paraconsistent logics - can be represented as non-Fregean systems. Thus, the non-Fregean approach offers a unified and inclusive framework for studying the nature of logical connectives and the principles underlying reasoning about the interplay between sentence meanings. Sentential Calculus with Identity (SCI) is a paradigmatic example of a classical non-Fregean logic. In the paper, we present a new, non-labelled dual tableau calculus for SCI, DTSCI for which we prove soundness, completeness, and termination with an exponential bound on branch length. We compare DTSCI with the already existing complexity-optimal labelled tableau calculus TSCI. We show that even though these systems use very different methodologies, which manifests itself not only in the presence of labels in one of them and the lack thereof in the other, but also in disparate sets of rules handling the identity connective and dissimilar techniques used throughout the completeness proofs, both offer a satisfactory solution to the problem of satisfiability/validity of SCI-formulas.