Vol-3197/short2
Wolfgang Fahl
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
Paper[edit]
| 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[edit]
Abductive Reasoning with Sequent-Based Argumentation[edit]
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
�
Abductive Reasoning with Sequent-Based Argumentation[edit]
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
�