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.
