PaperlayerView exact revision on arXiv

Source-linked AI summary

A Simple Doxastic Deontic Logic for Norm-Guided Decision Making

Thorsten Engesser, Agata Ciabattoni

arXiv:2610.00668v1cs.AIcs.LO

TL;DR

Autonomous systems must choose actions amid conflicting norms and incomplete or unreliable information, including uncertainty about which conditional norms apply. The paper combines a lightweight deontic logic with agents’ beliefs and formulates weighted norm-compliance optimization; under stated conditions, subjective and objective optima coincide and optimal decisions reduce to weighted partial MaxSAT in polynomial time.

  • Problem

    Conflicting norms can make full compliance impossible, while incomplete or unreliable beliefs make it difficult to determine which conditional norms apply.

    Source: §1 · p. 1

  • Method

    The paper combines a restricted deontic logic with multi-agent doxastic reasoning and defines an optimization problem that minimizes weighted norm violations.

    Source: §1 · p. 2

  • Results

    For local, decision-sound DNCOPs, optimal decisions reduce in polynomial time to weighted partial MaxSAT.

    Source: §7 · p. 16

  • Takeaways & Limitations

    Under locality and truthfulness conditions, subjectively optimal decisions are also objectively optimal.

    Source: §7 · p. 16

    The framework favors simplicity over expressiveness by restricting normative contents to atomic propositions.

    Source: §7 · p. 16

Abstract

from arXiv · show

Making decisions despite conflicting norms and incomplete or unreliable information is a fundamental challenge for autonomous systems. We introduce a simple doxastic deontic logic for this setting: a classically reducible fragment of Chellas' Minimal Deontic Logic, extended with explicit conditional norms and combined with multi-agent KD45, so that norms can depend on agents' beliefs about both facts and norms. On this logic we define the Doxastic Norm Compliance Optimization Problem, where an agent chooses a decision minimizing weighted norm violations. We distinguish subjective optimization (relative to the agent's beliefs) from objective optimization (relative to the actual facts). We give conditions under which (i) the two coincide and (ii) optimal decision-making can be reduced to weighted partial MaxSAT in polynomial time.

1 Introduction

Norm-guided agents may face conflicting norms and incomplete or unreliable beliefs, making full compliance impossible and norm applicability uncertain. The paper combines a lightweight deontic logic with doxastic reasoning and weighted violation minimization, with conditions for aligning subjective and objective choices and reducing optimization to weighted partial MaxSAT.

1 Introduction

  • When conflicts make full compliance impossible, agents should minimize violation severity and determine applicable conditional norms using their beliefs about the world.Existing approaches address different aspects of these challenges but do not provide a unified framework for doxastic normative reasoning suited to automated decision making.Source: §1 · pp. 1–2
  • The framework combines a restricted fragment of Chellas’ Minimal Deontic Logic with explicit conditional norms and multi-agent doxastic logic, allowing norms to depend on beliefs about facts and norms.Its design targets practical decision support rather than a comprehensive theory of deontic reasoning.Source: §1 · p. 2
  • The Doxastic Norm Compliance Optimization Problem selects among decisions by minimizing weighted norm violations, distinguishing subjective beliefs from the objective state of the world.The framework uses a single quantitative measure of harm and supports encoding contrary-to-duty obligations and exceptions through weighted norms.Source: §1 · p. 2
  • Under natural locality and truthfulness conditions, subjective and objective optimal decisions coincide, and optimal decision making reduces in polynomial time to weighted partial MaxSAT.This enables direct use of existing optimization technology.Source: §1 · p. 2
  • The framework keeps norms explicit and beliefs relevant to their applicability, while its modular design allows integration with existing epistemic logics.The stated aim is logical transparency alongside computational efficiency.Source: §1 · p. 2

2 Preliminaries: Chellas’ Minimal Deontic Logic

Chellas’ Minimal Deontic Logic represents obligations using a neighborhood semantics and tolerates deontic conflicts. A material-implication encoding of conditional obligations detaches, but makes the conditional obligation true whenever its condition is false.

2 Preliminaries: Chellas’ Minimal Deontic Logic

  • In Minimal Deontic Logic, Oφ means that φ is obligatory; Fφ abbreviates O¬φ, and Pφ abbreviates ¬Fφ.The language uses classical atoms, Boolean connectives, and the obligation operator.Source: §2 · p. 3
  • MDL evaluates obligations over neighborhood models, where a neighborhood function assigns sets of worlds to each world and valuations assign atoms.The neighborhoods exclude the empty set and are closed under supersets.Source: §2 · p. 3
  • Defining O(φ|ψ) as ψ → Oφ permits detachment when ψ holds, but also makes the conditional obligation true whenever ψ is false.That behavior is inadequate when the obligation essentially depends on its condition.Source: §2 · p. 3

3 A Tiny Fragment of MDL

The paper restricts MDL so obligations and prohibitions apply only to atomic normative contents, then shows that reasoning in this fragment agrees with classical propositional reasoning. This restriction enables finite instances of satisfiability and entailment to be handled propositionally.

3 A Tiny Fragment of MDL

  • The tiny fragment restricts normative contents to atoms, excluding obligations over arbitrary Boolean combinations such as O(φ ∧ ψ) and O(φ ∨ ψ).Instead, it represents separate obligations as Oφ ∧ Oψ; the restriction also blocks problematic inferences such as Ross’ paradox.Source: §3 · p. 3
  • The language LTDL is formed from simple normative atoms using negation and conjunction, with atoms including p, Oω, and Fω.The restriction is motivated by reducing deontic reasoning to classical propositional logic.Source: §3 · p. 3, Classical Logic as Alternative Semantics · p. 4
  • The canonical model establishes that truth in the fragment agrees with classical propositional truth for every LTDL formula.The result follows from the correspondence for simple normative atoms and the classical truth conditions for negation and conjunction.Source: Classical Logic as Alternative Semantics · p. 4
  • Each concrete finite set of LTDL formulas uses only finitely many simple normative atoms, so its satisfiability or entailment reduces to finite propositional reasoning.Although the overall set of simple normative atoms is infinite, an individual input uses only finitely many.Source: Classical Logic as Alternative Semantics · p. 4

4 Lightweight Deontic Logic

Lightweight Deontic Logic adds explicit conditional norms to a restricted deontic fragment, with factual detachment producing implicit unconditional obligations and prohibitions. Its propositional semantics and Hilbert system support classical reductions and yield NP-complete satisfiability and co-NP-complete validity.

4 Lightweight Deontic Logic

  • LDL represents conditional norms explicitly and uses factual detachment to derive corresponding implicit unconditional obligations and prohibitions.This distinguishes explicit conditional norms from implicit norms that concern the actual state.Source: §4 · p. 4, §4.1 · p. 5
  • LDL includes higher-order norms, such as an obligation to forbid smoking conditional on a prohibition on drinking.Explicit conditional obligations and prohibitions are written O(ω|φ) and F(ω|φ).Source: §4 · p. 4

4.1 Propositional Semantics

  • LDL’s propositional semantics preserves the fragment’s ability to represent dilemmas: having both Oω and Fω does not produce a contradiction.LDL is a conservative extension of the tiny fragment of Chellas’ MDL.Source: §4.1 · p. 5

4.2 Axiomatization of LDL

  • In LDL, satisfiability and validity reduce to classical propositional reasoning by adding the detachment implications for explicit conditional norms.The reduction applies to the normative atoms occurring in the input formula.Source: §4.2 · p. 6
  • LDL satisfiability is NP-complete, while LDL validity is co-NP-complete.The Hilbert-style proof system combines classical propositional tautologies with obligation and prohibition detachment axioms and modus ponens.Source: §4.2 · pp. 5–6

5 A Doxastic Extension of LDL

The extension combines LDL with multi-agent KD45, allowing norms to depend on agents’ beliefs and agents to represent beliefs about norms. Its Kripke semantics combines doxastic accessibility with LDL-consistent valuations and preserves factual detachment at each world.

5 A Doxastic Extension of LDL

  • The extension combines LDL with multi-agent KD45, allowing conditional norms to depend on agents’ beliefs and agents to represent beliefs about norms.Normative contents remain restricted to objective atoms, although norm conditions may contain belief operators.Source: §5 · pp. 6–7

5.1 Kripke Semantics over LDL-Valuations

  • LDLB models use worlds, agent-specific accessibility relations, and LDL-style valuations, with each relation serial, transitive, and euclidean.The model conditions also require LDL-consistency at every world.Source: §5.1 · p. 7
  • At each world, an explicit conditional norm and a satisfied condition entail the corresponding unconditional norm, lifting LDL factual detachment to agents’ mental states.The same detachment condition applies when an agent believes the norm and condition together, or believes them possible.Source: §5.1 · p. 7
  • If an agent believes a cyclist is possible, the norm F(r| ˆBac) entails Fr, whereas F(r|Bac) does not entail Fr.The example distinguishes a condition that the cyclist cannot be ruled out from one requiring belief that the cyclist is present.Source: §5.1 · p. 8
  • LDLB can be axiomatized by adding LDL detachment axioms to multi-agent KD45, and agents can derive beliefs about norms from their own beliefs.For example, believing both F(r| ˆBac) and that c is possible entails believing Fr.Source: §5.1 · p. 8

6 Optimizing Norm Violations

The section formalizes norm-guided decision making as minimizing weighted norm violations, distinguishing evaluation relative to an agent’s beliefs from evaluation against the true world and establishing conditions for these perspectives to agree. It also presents a polynomial reduction of decision-sound local DNCOPs to weighted partial MaxSAT, with optimal assignments encoding subjectively optimal decisions and, for truthful problems, objectively optimal ones.

6.2 Doxastic Norm Compliance Optimization Problems (DNCOPs)

  • A DNCOP asks an acting agent to choose a decision minimizing the total weight of violated applicable norms.It is specified by a finite state vocabulary, environment-fixed true and false atoms, controlled decision atoms and constraints, relevant norms, and positive integer norm weights.Source: §6 · p. 8, §6.2 · p. 9

6.1 State Vocabulary

  • The state vocabulary uses restricted doxastic-deontic atoms: objective atoms or nested belief literals over one objective atom, with consecutive belief operators belonging to different agents.A finite vocabulary closed under subatoms captures the atoms needed to describe the optimization problem.Source: §6.1 · pp. 8–9

6.3 Compatible Models and Violation Counts

  • Objective and subjective violation counts use compatible models based on, respectively, full facts or the acting agent’s beliefs, and take the worst-case weighted norm violations.Every objectively admissible decision is also subjectively admissible; objective counts can be computed directly from the fixed valuation, while subjective counts may remain uncertain.Source: §6.3 · pp. 11–13

6.4 When the Two Perspectives Coincide

  • In a decision-sound local DNCOP, subjectively compatible models agree on each decision’s violation count; adding truthful beliefs makes subjective and objective counts and optimal decisions coincide.Locality makes norms, their contents, and explicit norm conditions depend on the acting agent’s beliefs; truthfulness requires beliefs about fixed atoms to be correct.Source: §6.4 · pp. 13–14

6.5 Reduction to MaxSAT

  • For local DNCOPs, subjective violations can be optimized directly with MaxSAT, and under truthfulness the same construction optimizes objective violations.The stated reduction to weighted partial MaxSAT is polynomial; the translation begins with decision atoms as Boolean variables and encodes the decision constraint as hard clauses.Source: §6 · p. 8, §6.5 · pp. 14–15
  • For each norm, a hard constraint links a fresh variable to its translated violation condition, while a soft clause weighted by the norm’s violation cost charges exactly when it is violated.The hard constraints are converted to CNF using a Tseitin transformation.Source: §6.5 · p. 15
  • In the Example 25 instance, setting r false uniquely minimizes soft-clause cost and encodes the optimal decision d = ∅.Setting r true incurs cost one.Source: §6.5 · p. 15
  • A decision-sound local DNCOP reduces in polynomial time to weighted partial MaxSAT, encoding exactly the subjectively optimal decisions and, if truthful, the objectively optimal decisions.Truthfulness makes subjective and objective violation costs equal for every feasible decision.Source: §6.5 · pp. 15–16

7 Conclusions and Future Work

The paper presents a lightweight deontic logic for uncertain decision making and an optimization framework for minimizing weighted norm violations. It identifies conditions linking subjective and objective optima, a polynomial-time MaxSAT reduction, and directions for extending the framework.

7 Conclusions and Future Work

  • The framework begins with a restricted fragment of Chellas’ Minimal Deontic Logic, where deontic reasoning reduces to classical propositional reasoning while retaining atomic obligations and prohibitions.It adds explicitly represented conditional norms and factual detachment.Source: §7 · p. 16
  • The logic combines conditional norms with multi-agent belief reasoning, distinguishing subjective from objective optimization and conditions under which their optimal decisions coincide.Locality and truthfulness guarantee that subjectively optimal decisions are also objectively optimal.Source: §7 · p. 16
  • For local, decision-sound DNCOPs, optimal decisions can be found through a polynomial-time reduction to weighted partial MaxSAT.The reduction is described as preserving logical rigour and transparency.Source: §7 · p. 16
  • The framework restricts normative contents to atomic propositions, favoring simplicity over expressiveness while retaining coverage of a broad range of practical scenarios.Its modular design leaves room for richer normative and epistemic extensions.Source: §7 · p. 16
  • The paper proposes further analysis of LDLB, extensions beyond local DNCOPs, richer belief bases, and decentralized decision settings.It also plans a MaxSAT implementation and experimental scalability evaluation on representative benchmarks.Source: §7 · p. 16

A Proofs for Section 3 (A Tiny Fragment of MDL)

The proof constructs a neighborhood model for the restricted fragment of Minimal Deontic Logic and establishes its frame properties. It then verifies that atomic obligations and prohibitions correspond to their membership in the constructed worlds.

A Proofs for Section 3 (A Tiny Fragment of MDL)

  • MTDL is constructed with worlds as subsets of the language’s atoms and neighborhoods generated by obligation and prohibition contents, closed minimally under supersets.The construction defines separate sets for obligations and prohibitions and takes their superset closure.Source: A Proofs for Section 3 (A Tiny… · p. 19
  • The construction satisfies the Chellas-style neighborhood frame properties, including superset closure and exclusion of the empty set.The proof establishes that neither obligation nor prohibition generators are empty.Source: A Proofs for Section 3 (A Tiny… · p. 19
  • For each atomic normative content, membership in a world matches its truth there, and the corresponding neighborhood condition characterizes its obligation or prohibition.The proof handles obligations and prohibitions by showing the opposite generator type cannot establish the relevant neighborhood inclusion.Source: A Proofs for Section 3 (A Tiny… · p. 19

B Proofs for Section 4 (Lightweight Deontic Logic)

The proof establishes that consequence in the restricted deontic fragment agrees with classical propositional consequence. It does so by translating countermodels in both directions.

B Proofs for Section 4 (Lightweight Deontic Logic)

  • The equivalence proof proceeds by contraposition, translating a countermodel from one semantics into a countermodel for the other.For formulas in LTDL, the constructed valuation preserves truth and falsity under classical propositional semantics.Source: B Proofs for Section 4 (Lightweight… · p. 20
  • A countermodel to MDL consequence yields a classical valuation that falsifies the conclusion while satisfying the premises, and thus an LDL countermodel.The argument relies on LTDL formulas being Boolean combinations of atoms.Source: B Proofs for Section 4 (Lightweight… · p. 20
  • Conversely, an LDL countermodel can be restricted to the relevant atoms and converted by Theorem 4 into an MDL countermodel.Truth depends only on the atoms in LTDL premises and conclusion.Source: B Proofs for Section 4 (Lightweight… · p. 20

C Proofs for Section 5 (A Doxastic Extension of LDL)

The proof establishes soundness and completeness for LDLB using the propositional and multi-agent KD45 axioms together with deontic detachment. A canonical model supplies the completeness argument, including its frame and detachment conditions.

C Proofs for Section 5 (A Doxastic Extension of LDL)

  • LDLB consequence is equivalent to derivability in the system with propositional, KD45, and deontic detachment axioms.The soundness argument checks validity on serial, transitive, and euclidean frames and preservation by the inference rules.Source: C Proofs for Section 5 (A Doxastic… · pp. 20–21
  • Completeness uses maximal consistent sets to build a canonical model and applies the truth lemma to derive a countermodel when a conclusion is not provable.The proof extends the premises with the negated conclusion to a maximal consistent set.Source: C Proofs for Section 5 (A Doxastic… · p. 21
  • The canonical accessibility relation satisfies seriality, transitivity, and euclideanness, as established from the KD45 axioms.The frame proof derives these properties using axioms D, 4, and 5.Source: C Proofs for Section 5 (A Doxastic… · p. 21
  • The canonical model meets LDLB’s detachment condition, so a conditional obligation or prohibition whose condition holds yields its unconditional counterpart.The proof uses the truth lemma and the detachment axiom instances.Source: C Proofs for Section 5 (A Doxastic… · pp. 20–21
Loading 2610.00668v1…