Vol-3197/short2

Paper

Paper
edit
description	scientific paper published in CEUR-WS Volume 3197
id	Vol-3197/short2
wikidataid	Q117341470→Q117341470
title	Abductive Reasoning with Sequent-Based Argumentation
pdfUrl	https://ceur-ws.org/Vol-3197/short2.pdf
dblpUrl	https://dblp.org/rec/conf/nmr/ArieliBHS22
volume	Vol-3197→Vol-3197
session	→

Freitext

Abductive Reasoning with Sequent-Based Argumentation

Abductive Reasoning with Sequent-Based Argumentation
(Extended Abstract)

Ofer Arieli1 , AnneMarie Borg2 , Matthis Hesse3 and Christian Straßer3
1
  School of Computer Science, Tel-Aviv Academic College, Israel
2
  Department of Information and Computing Sciences, Utrecht University, The Netherlands
3
  Institute for Philosophy II, Ruhr University Bochum, Germany


                                             Abstract
                                             We show that logic-based argumentation, and in particular sequent-based frameworks, is a robust argumentative setting for
                                             abductive reasoning and explainable artificial intelligence.


1. Introduction                                                                                                                       monotonic (if 𝒮 ′ ⊢ 𝜑 and 𝒮 ′ ⊆ 𝒮, then 𝒮 ⊢ 𝜑), and tran-
                                                                                                                                      sitive (if 𝒮 ⊢ 𝜑 and 𝒮 ′ , 𝜑 ⊢ 𝜓 then 𝒮, 𝒮 ′ ⊢ 𝜓).
Abduction is the process of deriving a set of explanations
                                                                                                                                      ∙ The language L contains at least a ⊢-negation opera-
of a given observation relative to a set of assumptions.
                                                                                                                                      tor ¬, satisfying 𝑝 ̸⊢ ¬𝑝 and ¬𝑝 ̸⊢ 𝑝 (for atomic 𝑝), and
The systematic study of abductive reasoning goes back
                                                                                                                                      a ⊢-conjunction operator ∧, for⋀︀    which 𝒮 ⊢ 𝜓 ∧ 𝜑 iff
to Peirce (see [1]). Abduction is closely related to ‘in-
                                                                                                                                      𝒮 ⊢ 𝜓 and 𝒮 ⊢ 𝜑. We denote by Γ the conjunction of
ference to the best explanation (IBE)’ [2]. However, it is
                                                                                                                                      the formulas in Γ. We sometimes assume the availability
often distinguished from the latter in that abductive infer-
                                                                                                                                      of a deductive implication →, satisfying 𝒮, 𝜓 ⊢ 𝜑 iff
ence may provide explanations that are not known as the
                                                                                                                                      𝒮 ⊢ 𝜓 → 𝜑.
best explanation available, but that are merely worthy of
                                                                                                                                         A set 𝒮 of formulas is ⊢-consistent, if there are no
conjecturing or entertaining (see, e.g., [3, 4, 5]).
                                                                                                                                      formulas 𝜑1 , . . . , 𝜑𝑛 ∈ 𝒮 for which ⊢ ¬(𝜑1 ∧ · · · ∧ 𝜑𝑛 ).
   In this work, we model abduction (not in the strict
sense of IBE) by computational argumentation, and show                                                                                ∙ Arguments based on a logic L = ⟨L, ⊢⟩ are single-
that sequent-based argumentation frameworks [6, 7] are                                                                                conclusioned L-sequents [8], i.e., expressions of the form
a solid argumentative base for abductive reasoning. Ac-                                                                               Γ ⇒ 𝜓, where ⇒ is a symbol that does not appear in L,
cording to our approach, abductive explanations are han-                                                                              and such that Γ ⊢ 𝜓. Γ is called the argument’s support
dled by ingredients of the framework, and so different                                                                                (also denoted Supp(Γ ⇒ 𝜓)) and 𝜓 is its conclusion
considerations and principles concerning those explana-                                                                               (denoted Conc(Γ ⇒ 𝜓)). An 𝒮-based argument is an L-
tions are expressed within the framework. The advantages                                                                              argument Γ ⇒ 𝜓, where Γ ⊆ 𝒮. We denote by ArgL(𝒮)
of this are discussed in the last section of the paper.                                                                               the set of the L-arguments that are based on 𝒮.
                                                                                                                                         We distinguish between two types of premises: a ⊢-
                                                                                                                                      consistent set 𝒳 of strict premises, and a set 𝒮 of defea-
2. Sequent-Based Argumentation                                                                                                        sible premises. We write Arg𝒳 L (𝒮) for ArgL(𝒳 ∪ 𝒮).

We denote by L a propositional language. Atomic formu-                                                                                ∙ Attack rules are sequent-based inference rules for rep-
las in L are denoted by 𝑝, 𝑞, 𝑟, formulas are denoted by                                                                              resenting attacks between sequents. Such rules consist
𝜑, 𝜓, 𝛿, 𝛾, 𝜖, sets of formulas are denoted by 𝒳 , 𝒮, ℰ, and                                                                          of an attacking argument (the first condition of the rule),
finite sets of formulas are denoted by Γ, ∆, Π, Θ, all of                                                                             an attacked argument (the last condition of the rule), con-
which can be primed or indexed. The set of atomic formu-                                                                              ditions for the attack (the other conditions of the rule)
las appearing in the formulas of 𝒮 is denoted Atoms(𝒮).                                                                               and a conclusion (the eliminated attacked sequent). The
The set of the (well-formed) formulas of L is denoted                                                                                 elimination of Γ ⇒ 𝜑 is denoted by Γ ̸⇒ 𝜑.
WFF(L), and its power set is denoted ℘(WFF(L)).                                                                                          Given a set 𝒳 of strict (non-attacked) formulas, we
                                                                                                                                      shall concentrate here on the following two attack rules:
∙ The base logic is an arbitrary propositional logic,
namely a pair L = ⟨L, ⊢⟩ consisting of a language L Direct Defeat (for 𝛾 ̸∈ 𝒳 ):
and a consequence relation ⊢ on ℘(WFF(L))×WFF(L).                         Γ1 ⇒ 𝜓1 𝜓1 ⇒ ¬𝛾 Γ2 , 𝛾 ⇒ 𝜓2
The relation ⊢ is assumed to be reflexive (𝒮 ⊢ 𝜑 if 𝜑 ∈ 𝒮),                       Γ2 , 𝛾 ̸⇒ 𝜓2
                                                                                                                                      Consistency Undercut (for Γ2 ̸= ∅, Γ2 ∩𝒳 = ∅, Γ1 ⊆𝒳 ):
                                                                                                                                                                                      Γ2 , Γ′2 ⇒ 𝜓
                                                                                                                                                                            ⋀︀
NMR 2022: 20th International Workshop on Non-Monotonic Reasoning,                                                                                                  Γ1 ⇒ ¬        Γ2
August 7-9, 2022, Haifa, Israel
                                       © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License                                        Γ2 , Γ′2 ̸⇒ 𝜓
                                       Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)




                                                                                                                                143
�Direct Defeat (DirDef) indicates that if the conclusion                     E1                              E2
(𝜓1 ) of the attacker entails the negation of a formula (𝛾)
                                                                  clear_skies ⇒ clear_skies             rainy ⇒ rainy
in the support of an argument, the latter is eliminated.
When Γ1 = ∅, consistency undercut (ConUcut) elimi-                      clear_skies,                        rainy,
                                                                    clear_skies → ¬rainy             rainy → ¬sprinklers
nates an argument with an inconsistent support.                           ⇒ ¬rainy                      ⇒ ¬sprinklers

∙ A (sequent-based) argumentation framework (AF),                                                            rainy,
based on the logic L and the attack rules in AR, for a set                                           clear_skies → ¬rainy

of defeasible premises 𝒮 and a ⊢-consistent set of strict                   wet_grass ⇐
                                                                                                        ⇒ ¬clear_skies

premises 𝒳 , is a pair AFL,AR (𝒮) = ⟨ArgL (𝒮), A⟩ where
                            𝒳                 𝒳
                                                                             [sprinkler],                    rainy,
                                                                       sprinklers → wet_grass          rainy → wet_grass
A ⊆ Arg𝒳  L  (𝒮)×Arg   𝒳
                       L  (𝒮) and (𝑎1 , 𝑎 2 ) ∈ A iff there  is a                                         ⇒ wet_grass
rule R𝒳 ∈ AR, such that 𝑎1 R𝒳 -attacks 𝑎2 . We shall use
AR and A interchangeably, denoting both of them by A. Figure 1: Part of the AF of Example 1 (without the gray node)
∙ Semantics of sequent-based frameworks are defined as and of Example 2 (with the gray node).
usual by Dung-style extensions [9]: Let AF = AF𝒳         L,A (𝒮)
= ⟨Arg𝒳  L  (𝒮), A⟩  be  an AF  and  let  E   ⊆  Arg  𝒳
                                                      L (𝒮).    E
attacks 𝑎 if there is an 𝑎′ ∈ E such that (𝑎′ , 𝑎) ∈ A. E
defends 𝑎 if E attacks every attacker of 𝑎, and E is conflict- (since the argument rainy, rainy → wet_grass ⇒
free (cf) if for no 𝑎1 , 𝑎2 ∈ E it holds that (𝑎1 , 𝑎2 ) ∈ A. wet_grass is in E2 ), but it is not skeptically deducible
E is admissible if it is conflict-free and defends all of (there is no 𝑎 ∈ E1 such that Conc(𝑎) = wet_grass).
its elements. A complete (cmp) extension of AF is an
admissible set that contains all the arguments that it
defends. The grounded (grd) extension of AF is the ⊆-
minimal complete extension of Arg𝒳
                                                                  3. Abductive Reasoning
                                      L (𝒮), a preferred (prf)
extension of AF is a ⊆-maximal complete extension of For supporting abductive explanations in sequent-based
Arg𝒳 L (𝒮), and a stable (stb) extension of AF is a conflict- argumentation, we introduce abductive sequents, which
free set in Arg𝒳 L (𝒮) that attacks every argument not in         are expressions of the form 𝜑 ⇐ Γ, [𝜖], intuitively mean-
it.1 We denote by Extsem (AF) the set of all the extensions ing that ‘(the explanandum) 𝜑 may be inferred from Γ,
of AF of type sem.                                                assuming that 𝜖 holds’. While Γ ⊆ 𝒮 ∪ 𝒳 , 𝜖 may not be
∙ Entailments of AF = AF𝒳                     𝒳
                              L,A (𝒮) = ⟨ArgL (𝒮), A⟩        an assumption, but rather a hypothetical explanation of
with respect to a semantics sem are defined as follows:      the conclusion.
∘ Skeptical⋂︀entailment: 𝒮 |∼∩,sem   𝜑  if there is an argu-   Abductive sequents are produced by the following rule
                               L,A,𝒳
ment 𝑎 ∈ Extsem (AF) such that Conc(𝑎) = 𝜑.                  that models abduction as ‘backwards reasoning’:

                                       L,A,𝒳 𝜑 if for every
∘ Weakly skeptical entailment: 𝒮 |∼⋒,sem                                                                  𝜖, Γ ⇒ 𝜑
                                                             • Abduction:
extension E ∈ Extsem (AF) there is an argument 𝑎 ∈ E                                                      𝜑 ⇐ Γ, [𝜖]
such that Conc(𝑎) = 𝜑.
                               ∪,sem                           This rule allows us to produce abductive sequents like
∘ Credulous ⋃︀entailment: 𝒮 |∼L,A,𝒳 𝜑 iff there is an argu- wet_grass ⇐ [sprinklers], sprinklers → wet_
ment 𝑎 ∈ Extsem (AF) such that Conc(𝑎) = 𝜑.                  grass that provides an explanation to wet_grass.
Example 1. Consider a sequent-based AF, based on               Since abductive reasoning is a form of non-monotonic
classical logic CL and the set 𝒮 of defeasible assumptions: reasoning, we need a way to attack abductive sequents.
                                                             To this end, we consider rules like those from Section 2:
  ⎨ clear_skies, rainy, clear_skies → ¬rainy, ⎬
  ⎧                                                     ⎫

    rainy → ¬sprinklers, rainy → wet_grass,               • Abductive Direct Defeat (for 𝛾 ∈ (Γ2 ∪ {𝜖}) ∖ 𝒳 ):
    sprinklers → wet_grass
  ⎩                                           ⎭
                                                                             Γ1 ⇒ 𝜑1 𝜑1 ⇒ ¬𝛾 𝜑2 ⇐ [𝜖], Γ2
  Suppose further that 𝒳 = ∅ and the attack rules are                                   𝜑2 ̸⇐ [𝜖], Γ2
DirDef and ConUcut. Then, for instance, the arguments
                                                          Note that this attack rule assures, in particular, the con-
𝑎1 : clear_skies, clear_skies → ¬rainy ⇒ ¬rainy
                                                          sistency of explanations with the strict assumptions, thus
𝑎2 : rainy, clear_skies → ¬rainy ⇒ ¬clear_skies
                                                          it renders the following rule admissible:
DirDef-attack each other. There are two stable/preferred
extensions E1 and E2 , where 𝑎1 ∈ E1 and 𝑎2 ∈ E2 (see • Consistency (for Γ ⊆ 𝒳 ): Γ1 ⇒ ¬𝜖 𝜑 ⇐ [𝜖], Γ2
                                                                                1
Fig. 1). Thus, with respect to stable or preferred seman-                                        𝜑 ̸⇐ [𝜖], Γ2
tics, wet_grass credulously follows from the framework
                                                             Abductive explanations should meet certain require-
1
  For an in-depth discussion of extension types see [10]. ments to ensure their behavior (see, e.g., [11]). Below,




                                                           144
�we express some of the common properties in terms of           ∘ weakly-skeptical sem-explanation of 𝜑, if in every sem-
attack rules that may be added to the framework.               extension
                                                                     ⋀︀ of AAFL,A⋆(𝒮) there is an abductive argument
                                                                                 𝒳

                                                               𝜑 ⇐ [ ℰ], Γ for some Γ ⊆ 𝒮.
                                      ⊢ 𝜖 → 𝜑 𝜑 ⇐ [𝜖]
• Non Vacuousity:                                              ∘ credulous sem-explanation  of 𝜑, if there is Γ ⊆ 𝒮
                                           𝜑 ̸⇐ [𝜖]
                                                               such that 𝜑 ⇐ [ ℰ], Γ is in some sem-extension of
                                                                                 ⋀︀
This rule prevents self-explanations. Thus, in the running     AAF𝒳 L,A⋆(𝒮).
example, wet_grass ⇐ [wet_grass] is excluded.
                                                           Example 2. As mentioned, the abductive sequent wet_
• Minimality:                                              grass ⇐ [sprinklers], sprinklers → wet_grass
      𝜑 ⇐ [𝜖1 ], Γ 𝜖2 ⇒ 𝜖1 𝜖1 ̸⇒ 𝜖2 𝜑 ⇐ [𝜖2 ], Γ           is producible by Abduction from the sequent-based frame-
                                                           work in Example 1, and belongs to a stable/preferred
                      𝜑 ̸⇐ [𝜖2 ], Γ                        extension of the related abductive sequent-based frame-
This rule assures the generality of explanations. Thus, in work (see again Fig. 1). Therefore, sprinklers is a cred-
our example, sprinklers ∧ irrelevant_fact should ulous (but not [weakly] skeptical) stb/prf-explaination
not explain wet_grass, since sprinklers is a more gen- of wet_grass.
eral and so more relevant explanation.                     Example 3. Let L = CL, A = {DirDef, ConUcut}
                                  Γ1 ⇒ 𝜑 𝜑 ⇐ [𝜖], Γ2                 with 𝒮 = {𝑝, ¬𝑝 ∧ 𝑞} and 𝒳 = {𝑞 ∧ 𝑟 → 𝑠}. For sem ∈
• Defeasible Non-Idleness:                                           {stb, prf}, 𝑞 ∧ 𝑟 is a weakly-skeptical sem-explanation
                                      𝜑 ̸⇐ [𝜖], Γ2
                                                                     of 𝑠, since the corresponding abductive framework has
                                        Γ1 ⇒ 𝜑 𝜑 ⇐ [𝜖], Γ2           two sem-extensions, one with 𝑠 ⇐ [𝑞 ∧ 𝑟], 𝑝, 𝑞 ∧ 𝑟 → 𝑠
• Strict Non-Idleness (Γ1 ⊆ 𝒳 ):
                                               𝜑 ̸⇐ [𝜖], Γ2          and the other with 𝑠 ⇐ [𝑞 ∧ 𝑟], ¬𝑝 ∧ 𝑞, 𝑞 ∧ 𝑟 → 𝑠. This
                                                                     holds also when the non-vacuousity or the strict non-
The two rules above assure that assumptions shouldn’t al- idleness attack rules are part of the framework. However,
ready explain the explanandum. Defeasible non-idleness 𝑞 ∧ 𝑟 is no longer a weakly-skeptical sem-explanation of
rules out explaining wet_grass by sprinklers, since 𝑠 when minimality attack is added, since the extension
the former is already inferred from the defeasible assump- that contains 𝑠 ⇐ [𝑞 ∧ 𝑟], ¬𝑝 ∧ 𝑞, 𝑞 ∧ 𝑟 → 𝑠 includes a
tions (assuming that it is rainy), while strict non-idleness minimality attacker, 𝑠 ⇐ [𝑟], ¬𝑝 ∧ 𝑞, 𝑞 ∧ 𝑟 → 𝑠.
allows this alternative explanation (wet_grass cannot
be inferred from the strict assumptions). These two at- Example 4. Consider now 𝒮 = {𝑝 ∧ 𝑞, ¬𝑝 ∧ 𝑞}. This
tack rules are particularly interesting when abductive time, with minimality, 𝑞 ∧ 𝑟 is not even a credulous
reasoning is used to generate novel hypotheses explain- sem-explanation of 𝑠 (sem ∈ {stb, prf}), since each of
ing observations that are not already explained by a given the two sem-extensions contains a minimality attacker
theory resp. the given background assumptions.2                      (𝑠 ⇐ [𝑟], 𝑝∧𝑞, 𝑞 ∧𝑟 → 𝑠 or 𝑠 ⇐ [𝑟], ¬𝑝∧𝑞, 𝑞 ∧𝑟 → 𝑠).
                                                                     So, 𝑞 ∧ 𝑟, unlike 𝑟, does not sem-explain 𝑠.
    Next, we adapt sequent-based argumentation frame-
works to an abductive setting, using abductive sequents,
the new inference rule, and additional attack rules.                 4. Discussion and Conclusion
    Given a sequent-based framework AF𝒳             L,A (𝒮), an  ab-
                                                                     Abduction has been widely applied in different deduc-
ductive sequent-based framework AAF𝒳           L,A⋆(𝒮) is construc-
ted by adding to the arguments in ArgL (𝒮) also abduc- tive systems (such as adaptive logics [12]) and AI-based
                                                 𝒳

tive arguments, produced by Abduction, and where A⋆ is disciplines (e.g., logic programing [13]), including in the
obtained by adding to the attack rules in A also (some of) context of formal argumentation (see the survey in [14]).
the rules for maintaining explanations that are described               This ongoing work offers several novelties. In terms
above. Explanations are then defined as follows:                     of knowledge representation we transparently represent
                                                                     abductive inferences by an explicit inference rule that
Definition 1. Let AAF𝒳         L,A⋆(𝒮) be an abductive sequent- produces abductive arguments. The latter are a new type
based argumentation framework as described above. A of hypothetical arguments that are subjected to poten-
finite set ℰ of L-formulas is called:                                tial defeats. Specifically designed attack rules address
                                                                     the quality of the offered explanation and thereby model
         ⋀︀ sem-explanation of 𝜑, if there is Γ 𝒳⊆ 𝒮 s.t. critical questions [15] and meta-argumentative reason-
∘ skeptical
𝜑 ⇐ [ ℰ], Γ is in every sem-extension of AAFL,A⋆(𝒮).
                                                                     ing [16]. This is both natural and philosophically moti-
2
  In some accounts of abduction, e.g. [5], it is argued that the ab- vated, as argued in [17]. Our framework offers a high
  ductively inferred 𝜖 should be of lesser epistemic status than the degree of modularity, and may be based on a variety of
  reasoner’s starting point and so “the fundamental conceptual fact
  about abduction is that abduction is ignorance-preserving reason- propositional logics. Desiderata on abductive arguments
  ing” (p. 40). Our attack rules ensure that the reasoner faces what can be disambiguated in various ways by simply chang-
  Gabbay & Woods call an ‘ignorance problem’ (p. 42, Def. 3.2).      ing the attack rules, all in the same base framework.




                                                            145
�References                                                     of explanatory hypotheses: an argumentative ap-
                                                               proach, Logic Journal of the IGPL 29(4) (2021) 523–
 [1] C. S. Peirce, The Collected Papers of Charles             535.
     Sanders Peirce, Vol. I: The Principles of Philosophy,
     Harvard University Press, Cambridge, 1931.
 [2] P. Lipton, Inference to the Best Explanation, Rout-
     ledge, 2004. 2nd edition.
 [3] S. Yu, F. Zenker, Peirce knew why abduction isn’t
     IBE — A scheme and critical questions for abductive
     argument, Argumentation 32 (2017) 569–587.
 [4] G. Minnameier, Peirce-suit of truth – Why infer-
     ence to the best explanation and abduction ought
     not to be confused, Erkenntnis 60 (2004) 75–105.
 [5] D. Gabbay, J. Woods, The reach of abduction. A
     practical logic of cognitive systems, North-Holland,
     2005.
 [6] O. Arieli, C. Straßer, Sequent-based logical argu-
     mentation, Argument & Computation 6 (2015) 73–
     99.
 [7] A. Borg, Assumptive sequent-based argumenta-
     tion, Journal of Applied Logics – IfCoLog Journal
     of Logics and Their Applications 7 (2020) 227–294.
 [8] G. Gentzen, Untersuchungen über das logische
     schließen I, II, Mathematische Zeitschrift 39 (1934)
     176–210, 405–431.
 [9] P. M. Dung, On the acceptability of arguments and
     its fundamental role in nonmonotonic reasoning,
     logic programming and n-person games, Artificial
     Intelligence 77 (1995) 321–357.
[10] P. Baroni, M. Caminada, M. Giacomin, Abstract
     argumentation frameworks and their semantics, in:
     P. Baroni, D. Gabbay, M. Giacomin, L. van der Torre
     (Eds.), Handbook of Formal Argumentation, vol-
     ume 1, College Publications, 2018, pp. 159–236.
[11] J. Meheus, L. Verhoeven, M. Van Dyck, D. Provijn,
     Ampliative adaptive logics and the foundation of
     logic-based approaches to abduction, Logical and
     Computational Aspects of Model-Based Reasoning
     25 (2002) 39–71.
[12] J. Meheus, D. Batens, A formal logic for abductive
     reasoning, Logic Journal of the IGPL 14 (2006) 221–
     236.
[13] M. Denecker, A. Kakas, Abduction in logic pro-
     gramming, in: Computational Logic: Logic Pro-
     gramming and Beyond, LNCS 2407, Springer, 2002,
     pp. 402–436.
[14] K. Cyras, A. Rago, E. Albini, P. Baroni, F. Toni, Ar-
     gumentative XAI: A survey, in: Proc. 30th IJCAI,
     2021, pp. 4392–4399.
[15] D. Walton, C. Reed, F. Macagno, Argumentation
     Schemes, Cambridge University Press, 2008.
[16] G. Boella, D. Gabbay, L. van der Torre, S. Villata,
     Meta-argumentation modelling I: Methodology and
     techniques, Studia Logica 93 (2009) 297–355.
[17] P. Olmos, Abduction and comparative weighing




                                                         146
�