In their daily use arguments are usually not completely enunciated. That is, we often rely on implicit parts, for example, unstated premises, sometimes referred to as enthymemes. Completions of partially stated arguments can favor knowledge engineering processes, where the workload of an engineer can be reduced by suggesting such completions. In this work, we focus on an integral aspect of 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 a declarative approach to compute completions of partial arguments in answer set programming (ASP), including the possibility of preferential reasoning in completions. We empirically evaluate a resulting prototype.
Drawing motivation from the philosophical literature on normative reasons, detachment functions model the way that interaction or competition between reasons determines deontic status of options. This paper presents detachment functions that capture the "dual scale model" of weighing reasons, as outlined in Chris Tucker's recent book "The Weight of Reasons". The dual scale model relaxes an assumption of the standard "single scale model" that much of the informal philosophical literature on reasons relies on, explicitly or implicitly. We define dual scale, single scale, and two further detachment functions, as well as provide a principle-based analysis comparing these systems.
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.
Building on the principles of case-based reasoning, we investigate the extraction of arguments from legal case databases. An argument is modeled as a set of factors that frequently support one party (plaintiff or defendant) over the other. The relevance of an argument is assessed by the number of cases that confirm it versus those that contradict it. Following established practices in data mining, we introduce a condensed representation of arguments called closed arguments, which capture the strongest form of support given the factors they contain. We develop propositional SAT-based encodings to enable the extraction of both arguments and closed arguments using SAT solvers. Additionally, we define a more compact condensed representation called maximal arguments, which eliminates redundancy by retaining only the most informative arguments with respect to given thresholds. We propose a level-wise algorithm that builds on our SAT-based approach for argument extraction. Preliminary experiments demonstrate the feasibility of our SAT-based mining methods.
This paper presents an overview of the Python library InfOCF that provides powerful tools for working with conditional belief bases consisting of defeasible rules of the form "If A, then usually B". Because many operations on belief bases, like checking their consistency or performing nonmonotonic reasoning for answering queries, require solving propositional satisfiability problems and generalizations thereof, InfOCF builds upon the power of current SMT and MaxSAT solvers. For achieving solver independence, established interfaces like PySMT are used, allowing the user to select from different solvers. Multiple queries can be run in parallel for speeding up the answering process. Besides its rigorous focus on modularity and extensibility, further notable features of InfOCF include comprehensive methods for caching program states enabling the reuse of intermediate results across different queries to the same belief base. Successful applications realized with, and now available in, InfOCF cover state-of-the-art implementations of nonmonotonic reasoning with p-entailment, system Z, lexicographic inference, c-inference, and system W; each of these implementations scales up and outperforms all previous implementations of the corresponding inference operator by an order of magnitude.
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 non-classical 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 ( ) is a paradigmatic example of a classical non-Fregean logic. In the paper, we present a new, non-labelled dual tableau calculus for , _ for which we prove soundness, completeness, and termination with an exponential bound on branch length. We compare _ with the already existing complexity-optimal labelled tableau calculus _ . 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 -formulas.
In this paper, we survey literature on grounding in Answer Set Programming (ASP) and related fields, analyse the common benchmarks used for this purpose, and introduce a new grounding benchmark called DIRT. In ASP, reasoning engines typically rely on a "groundand-solve" approach, in which a high-level description of a problem domain (e.g., an Answer Set Program) is first transformed into a low-level description (e.g., aspif) in order to solve. This process, better known as grounding, has a significant effect on the overall speed of the reasoning engine. For this reason, literature contains numerous works dedicated to optimizing various aspects of the grounding process. However, each paper tends to measure their improvements on distinct benchmarks, making a direct comparison between works often difficult. We argue that this is caused by a lack of standardized benchmarks for grounding, and substantiate this claim through a survey of grounding literature. Based on this survey, we have distilled the Dataset for Instantiating in Reasoning Tools (DIRT) as a specialized grounding benchmark. We provide encodings for ASP and ASP-like formats, and present their baseline performance on this problem set. In this way, our benchmark suite can help identify bottlenecks in state-of-the-art grounders, and can serve as a standardized dataset for future works on grounding.
This paper presents the first systematic study of how similarity between arguments affects their evaluation under extension semantics. We define a set of principles that govern how similarity should be taken into account by a semantics, and introduce a broad family of parameterized extension semantics that adhere to these principles. Each member of this family generalizes a classical extension semantics (such as preferred semantics) while disregarding redundant attacks. We identify classes of argumentation graphs in which similarity has no effect on the acceptability status of arguments, and we characterize the conditions under which a family instance either improves an argument's acceptability or coincides with the semantics it generalizes. Finally, we discuss different types of selection functions, which specify the subset of attacks to disregard.
In this paper, we investigate unit refutability in Unit Two Variable Per Inequality (UTVPI) Constraint Systems (UCSs). A Unit Two Variable Per Inequality (UTVPI) constraint is a linear relationship of the form: ± x_i± x_j≤ b_ij , where b_ij∈ℤ . A UCS is a conjunction of such constraints. If it is required that the two variables in a UTVPI constraint have opposite signs, then the constraint is called a difference constraint and a conjunction of such constraints is called a difference constraint system (DCS). When a decision procedure deems a UCS is infeasible, it is important to provide a certificate which attests to the infeasibility of the UCS. Such a certificate is called a negative certificate. Refutations (under an appropriate refutation system) form an important subclass of negative certificates. All problems in the complexity class P have succinct negative certificates. We focus on a subclass of refutations called Unit Refutations (UR). The UR refutation system is incomplete, in that unsatisfiable UCSs may not have unit refutations. However, they are useful from the perspective of identifying variable domains responsible for system inconsistency. Previous work has examined dag-like unit refutations of UCSs [18]. In this paper, we examine tree-like unit refutations of UCSs.
Temporal reference, understood as the capability of referring to particular points of time, is an essential aspect of temporal reasoning. In this paper we model it with the definite description (iota) operator added to first-order monadic logic of order-a standard formalism for reasoning about time. This allows us to express temporal reference directly and with dedicated tools, which is of particular importance from the point of view of proof systems for automated reasoning. We construct a sound and complete tableau system, as well as provide complexity results for the satisfiability problem of the obtained logic.
Handling partially specified inconsistent information is a major challenge, especially when balancing the richness of query answers with the need to control computational complexity. We address this challenge by proposing an efficient method for computing a consistent and enriched fragment of data, known as a repair, within knowledge bases that rely on a stable terminological component and incorporate partially ordered uncertainty in the data (ABox). Our approach, grounded in possibility theory, avoids exhaustive enumeration of conflicts or justifications by applying a positive deductive closure directly to the partially ordered ABox. This enables repair computation through simple consistency checks over data subsets, ensuring tractability while supporting an extended set of plausible inferences. Beyond this main contribution on efficient repair computation, we briefly introduce a semantic characterisation of repairs that generalises the classical notion of models for consistent knowledge bases. Finally, we present an experimental evaluation against existing possibilistic approaches, demonstrating both practical effectiveness and computational benefits.
ANTHEM is a proof assistant designed for verifying several conditions that play an important role in answer set programming. In this note we show that ANTHEM can help us verify equivalence of logic programming solutions to the same problem that have been independently developed by different programmers.
Parametric array theories are extensions of the quantifier-free theory of arrays with relations that hold componentwise. We show that these theories retain rich (general and uniform) quantifier-free interpolation properties. Our results include the interpolation properties of the simple flat array fragment, which were left open in the literature.
In this paper, we investigate preprocessing techniques aimed at improving the efficiency of accessing models of propositional formulas represented in conjunctive normal form (CNF). We focus on three fundamental tasks: uniform sampling, direct model access, and model enumeration. Our analysis reveals that most state-of-the-art preprocessors, when they do not preserve formula equivalence, are generally unsuitable for these tasks. In contrast, we demonstrate that preprocessors which preserve model counts can be effectively leveraged, provided relevant preprocessing information is maintained. To validate our approach, we perform extensive experiments on a diverse suite of benchmarks from multiple domains. The experimental results show that our preprocessing methods are both efficient and robust, yielding significant performance improvements for model access queries when CNF formulas are compiled into d-DNNF representations.
Counting the number of solutions of true and false quantified Boolean formulas (QBFs) 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 is not complete for QBF. Solution enumeration runs into the same problem. 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 that can be interrupted at any time as soon as enough solutions are found. We evaluated our implementation called QEnum in three different case studies.
We introduce an extension of Alternating-Time Temporal Logic (ATL) that incorporates default actions to model communication failures in multi-agent systems. Our framework, ATL-kD, allows for a limited number of communication failures during which agents' intended strategies may not be delivered. In the event of such a communication failure, a predefined default action is played. We analyse the computational complexity of model checking in this setting, showing NP-hardness and coNP-hardness in general, but polynomial-time solvability when default actions are restricted to a fixed subset of agents. We also study a variant with default preferences, which better handles cases where the default action might be unavailable in some states due to protocol constraints. Additionally, we introduce default action updates, allowing the default action to be revised during system execution. Together, these results provide a formal foundation for robust verification under unreliable communication.
Action reversibility in planning deals with the question whether the consequences of a given action can be undone so that the state of the environment returns to what it was before the action was applied. This problem is known to be PSPACE-complete in general. In this paper, we evaluate two PSPACE-complete logic programming languages, namely: Quantified Answer Set Programming (QASP) that extends Answer Set Programming (ASP) with quantified atoms; and Bule, a logic programming language that extends Quantified Boolean Formulas (QBFs) with Datalog-like rules in order to separate the problem domain and problem instance. We give two novel encodings for the problem of action reversibility and perform experiments to see how the solvers for these two languages compare to established methods.
The areas of safety and robustness are key areas where communities from verification, neuro-symbolic AI, and machine learning come together. Safety and robustness are often formalized in terms of point-wise metrics: given an input point, we identify a circle or a region where certain properties hold in terms of the consistency of prediction. However, the broader goal of neuro-symbolic AI applied to machine learning correctness would ideally integrate safety and robustness conditions with explanations. Nonetheless, there is no paper that discusses these properties in a unified manner. What we consider in this paper is a new simple framework for formalizing a variety of such properties. We are able to characterize the robustness condition, safety conditions, hyper-safety conditions, counterfactual explanations, and fairness, among others. We can express these properties using simple notation for an abstract model based on a binary classifier. We hope these definitions would lead to neuro-symbolic frameworks that contribute to all of these areas jointly.
The analysis of unsatisfiable propositional formulas is crucial across a wide range of application domains. While minimal unsatisfiable 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.
This paper introduces novel Maximum Satisfiability (MaxSAT) formulations for the Nonlinear Integer Programming (NLIP) problems with discrete polynomial functions. We develop a generic framework based on three established integer encoding techniques from the literature. Our approach treats each polynomial term as an atomic unit and demonstrates how it can be efficiently encoded through compact representations of integer assignments. Additionally, we present two distinct decomposition methods based on the degrees of polynomial terms. This work lays a foundation for future research and has the potential to extend the applicability of modern MaxSAT solvers to a wider range of optimization problems.
