ABSTRACT. Dung's abstract Argumentation Framework (AF) has been extended in several directions to make knowledge representation and reasoning more intuitive and expressive. In this paper, we discuss the Knowledge-based Argumentation Framework (KAF), an extension of AF with a Knowledge Base (KB) expressed in DL-Lite, which includes concept and role instances describing the topology of an AF, besides additional knowledge on the domain~[1]. The KAF semantics is given by a set of KAF extensions, each consisting of an extension of the underlying AF together with a ``pertinent'' subset of the original KB, which is obtained by discarding assertions referring to arguments that have been ruled out in the AF extension. Then, the framework is further expanded into the Constrained KAF (CKAF), where a set of restricted relational calculus formulae is used for reasoning over `feasible' subframeworks that satisfy the formulae and minimally differ from the original framework.

ABSTRACT. Description Logic (DL) terminologies are collections of rules in which a class is defined in terms of a complex DL concept. Various semantics for terminologies have been proposed over the past decades. However, the tight relation with the recent W3C SHACL standard for expressing constraints over RDF graphs motivated the need to enrich terminologies with forms of commonsense reasoning. In this paper, we explore how reasoning over DL terminologies can be captured in argumentative terms, by establishing a translation into Assumption-Based Argumentation (ABA), a rule-based formalism comprising defeasible assumptions, where argumentation semantics are used to retrieve sets of jointly acceptable assumptions. We focus on the problem of graph completion, where a labeled graph is extended by assigning additional labels only to existing nodes while satisfying a given terminology. Building on the existing correspondence between logic programs and ABA, we show how a DL terminology and a labeled graph can be encoded as an ABA framework such that different completions of the graph arise from different criteria for selecting sets of assumptions. We present results for DL terminologies in ALCI under the classical semantics, the minimal model semantics of Circumscription, and the stable model semantics of Quantified Equilibrium Logic. Furthermore, we provide preliminary results for fragments of the DL-Lite family, where the problem of graph completion is extended to allow the introduction of new domain elements, enabling full model construction.

ABSTRACT. Modifying a knowledge base to remove an unwanted consequence is a difficult task, since it is not obvious how to change it so that the unwanted consequence is no longer implied while avoiding unnecessary loss of information. This problem has been widely researched in belief change under the name of contraction and in ontology engineering under the name of ontology repair. The extension of belief change theory to description logic ontologies represents an important development for both areas, as it allows repair techniques to benefit from advances in belief change and enables contraction operations to preserve more consequences than classical contractions based on subsets of the belief base by utilizing advances in repair techniques. Consequently, to different variations of these postulates have emerged in the literature, seeking to preserve the same intuitions as the original sets in different ways, as is the case with the use of Description Logics. This paper discusses the existing contraction postulates and their adequacy across different scenarios, exploring the intuition behind them and the use of different types of contraction postulates in the literature.

ABSTRACT. Recent work in defeasible reasoning has seen notions of preferential semantics in the style of Kraus et al. applied in various modal logics. However, work in this field has focussed primarily on satisfiability checking, and monotonic notions of entailment which may be inferentially weak. One particular modal logic where this has been introduced, is propositional standpoint logics, where modalities can express the views of different viewpoints. This has resulted in the formalisation of propositional defeasible standpoint logic (PDSL). In this paper, we propose a means of lifting the class of (non-monotonic) rational entailment relations from traditional KLM-style reasoning to a fragment of PDSL. In order to do so, we extend the expressivity of PDSL via situated standpoint conditionals, allowing us to talk about a defeasible conditional holding in the context of a given standpoint. This allows us to the syntax of PDSL in terms of situated conditionals, and showing that a large fragment of PDSL is expressible as a set of situated conditionals. We then focus on characterizing non-monotonic entailment in this fragment, defining a method to transport any ranking-based entailment relation from the propositional case into the PDSL case. This is first described in the general case and then considered in the specific cases of rational and lexicographic closure, which provides a faithful translation of each inference to PDSL. We also show that entailment-checking in this fragment of PDSL can be done largely using algorithms from the propositional case, while preserving complexity bounds.

ABSTRACT. In this paper, we integrate the defeasible logic of Kraus, Lehmann and Magidor (KLM) with the standpoint logic framework of Gómez Álvarez and Rudolph. This is done with the goal of formally expressing knowledge taking into account multiple (possibly contradicting) viewpoints, which in turn may hold defeasible beliefs. In doing so, we utilize Defeasible Restricted Standpoint Logics (DRSL), introduced by Leisegang et al. Our work expands on previous work by providing a foundational representation result for DRSL semantics and systematically lifting several well-known entailment relations from the propositional case to the standpoint-enhanced setting. In particular, we characterize the semantics for DRSL through a set of KLM-style postulates adapted for the standpoints case. We furthermore provide a means to lift preferential entailment, and the class of entailment relations based on single ranking functions from the purely propositional to the standpoint-enhanced context, including rational and lexicographic closure. We show this can be done equivalently through semantic and algorithmic means. Furthermore, we show that, for each considered form of entailment, the complexity class of entailment checking does not change when moving from propositional KLM to DRSL.

ABSTRACT. The present contribution is framed in the context of probabilistic belief by analyzing two main approaches to the subject: the Lockean thesis, and Leitgeb’s notion of P-stable sets. More precisely, the present contribution puts forward an investigation that aims at establishing contact points between the deductive closure of Lockean belief sets, conformity to a characterization we obtained in terms of step probabilities, and the revision of belief sets that are defined in terms of P-stability. For the latter approach, in addition to the original ideas and results of Leitgeb from 2013, we will also follow a path recently studied by Delgrande, Lakemeyer, Pagnucco, and Sack. We find tight links between these two approaches in the setting of probabilistic epistemic change.

ABSTRACT. Inductive definitions are an important form of knowledge in mathematics and computer science. Two common techniques to prove theorems about inductive definitions are the principle of mathematical induction and the principle of infinite descent. To formalize these principles, Brotherston and Simpson introduced the sequent calculus proof systems LKID for mathematical induction, and LKID𝜔 and CLKID𝜔 for infinite descent. LKID𝜔 is an infinitary system, in which proofs are infinite trees, and CLKID𝜔 a cyclic system, in which proofs are finite graphs. However, these calculi restrict to monotone definitions, while inductive definitions are generally non-monotone. The logic FO(ID) extends classical first-order logic with non-monotone inductive definitions. In previous work, we provided a formalization of the principle of mathematical induction for non-monotone definitions by extending LKID to a sequent calculus SCFO(ID) for FO(ID). In this work, we provide a formalization of the principle of infinite descent for non-monotone definitions by extending LKID𝜔 and CLKID𝜔 to sequent calculi SCFO(ID)∞ resp. SCFO(ID)⟲ for FO(ID). We extend several proof-theoretic results for LKID𝜔 and CLKID𝜔 to SCFO(ID)∞ and SCFO(ID)⟲ regarding soundness, completeness, cut-elimination and the relation with SCFO(ID).

ABSTRACT. Independence in nonmonotonic and probabilistic reasoning, in various forms, has long been an active area of study. At the same time, significant progress has been made in consolidating the study of independence in category theory. In particular, the notion of an independent product characterises independence or separability in a remarkable variety of contexts. This paper takes some first steps toward applying this theory to nonmonotonic and probabilistic reasoning. We detail several categories C of preference structures and introduce the notion of a preference functor 𝑃 : Sig → C, which assigns signatures to preference structures on possible worlds. We define a notion of semantic independence with respect to a preference functor 𝑃 in terms of independent products. For ordinal conditional functions, this corresponds to known notions of independence in nonmonotonic reasoning and belief revision. On the other hand, we show that the category of total preorders does not possess an independent product that corresponds to such established notions of independence. In doing so, we demonstrate how established definitions of independence for OCFs are in fact the same phenomenon as usual independence of random variables in probability theory, while also offering a reason why TPOs are not as well-behaved as OCFs in terms of independence. Our proposed framework allows for reasoning about independence in nonmonotonic and probabilistic reasoning at a new level of generality. Furthermore, this opens the door to apply theories of independence from diverse contexts to our setting.

ABSTRACT. Input/Output (I/O) logic provides a flexible framework for representing conditional norms without reducing them to truth-functional implications. Among its variants, constrained Input/Output logic refines the applicability of norms by introducing constraints that limit when obligations may be detached, enabling a fine-grained account of defeasible normative reasoning. In this paper, we present a formal embedding of I/O logic in Higher-Order Logic (HOL), building on the algebraic approach based on subordination structures and slanted algebras. The embedding is based on the algebraic characterization of input/output operations with intermediate translations into slanted modal algebras. We formalize constrained input/output operations within the algebraic framework and embed them in HOL. We then implement the translation in the Isabelle/HOL proof assistant, enabling automated reasoning within the system. Our approach generalizes previous embeddings of standard I/O logic and provides a foundation for the analysis and verification of defeasible normative systems.