Logical argumentation uses calculi to generate arguments and counter-arguments to capture defeasible reasoning. In this paper, we introduce modular proof-search procedures for a large class of such argument calculi developed to capture two core forms of defeasible reasoning: normative reasoning, formalized via input/output logics, and doxastic reasoning, formalized via normal default logic. Our approach relies on modular, rule-based, and terminating decomposition trees via step-by-step decomposition of norms and defaults. When successful, a terminated decomposition tree certifies derivability of a given argument in its corresponding calculus, including arguments for obligations and beliefs, as well as defeating arguments concluding inapplicability of norms and defaults. We show how rule-based decomposition of norms and defaults is used to determine nonmonotonic inference for credulous reasoning with maximal consistent sets of norms and defaults as well as stable sets of arguments in formal argumentation.

A normative supervisor is an external module that uses a formal reasoning engine to impose normative constraints on re inforcement learning agents, by either dynamic action masking or feeding the agent additional punishments when violations of norms occur (or both). In this paper, we use a normative supervisor implemented with a solver for deontic answer set programming (ASP) — deolingo — as a basis for the construction of a normative narrator, which uses deolingo’s ability to interface with the explainable solver xclingo to construct a module capable of both regulating behaviour through action masking and additional punishments, and providing contrastive explanations of why a given action was allowed while others were not, relative to the normative system being enforced. The explanations are modelled after the two tiers – internal and external – of explanation. We demonstrate this approach’s ability to provide understandable and descriptive explanations in a scenario where a taxi driver agent must act in accordance to a normative system governing its normal duties and provisions that must be made in case of an emergency.

Dialectical Classical Argumentation (Dialectical Cl-Arg) has been shown to satisfy rationality postulates under resource bounds.In particular, the consistency and non-contamination postulates are satisfied despite dropping the assumption of logical omniscience and the consistency and subset minimality checks on arguments' premises that are deployed by standard approaches to Cl-Arg.This paper studies Dialectical Cl-Arg's formalisation of Preferred Subtheories (PS) nonmonotonic reasoning under resource bounds.The contribution of this paper is twofold.First, we establish soundness and completeness for Dialectical Cl-Arg's credulous consequence relation under the preferred semantics and credulous PS consequences.This result paves the way for the use of argument game proof theories and dialogues that establish membership of arguments in admissible (and so preferred) extensions, and hence the credulous PS consequences of a belief base.Second, we refine the non-standard characteristic function for Dialectical Cl-Arg, and use this refined function to show soundness for Dialectical Cl-Arg consequences under the grounded semantics and resource-bounded sceptical PS consequence.We provide a counterexample that shows that completeness does not hold.However, we also show that the grounded consequences defined by Dialectical Cl-Arg strictly subsume the grounded consequences defined by standard Cl-Arg formalisations of PS, so that we recover sceptical PS consequences that one would intuitively expect to hold.

We present a novel computational approach to resolving conflicts among norms by nonmonotonic normative reasoning (in constrained I/O logics). Our approach extends standard sequent-based proof systems and makes them more adequate to nonmonotonic reasoning by adding to the sequents annotations that keep track of what is known about the defeasible status of the derived sequents. This makes transparent the reasons according to which norms should be applicable or inapplicable, and accordingly the sequents that make use of such norms are accepted or retracted. We also show that this proof theoretic method has tight links to the semantics of formal argumentation frameworks. The outcome of this paper is thus a threefold characterization result that relates, in the context of nonmonotonic normative reasoning, three traditional ingredients of AI-based reasoning methods: maximally consistent sets of premises (in constrained I/O logics), derived sequents (which are accepted in corresponding annotated sequent calculi), and logical arguments (that belong to the grounded extensions of the induced logical argumentation frameworks).

This paper makes a proof-theoretic contribution to resource-bounded dialectical argumentation. Practical deployment of argumentation-based nonmonotonic reasoning can benefit from integration of proof-theoretic means for construction and evaluation of arguments, while accommodating agents with bounded resources. We present a nonmonotonic proof system that implements a generalization of dialectical argumentation, adopting arguments that differentiate between committed and supposed premises, while integrating rules for constructing arguments. The proof system adopts annotations to capture the changing status of arguments in a derivation and employs annotation revision rules that evaluate the dialectical acceptability of these arguments, yielding rational outcomes under resource bounds. Soundness and completeness is shown for the dialectical grounded semantics.

We propose a novel knowledge representation method for the Default Logic paradigm by developing a proof calculus that yields arguments and counter-arguments in which defaults serve as explicit objects of reasoning. The proposed formalism allows for more transparent default reasoning and the use of explain-ability methods in formal argumentation. In particular, we provide a sound and complete argumentative characterization of Default Logic, by demonstrating that argumentation frameworks instantiated by the arguments derivable in our calculus yields the same inference relation as that of Default Logic. The modularity of our approach allows for various modifications of Default Logic. We demonstrate this by extending our calculus with a rule that enables disjunctive defeasible reasoning.

Conflicts are inherent to normative systems. In this paper, we explore a novel approach to normative reasoning by quantifying the amount of conflicts within normative systems. We refine the idea from classical logic, according to which a formula is a consequence of a knowledge base in case its negation renders the knowledge base inconsistent. In our approach, whether a formula is a logical consequence depends, for instance, on its negation's marginal contribution to the inconsistency of the given knowledge base. Accordingly, various inconsistency measures and corresponding (nonmonotonic and paraconsistent) normative entailment relations are analyzed relative to a number of logical properties. To illustrate our approach, we adopt Input/Output logic, a renowned formalism in deontic logic, specifically designed for defeasible normative reasoning. As an application, the resulting entailment relations provide recommendations to agents for minimizing norm conflicts, and may be incorporated in a number of implementations (like the Tweety libraries and the LogiKey framework) by involving inconsistency measurements in normative reasoning.

This paper provides a set of cut-free complete sequent-style calculi for deontic STIT (‘See To It That’) logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting. We leverage these calculi to write a proof-search algorithm deciding deontic, multi-agent STIT logics with (un)limited choice and introduce a loop-checking mechanism to ensure the termination of the algorithm. Despite the acknowledged potential for deontic reasoning in the context of autonomous, multi-agent scenarios, this work is the first to provide a syntactic decision procedure for this class of logics. Our proofsearch procedure is designed to provide verifiable witnesses/certificates of the (in)validity of formulae, which permits an analysis of the (non)theoremhood of formulae and act as explanations thereof. We show how the proof system and decision algorithm can be used to automate normative reasoning tasks such as duty checking (viz. determining an agent’s obligations relative to a given knowledge base), compliance checking (viz. determining if a choice, considered by an agent as potential conduct, complies with the given knowledge base), and joint fulfillment checking (viz. determining whether under a specified factual context an agent can jointly fulfill all their duties).

This paper presents a formal model of specific reasoning patterns in conflict of laws (CoL). CoL arises when multiple countries have jurisdiction due to the diverse nationalities of the involved factors. When initiating legal action in one country, the question of which country’s substantial law to apply emerges, possibly involving the CoL regulations of other countries (in cases of transmission and renvoi). Moreover, parties contemplating legal action in a case falling under CoL often engage in a deliberation process known as forum shopping: determining which country’s CoL regulations would result in the most favorable outcome for them. Our model integrates deontic logic (specifically Input/Output logic) with proof theory and formal argumentation techniques to model both types of reasoning.

Normative reasoning is inherently defeasible. Formal argumentation has proven to be a unifying framework for representing nonmonotonic logics. In this work, we provide an argumentative characterization of a large class of Input/Output logics, a prominent defeasible formalism for normative reasoning. In many normative reasoning contexts, one is not merely interested in knowing whether a specific obligation holds, but also in why it holds despite other norms to the contrary. We propose sequent-style argumentation systems called Deontic Argument Calculi (DAC), which serve transparency and bring meta-reasoning about the inapplicability of norms to the object language level. We prove soundness and completeness between DAC-instantiated argumentation frameworks and constrained Input/Output logics. We illustrate our approach in view of two deontic paradoxes.

We introduce annotated sequent calculi, which are extensions of standard sequent calculi, where sequents are combined with annotations that represent their derivation statuses. Unlike in ordinary calculi, sequents that are derived in annotated calculi may still be retracted in the presence of conflicting sequents, thus inferences are made under stricter conditions. Conflicts in the resulting systems are handled like in adaptive logics and argumentation theory. The outcome is a robust family of proof systems for non-monotonic reasoning with inconsistent information, where revision considerations are fully integrated into the object level of the proofs. These systems are shown to be strongly connected to logical argumentation.