PaperlayerView exact revision on arXiv

Source-linked AI summary

Dialogue-based Explanations for Logical Reasoning using Structured Argumentation

Loan Ho, Stefan Schlobach

arXiv:2502.11291v1cs.AIcs.DBcs.HCcs.LO

TL;DR

Existing approaches to explaining reasoning in inconsistent knowledge bases can omit important information, including reasoning steps and non-binary conflicts. The paper proposes a general argumentation framework with dialogue-based proof procedures and trees; it reports soundness and completeness results and illustrates how a query can be accepted as possible.

  • Problem

    Existing explanations for inconsistent knowledge bases can omit reasoning steps or fail to represent non-binary conflicts, limiting how much of the reasoning they convey.

    Source: §1 · pp. 1, 3

  • Method

    The paper translates logics involving maximal consistent subsets into P-SAFs and uses explanatory dialogue models as dialectical proof procedures for acceptance.

    Source: §1 · pp. 4–5

  • Results

    The paper proves the dialogue model sound and complete with respect to argumentation semantics and illustrates a system concluding that Victor is possibly a researcher.

    Source: §1 · pp. 4–5

  • Takeaways & Limitations

    Dialogue trees represent explanations of acceptance and can expose intermediate reasoning steps in logical reasoning with inconsistencies.

    Source: §1 · p. 5

    In one AF4 case, the dialectical proof procedure fails to deliver an admissible set because argument construction enters an infinite loop.

    Source: §5.3 · p. 28

Abstract

from arXiv · show

The problem of explaining inconsistency-tolerant reasoning in knowledge bases (KBs) is a prominent topic in Artificial Intelligence (AI). While there is some work on this problem, the explanations provided by existing approaches often lack critical information or fail to be expressive enough for non-binary conflicts. In this paper, we identify structural weaknesses of the state-of-the-art and propose a generic argumentation-based approach to address these problems. This approach is defined for logics involving reasoning with maximal consistent subsets and shows how any such logic can be translated to argumentation. Our work provides dialogue models as dialectic-proof procedures to compute and explain a query answer wrt inconsistency-tolerant semantics. This allows us to construct dialectical proof trees as explanations, which are more expressive and arguably more intuitive than existing explanation formalisms.

1. Introduction

Existing explanations for reasoning in inconsistent knowledge bases can omit the reasoning steps connecting premises to conclusions and may fail to track relevant conflicts. The paper proposes a general argumentation framework and dialogue-based explanations, illustrated by a case where additional evidence is needed to defend a query answer.

1. Introduction

  • Set-based explanations provide premises but may omit the reasoning connecting them to a conclusion, while existing proof-based explanations largely focus on consistent knowledge bases.The paper also identifies missing contradiction tracking and, in prior dialogue models, incomplete explanations and limits on n-ary conflicts.Source: §1 · pp. 1–2
  • Prior approaches are described as restricted to particular logics or representation settings, binary conflicts, or explanations that do not expose argument structure exhaustively.The paper contrasts these limits with a general framework for dialogue models in structured argumentation.Source: §1 · pp. 2–3
  • In the Victor example, the initial cause for accepting researcher omits the KD teaching fact needed to explain why the answer is only possible.That fact supports lecturer status, which makes the conflicting teaching-assistant argument uncertain under the constraint that lecturers cannot be teaching assistants.Source: §1 · p. 3
  • A proponent defends researcher status with the KR-course facts, counters the opponent’s teaching-assistant attack using the KD teaching fact, and succeeds when the opponent has no further argument.The resulting defending set extends the initial justification with the KD teaching fact; the opponent can also defend the contrary claim, so the answer is possible rather than plausible.Source: §1 · p. 4
  • P-SAF generalizes monotonic and non-monotonic logics involving maximal consistent subsets, translates such logics to argumentation, and can encode n-ary conflicts in inconsistent knowledge bases.The paper also investigates how existing argumentation frameworks can be instantiated as P-SAFs.Source: §1 · p. 4
  • The proposed dialogue model acts as a dialectical proof procedure for computing and explaining credulous, grounded, and sceptical acceptance in P-SAFs.The paper reports soundness and completeness with respect to argumentation semantics and represents dialogue explanations as trees.Source: §1 · p. 5

2. Preliminaries

This section establishes a generalized consequence-operator view of abstract logics and defines inconsistency-tolerant entailment via maximal consistent subsets. It illustrates the framework through classical, defeasible, and Datalog± logics.

2. Preliminaries

  • Abstract logics pair formulas with consequence operators; inconsistent-KB reasoning selects maximal consistent subsets and distinguishes possible, plausible, and surest answers.Source: §2 · pp. 5–6

2.1. Classical Logic.

  • Classical logic is represented by a consequence operator, with propositional inference captured one rule at a time and satisfying A1–A5.Source: §2.1 · p. 7

2.2. Defeasible Logic.

  • Defeasible logic derives literals through strict or defeasible rules, optionally their contrapositives, yielding abstract logics whose operators satisfy A1–A3.Source: §2.2 · pp. 7–8

2.3. Datalog±.

  • Datalog± treats TGDs and negative constraints as inference rules; its operator satisfies A1–A2, while A3 holds for guarded and weakly guarded fragments.Source: §2.3 · p. 9

3. Proof-oriented (Logical) Argumentations

This section develops proof-oriented argumentation frameworks and relates their reasoning to maximal consistent subsets and knowledge-base repairs. It also presents explanatory dialogues as dialectical proof procedures for determining and explaining query acceptance.

3.1. Arguments, Collective Attacks and Proof-oriented Argumentations

  • P-SAF arguments are proof trees from fact-premise leaves to a conclusion, and the framework omits extra consistency and minimality restrictions to remain general.The paper presents P-SAFs as an instantiation of structured argumentation frameworks, with arguments represented as trees.Source: §3.1 · pp. 10, 13
  • Collective attacks capture non-binary conflicts that binary attacks cannot express; in the example, three arguments yield extensions containing each pair.The comparison approach uses six arguments and yields extensions containing pairs of single arguments plus a compound argument.Source: §3.1 · pp. 12–13

3.2. Translating the Existing Argumentation Frameworks to P-SAFs

  • P-SAFs simulate sequent-based argumentation and contrapositive ABAs, representing inference-rule derivations as proof trees and translating their attacks.The section also identifies deductive argumentation, DeLP, ASPIC, ASPIC+ without preferences, and ABA as instances of the framework.Source: §3.2 · pp. 13–15

3.3. Acceptability of P-SAFs and Relations to Reasoning with MSCs

  • P-SAF stable and preferred extensions correspond to individual MCSs, while the grounded extension corresponds to their intersection.In general, the grounded extension is contained in the intersection of all MCSs.Source: §3.3 · p. 16
  • Theorem 3.14 equates credulous, sceptical, and grounded acceptance with entailment in some, all, and the intersection of all MCSs, respectively.The paper also states that P-SAFs satisfy rationality postulates.Source: §3.3 · p. 16

3.3. Acceptability of P-SAFs and Relations to Reasoning with MSCs.

  • AFK satisfies consistency and closure under the adm, stb, prf, and grd semantics.Consistency means every extension has consistent conclusions, while closure means its conclusions are closed under CN.Source: §3.3 · p. 16
  • The example’s P-SAF extensions correspond to repairs of the knowledge base, as established by Theorem 3.14.For the example, the stb and prf extensions are E1 through E6.Source: §3.3 · p. 16
  • Under stb and prf extensions, q1 = Re(v) is credulously accepted, making v a possible answer.Source: §3.3 · p. 16
  • The section maps acceptance of a formula to acceptance of arguments concluding that formula, then introduces explanatory dialogues as dialectical proof procedures.The following section uses dialogue models to determine and explain acceptance under argumentation semantics.Source: §3.3 · p. 17

4. Explanatory Dialogue Models

The paper develops P-SAF explanatory dialogues in which proponents and opponents exchange KB formulas, and uses the resulting dialogue trees to explain argument acceptance. Focused dialogue trees connect these concrete disputes to abstract argumentation trees.

4. Explanatory Dialogue Models

  • The P-SAF dialogue model explains formula acceptance through a dispute in which a proponent advances arguments and an opponent challenges the moves.A dialogue where the proponent wins represents a proof that the argument is accepted.Source: §4 · p. 17

4.1. Basic Notions.

  • Utterances form dialogues between two agents, and legal moves offer argument grounds, state supporting facts, or introduce contrary formulas.Utterances target earlier utterances, and the dialogue tree records the exchange as it progresses.Source: §4.1 · pp. 17–18, §4.2 · p. 18

4.2. Dialogue Trees, Dialogues and Focused Sub-dialogues.

  • Dialogue trees represent formulas, inference steps, and attacks; in the researcher example, the dialogue explains how one agent persuades another to accept the query.Nodes distinguish proponent and opponent contributions, while labels indicate whether formulas are facts, inferred, or unexamined.Source: §4.2 · pp. 18–20

4.3. Focused Dialogue Trees.

  • Focused dialogue trees isolate sub-dialogues as subtrees and correspond to abstract dialogue trees, with one proponent argument supporting the root and specified attack patterns.The model uses this correspondence to support results on argument acceptability.Source: §4.3 · p. 20

5. Results of the Paper

The section studies dialogue models and trees as proof procedures for determining and explaining formula acceptance and knowledge-base entailment under argumentation and maximal-consistent-subset semantics. It examines dialogue-tree acceptance, including soundness and completeness of winning conditions and tree forms for different semantics.

5.1. Notions for Soundness and Completeness Results.

  • Potential arguments extracted from dialogue trees correspond to conventional P-SAF arguments for the same conclusion and support.The section also defines attacks between these potential arguments and the P-SAF drawn from the dialogue tree.Source: §5.1 · p. 23

5.2.1. Computing credulous acceptance.

  • Defensive, non-redundant dialogue trees yield sound credulous acceptance under admissible and preferred semantics; the same conditions apply to stable semantics.Defensive trees ensure the proponent’s arguments do not attack themselves, while non-redundancy prevents repeated arguments from sustaining nonterminating dialogues.Source: §5.2.1 · pp. 25–27

5.2.2. Computing grounded acceptance.

  • A defensive, finite dialogue tree makes the dialogue groundedly successful and establishes grounded acceptance of its formula.Credulously successful dialogues alone are not sound for grounded acceptance when dialogue trees can be infinite.Source: §5.2.2 · p. 27

5.2.3. Computing sceptical acceptance.

  • An ideal dialogue tree makes the dialogue sceptically successful and establishes sceptical acceptance under admissible, preferred, or stable semantics.An ideal tree is defensive and non-redundant, and none of its opponent arguments belongs to an admissible set in the dialogue’s P-SAF.Source: §5.2.3 · pp. 27–28

5.3. Completeness Results.

  • Nonterminating argument construction can prevent completeness; under finite top-down argument construction, admissible and preferred credulous acceptance have corresponding successful dialogue trees.For Datalog±, an acyclic dependency graph ensures finite argument construction; the completeness results require admissible-successful or preferred-successful dialogues, respectively.Source: §5.3 · pp. 28–29
  • Grounded acceptance under grd with a groundedly-successful dialogue yields a defensive finite tree drawn from a focused sub-dialogue.This is the completeness result of Theorem 5.23.Source: §5.3 · p. 29
  • Sceptical acceptance under adm, prf, or stb with a sceptically-successful dialogue yields an ideal dialogue tree.This is the completeness result of Theorem 5.24.Source: §5.3 · p. 29

5.4. Results for a Link between Inconsistency-Tolerant Reasoning and Dialogues.

  • KB entailment in some, the intersection of, or all maximal consistent subsets corresponds respectively to defensive non-redundant, defensive finite, or ideal dialogue trees.The section presents this correspondence as a way to determine and explain KB entailment using dialogue trees.Source: §5.4 · p. 29

6. Summary and Conclusion

This section summarizes P-SAF’s use of explanatory dialogues and dialectical proof trees for explaining acceptance under inconsistency-tolerant semantics, and presents formal properties of dialogue-tree constructions, including correspondences with abstract dialogue trees and admissibility-related properties.

6. Summary and Conclusion

  • P-SAF drops minimality and support-consistency conditions, represents arguments as trees, accommodates conflicting assumptions, and uses collective attacks to model n-ary constraints.The paper identifies deductive arguments, DeLP, ASPIC/ASPIC+ without preferences, flat or non-flat ABAs, and sequent-based argumentation as instances of P-SAF.Source: §6 · p. 30
  • The authors claim no framework is universally better, say application needs should guide framework choice, and leave real-data, human-evaluation, and explanation-complexity studies for future work.The paper frames its study as theoretical and proposes empirical and theoretical analysis of explanation-computation complexity.Source: §6 · pp. 30–31
  • P-SAF models logics with maximal consistent subsets and connects argumentation semantics to explanatory dialogues and graphical dialectical proof trees for query acceptance.The paper describes these explanations as more expressive and intuitive than existing formalisms.Source: §6 · p. 31

Appendix A. Preliminaries

  • The soundness and completeness proof strategy links dialogue trees to abstract dialogue trees, then extends Corollary 1 of for completeness.A dialogue may be decomposed into independent focused sub-dialogues, whose dialogue trees are subtrees of the original.Source: Appendix A · p. 31

A.1. Abstract Dialogue Trees and Abstract Dialogue Forests.

  • An abstract dialogue forest for a formula groups the abstract dialogue trees corresponding to its possible arguments with that conclusion.A dialogue tree rooted at a formula may correspond to one, none, or multiple abstract dialogue trees.Source: §A.1 · pp. 31–32

A.2. Partitioning a Dialogue Tree into Focused Substrees.

  • Every focused subtree of a dialogue tree rooted at ϕ is drawn from a focused sub-dialogue of the original dialogue.The appendix also shows that each constructed focused sub-dialogue draws the corresponding subtree.Source: §A.2 · pp. 32–33

A.3. Transformation from Dialogue Trees into Abstract Dialogue Trees.

  • The correspondence principle translates defensive, non-redundant dialogue trees to admissible abstract dialogue trees and back, with defence and culprit sets included in the corresponding sets.The containment relations hold in each direction between the dialogue tree and abstract dialogue tree.Source: §A.3 · p. 33

2. The transformation from abstract dialogue trees into dialogue trees

  • The reverse construction builds a focused subtree of a dialogue tree from an abstract dialogue tree by induction.It uses support and context trees to represent argument support and attacks, including collective attacks.Source: §2 · p. 35
  • The inductive limit T(δi) is defensive and non-redundant, the proponent wins, and its defense and culprit sets are subsets of TG’s.The construction expands opponent nodes with context trees and proponent nodes with support trees when their formula sets are inconsistent with α.Source: §2 · pp. 35–36

A.4. Notions and Results of Acceptance of an Argument from Its Abstract Dialogue Trees.

This section relates success of focused sub-dialogues to argument acceptance under several semantics. It also explains how abstract dialogue results apply to focused sub-dialogues.

A.4. Notions and Results of Acceptance of an Argument from Its Abstract Dialogue Trees.

  • Abstract dialogues can be treated as focused sub-dialogues because their trees correspond to focused subtrees of dialogue trees.The section states this correspondence follows from Lemma A.5 and Theorem A.7.Source: §A.4 · p. 36
  • A focused sub-dialogue is admissible-, preferred-, grounded-, or sceptical-successful according to properties of its abstract dialogue tree.Grounded success requires an admissible, finite tree; sceptical success also requires no admissible tree for the argument labelling any opponent node.Source: §A.4 · p. 36
  • Credulous, grounded, and sceptical acceptance correspond respectively to admissible/preferred-, grounded-, and sceptical-successful focused sub-dialogues.The corollary relates each successful sub-dialogue to acceptance in the corresponding P-SAF semantics.Source: §A.4 · p. 36

Appendix B. Proofs for Section 5.2

The appendix proves results for Section 5.2 by converting dialogue trees into abstract dialogue trees and applying their success criteria.

Appendix B. Proofs for Section 5.2

  • The proof strategy partitions a dialogue tree for ϕ into subtrees drawn from focused sub-dialogues.This partition is attributed to Lemma A.5.Source: Appendix B · p. 37
  • The correspondence principle transfers each focused subtree into an abstract dialogue tree.The transfer is attributed to Theorem A.7.Source: Appendix B · p. 37
  • The proofs apply Definition A.10 and Corollary A.11 for abstract dialogue trees to establish soundness.The cited criteria are described as analogous to Definition 9 and Corollary 1 in.Source: Appendix B · p. 37

B.1. Proof of Theorem 5.14.

The proof shows that a defensive, non-redundant focused dialogue tree yields admissible success and credulous acceptance. It establishes this through the corresponding abstract dialogue tree.

B.1. Proof of Theorem 5.14.

  • A defensive, non-redundant focused dialogue tree makes its sub-dialogue admissible-successful and ϕ credulously accepted under admissible semantics.The proof states the result for the P-SAF drawn from the dialogue.Source: §B.1 · pp. 37–38
  • The proof maps each focused subtree to an abstract dialogue tree and takes its proponent arguments as the set B.The subtrees are focused by Lemma A.5, and the correspondence principle is attributed to Theorem A.7.Source: §B.1 · p. 37
  • The proponent arguments in B defend against every attack and do not attack themselves, making the abstract tree admissible.Defensiveness and the absence of self-attacks are established from the focused tree's properties.Source: §B.1 · p. 37
  • Non-redundancy prevents an argument in the abstract tree from labelling both a proponent and opponent node.The proof combines this condition with admissibility to establish admissible success.Source: §B.1 · p. 37

B.2. Proof of Theorem 5.17.

The proof establishes grounded acceptance when a focused dialogue tree is defensive and finite. Its argument uses a finiteness characterization and lifts groundedness from the focused tree to the full dialogue.

B.2. Proof of Theorem 5.17.

  • An abstract dialogue tree is finite exactly when its proponent-labelled arguments form a subset of the grounded set.This equivalence is the stated lemma used in the proof.Source: §B.2 · p. 38
  • In a finite P-SAF, ranks of grounded arguments guide construction of dialogue trees whose branches have finite length.The proof states that decreasing ranks make branches finite and that finiteness of the P-SAF makes the tree finite in breadth.Source: §B.2 · pp. 38–39
  • A defensive, finite focused dialogue tree makes its sub-dialogue grounded-successful and ϕ groundedly accepted.The acceptance is in the grounded semantics of the P-SAF drawn from the dialogue.Source: §B.2 · p. 39
  • The defensive focused tree corresponds to an abstract tree whose proponent arguments are grounded, yielding grounded success for the focused sub-dialogue.The proof uses the finite-tree characterization to establish groundedness of those arguments.Source: §B.2 · p. 39
  • Groundedness then carries from each focused tree to the full dialogue's abstract dialogue forest.The proof relies on trees in the forest having separate sets of proponent arguments.Source: §B.2 · p. 39

B.3. Proof of Theorem 5.19.

Theorem 5.19 connects an ideal dialogue tree with a sceptically successful dialogue and sceptical acceptance of its formula under the stated argumentation semantics.

B.3. Proof of Theorem 5.19.

  • An ideal dialogue tree yields a sceptically-successful dialogue and sceptical acceptance of ϕ under adm, prf, or stb in AFδ.The acceptance is supported by DE(T(δ)).Source: §B.3 · p. 39
  • The proof uses the correspondence principle to transfer focused subtrees of the ideal dialogue tree to abstract dialogue trees.The subtrees remain ideal and therefore defensive.Source: §B.3 · pp. 39–40
  • For admissible semantics, the proof establishes admissibility and excludes admissible opponent arguments, yielding sceptical success and acceptance.The preferred and stable cases are stated to be analogous.Source: §B.3 · pp. 39–40

Appendix C. Proofs for Section 5.3

Appendix C proves completeness by connecting focused sub-dialogues to abstract dialogue trees and transferring those trees back to dialogue trees.

Appendix C. Proofs for Section 5.3

  • Completeness is proved by partitioning a dialogue into focused sub-dialogues, obtaining abstract dialogue trees for them, and transferring those trees back to dialogue trees.The transfer uses the correspondence principle and Theorem A.7.Source: Appendix C · p. 40

C.1. Preliminaries.

  • The completeness preliminaries extend Corollary A.11, with preferred success following from admissible success and the extension result for admissible arguments.The grounded-successful and sceptical-successful statements are described as generalizations of prior results and.Source: §C.1 · pp. 40–41
  • Corollary C.1 links acceptance in AFK to a successful focused sub-dialogue: admissible or preferred for credulous acceptance, grounded for grounded acceptance, and sceptical for acceptance in all preferred extensions.The proof uses correspondence between focused dialogue subtrees and abstract dialogue trees.Source: §C.1 · p. 40

C.2. Proof of Theorem 5.21.

Theorem 5.21 establishes that credulous admissible acceptance together with admissible success yields a defensive, non-redundant dialogue tree from a focused sub-dialogue.

C.2. Proof of Theorem 5.21.

  • Credulous admissible acceptance of ϕ and admissible success of δ guarantee a defensive, non-redundant dialogue tree for ϕ from a focused sub-dialogue.The theorem states that the acceptance is supported by DE(T(δ)).Source: §C.2 · p. 41
  • Corollary C.1 supplies an admissible-successful focused sub-dialogue from the assumed credulous acceptance.The proof then obtains an admissible abstract dialogue tree and transfers it by the correspondence principle.Source: §C.2 · p. 41
  • The corresponding dialogue tree is defensive and non-redundant because its abstract dialogue tree is admissible.Source: §C.2 · p. 41

C.3. Proof of Theorem 5.23.

Theorem 5.23 establishes that grounded acceptance together with grounded success yields a defensive, finite dialogue tree from a focused sub-dialogue.

C.3. Proof of Theorem 5.23.

  • Grounded acceptance of ϕ and grounded success of δ guarantee a defensive, finite dialogue tree for ϕ from a focused sub-dialogue.The theorem states that the acceptance is supported by DE(T(δ)).Source: §C.3 · p. 41
  • Corollary C.1 provides a grounded-successful focused sub-dialogue, from which the proof constructs an admissible, finite abstract dialogue tree.The correspondence principle transfers that abstract tree to a dialogue tree.Source: §C.3 · p. 41
  • The transferred dialogue tree is finite because its corresponding abstract dialogue tree is finite.Source: §C.3 · p. 42

C.4. Proof of Theorem 5.24.

Theorem 5.24 concludes that skeptical acceptance under admissible, preferred, or stable semantics, together with skeptical success, yields an ideal dialogue tree for the formula. The proof establishes the admissible case and states that the preferred and stable cases are analogous.

C.4. Proof of Theorem 5.24.

  • Skeptical acceptance under admissible, preferred, or stable semantics and skeptical success imply an ideal dialogue tree for the formula.The proof treats admissible semantics; preferred and stable semantics are handled analogously.Source: §C.4 · p. 42
  • For focused sub-dialogues, skeptical success supplies abstract dialogue trees that are admissible and have no opponent node with an admissible abstract dialogue tree.The proof then uses the correspondence principle to obtain corresponding dialogue trees.Source: §C.4 · p. 42
  • The corresponding dialogue trees must be defensive and non-redundant, with no opponent arguments belonging to an admissible set of potential arguments.The proof uses these conditions to establish ideality.Source: §C.4 · p. 42
Loading 2502.11291v1…