Abductive Reasoning with Sequent-Based Argumentation

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. Abduction is the process of deriving a set of explanations of a given observation relative to a set of assumptions. ∙ The language L contains at least a ⊢-negation operator ¬, satisfying ̸⊢ ¬ and ¬ ̸⊢ (for atomic ), and a ⊢-conjunction operator ∧, for which ⊢ ∧ if ⊢ and ⊢ . We denote by ⋀︀Γ the conjunction of the formulas in Γ . We sometimes assume the availability of a deductive implication →, satisfying , ⊢ if ⊢ → . A set of formulas is ⊢-consistent, if there are no formulas 1, . . . , ∈ for which ⊢ ¬(1 ∧ · · · ∧ ).

1. Introduction

monotonic (if ′ ⊢ and ′ ⊆ , then ⊢ ), and transitive (if ⊢ and ′, ⊢ then , ′ ⊢ ).

2. Sequent-Based Argumentation

We denote by L a propositional language. Atomic formu- ∙ Attack rules are sequent-based inference rules for replas 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), ifnite sets of formulas are denoted by Γ , ∆ , Π , Θ , all of an attacked argument (the last condition of the rule), conwhich 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:

We distinguish between two types of premises: a ⊢consistent set of strict premises, and a set of defeasible premises. We write ArgL () for ArgL( ∪ ). ∙ The base logic is an arbitrary propositional logic, namely a pair L = ⟨L, ⊢⟩ consisting of a language L and a consequence relation ⊢ on ℘(WFF(L)) × WFF(L).

The relation ⊢ is assumed to be reflexive ( ⊢ if ∈ ),

Direct Defeat (for ̸∈ ): Γ1 ⇒ 1 1 ⇒ ¬ Γ2, ̸⇒ 2

Γ2, ⇒ 2 Consistency Undercut (for Γ 2 ̸= ∅, Γ 2 ∩ = ∅, Γ 1⊆ ): Γ1 ⇒ ¬ ⋀︀ Γ2

Γ2, Γ′2 ⇒ Γ2, Γ′2 ̸⇒ ∙ Entailments of AF = AFL,A() = ⟨ArgL (), A⟩ with respect to a semantics sem are defined as follows: ∙ Semantics of sequent-based frameworks are defined as usual by Dung-style extensions [ 9 ]: Let AF = AFL,A() = ⟨ArgL (), A⟩ be an AF and let E ⊆ ArgL (). 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 ⊆ - 3. Abductive Reasoning minimal complete extension of ArgL (), a preferred (prf) extension of AF is a ⊆ -maximal complete extension of ArgL (), and a stable (stb) extension of AF is a conflictfree set in ArgL () that attacks every argument not in it.1 We denote by Extsem(AF) the set of all the extensions of AF of type sem.

For supporting abductive explanations in sequent-based argumentation, we introduce abductive sequents, which are expressions of the form ⇐ Γ , [ ], intuitively meaning that ‘(the explanandum) may be inferred from Γ , assuming that holds’. While Γ ⊆ ∪ , may not be an assumption, but rather a hypothetical explanation of the conclusion.

Abductive sequents are produced by the following rule that models abduction as ‘backwards reasoning’: 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: ∩,sem if there is an argu∘ Skeptical entailment: |∼ L,A, ment ∈ ⋂︀ Extsem(AF) such that Conc() = .

⋒,sem if for every ∘ Weakly skeptical entailment: |∼ L,A, extension E ∈ Extsem(AF) there is an argument ∈ E such that Conc() = .

∪,sem if there is an argu∘ Credulous entailment: |∼ L,A, ment ∈ ⋃︀ Extsem(AF) such that Conc() = .

⎧ clear_skies, rainy, clear_skies → ¬rainy, ⎫ ⎨ rainy → ¬sprinklers, rainy → wet_grass, ⎬ ⎩ sprinklers → wet_grass ⎭ Suppose further that = ∅ and the attack rules are DirDef and ConUcut. Then, for instance, the arguments 1 : clear_skies, clear_skies → ¬rainy ⇒ ¬rainy 2 : rainy, clear_skies → ¬rainy ⇒ ¬clear_skies DirDef-attack each other. There are two stable/preferred extensions E1 and E2, where 1 ∈ E1 and 2 ∈ E2 (see Fig. 1). Thus, with respect to stable or preferred semantics, wet_grass credulously follows from the framework 1For an in-depth discussion of extension types see [ 10 ]. • Abduction:

This rule allows us to produce abductive sequents like wet_grass ⇐ [sprinklers], sprinklers → wet_ grass that provides an explanation to wet_grass.

, Γ ⇒ ⇐ Γ , [ ] • Abductive Direct Defeat (for ∈ (Γ 2 ∪ { }) ∖ ): Γ 1 ⇒ 1 1 ⇒ ¬ 2 ⇐ [ ], Γ 2

2 ⇍ [ ], Γ 2 Note that this attack rule assures, in particular, the consistency of explanations with the strict assumptions, thus it renders the following rule admissible: • Consistency (for Γ 1 ⊆ ): Γ 1 ⇒ ¬ ⇍ [ ], Γ 2

⇐ [ ], Γ 2

Abductive explanations should meet certain require

ments to ensure their behavior (see, e.g., [ 11 ]). Below, Direct Defeat (DirDef) indicates that if the conclusion ( 1) of the attacker entails the negation of a formula ( ) in the support of an argument, the latter is eliminated.

When Γ 1 = ∅, consistency undercut (ConUcut) eliminates an argument with an inconsistent support. ∙ A (sequent-based) argumentation framework (AF), based on the logic L and the attack rules in AR, for a set of defeasible premises and a ⊢-consistent set of strict premises , is a pair AFL,AR() = ⟨ArgL (), A⟩ where A ⊆ ArgL ()× ArgL () and (1, 2) ∈ A if there is a rule R ∈ AR, such that 1 R -attacks 2. We shall use AR and A interchangeably, denoting both of them by A. clear_skies ⇒ clear_skies

clear_skies, clear_skies → ¬rainy ⇒ ¬rainy rainy ⇒ rainy

rainy, rainy → ¬sprinklers ⇒ ¬sprinklers

rainy, clear_skies → ¬rainy ⇒ ¬clear_skies we express some of the common properties in terms of ∘ weakly-skeptical sem-explanation of , if in every semattack 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

AAFL,A⋆().

This rule prevents self-explanations. Thus, in the running 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 framework in Example 1, and belongs to a stable/preferred ⇍ [ 2], Γ extension of the related abductive sequent-based frameThis rule assures the generality of explanations. Thus, in work (see again Fig. 1). Therefore, sprinklers is a credour 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: ⇍ [ ], Γ 2 {stb, prf}, ∧ is a weakly-skeptical sem-explanation 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 nonThe 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 attack rules are particularly interesting when abductive reasoning is used to generate novel hypotheses explaining observations that are not already explained by a given theory resp. the given background assumptions.2 Example 4. Consider now = { ∧ , ¬ ∧ }. This time, with minimality, ∧ is not even a credulous sem-explanation of (sem ∈ {stb, prf}), since each of the two sem-extensions contains a minimality attacker ( ⇐ [], ∧ , ∧ → 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.

Given a sequent-based framework AFL,A(), an abductive sequent-based framework AAFL,A⋆() is constructed by adding to the arguments in ArgL () also abductive arguments, produced by Abduction, and where A⋆ is obtained by adding to the attack rules in A also (some of) the rules for maintaining explanations that are described above. Explanations are then defined as follows:

Abduction has been widely applied in diferent deduc

tive systems (such as adaptive logics [ 12 ]) and AI-based disciplines (e.g., logic programing [ 13 ]), including in the context of formal argumentation (see the survey in [ 14 ]).

This ongoing work ofers several novelties. In terms of knowledge representation we transparently represent abductive inferences by an explicit inference rule that Definition 1. Let AAFL,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 potenifnite set ℰ of L-formulas is called: tial defeats. Specifically designed attack rules address ∘ skeptical sem-explanation of , if there is Γ ⊆ s.t. the quality of the ofered explanation and thereby model ⇐ [⋀︀ℰ ], Γ is in every sem-extension of AAFL,A⋆(). critical questions [ 15 ] and meta-argumentative reasoning [ 16 ]. This is both natural and philosophically moti2In some accounts of abduction, e.g. [ 5 ], it is argued that the ab- vated, as argued in [ 17 ]. Our framework ofers a high ductively inferred should be of lesser epistemic status than the degree of modularity, and may be based on a variety of raebaosuotnaebrd’suscttaiortninigs tphoaitnatbadnudcstioon“thiseifgunnodraamnceen-tparlecsoernvcienpgtureaalsfoacnt- 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 changGabbay & Woods call an ‘ignorance problem’ (p. 42, Def. 3.2). ing the attack rules, all in the same base framework.

4. Discussion and Conclusion

References

[1] C. S. Peirce , The Collected Papers of Charles Sanders Peirce , Vol. I: The Principles of Philosophy , Harvard University Press, Cambridge, 1931 .

[2] P. Lipton , Inference to the Best Explanation , Routledge, 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 inference 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 argumentation , Argument & Computation 6 ( 2015 ) 73 - 99 .

[7] A. Borg , Assumptive sequent-based argumentation , 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 , volume 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 programming , in: Computational Logic: Logic Programming and Beyond, LNCS 2407 , Springer, 2002 , pp. 402 - 436 .

[14] K. Cyras , A. Rago , E. Albini, P. Baroni , F. Toni , Argumentative 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 of explanatory hypotheses: an argumentative approach , Logic Journal of the IGPL 29 ( 4 ) ( 2021 ) 523 - 535 .