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