<figure><img src="image_1.png" /></figure>

HAL
open science

# Abductive Reasoning in Expansions of Belnap-Dunn Logic

Meghyn Bienvenu, Katsumi Inoue, Daniil Kozhemiachenko

<figure><img src="image_2.png" /></figure>

► To cite this version:

Meghyn Bienvenu, Katsumi Inoue, Daniil Kozhemiachenko. Abductive Reasoning in Expansions of Belnap-Dunn Logic. Journal of Artificial Intelligence Research, 2026, 85, 10.1613/jair.1.18874. hal-05501987

HAL Id: hal-05501987

https://hal.science/hal-05501987v1

Submitted on 10 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Abductive Reasoning in Expansions of Belnap-Dunn Logic

MEGHYN BIENVENU, Université de Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, France

KATSUMI INOUE, National Institute of Informatics, Japan

DANIIL KOZHEMIACHENKO*, Aix-Marseille Univ, CNRS, LIS, France and Université de Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, France

In this paper, we explore the problem of explaining observations starting from a classically inconsistent theory by adopting a paraconsistent framework. More precisely, we consider theories formulated in the well-known Belnap-Dunn paraconsistent four-valued logic BD and its implicative expansion $BD_2$. Abductive solutions are then given in one of the two further expansions of BD: $BD_0$ that introduces formulas of the form $\circ\phi$ ('the information on $\phi$ is reliable') and $BD_\Delta$ that augments the language with $\Delta\phi$'s ('there is information that $\phi$ is true'). We show that explanations in $BD_0$ and $BD_\Delta$ are not reducible to one another. We analyse the complexity of standard abductive reasoning tasks (solution recognition, solution existence, and relevance / necessity of hypotheses) depending on the language of the solution ($BD_0$ or $BD_\Delta$) and on the language of the theory (BD or $BD_2$). In addition, we consider the complexity of abductive reasoning in the Horn fragment of $BD_2$. By showing how to reduce abduction in BD and its expansions to abduction in classical propositional logic, we enable the reuse of existing abductive reasoning procedures.

**JAIR Associate Editor:** Martin Gebser

**JAIR Reference Format:**

Meghyn Bienvenu, Katsumi Inoue, and Daniil Kozhemiachenko. 2026. Abductive Reasoning in Expansions of Belnap-Dunn Logic. *Journal of Artificial Intelligence Research* 85, Article 8 (February 2026), 34 pages. doi: 10.1613/jair.1.18874

## 1 Introduction

Abduction constitutes, together with deduction and induction, one of the three main forms of reasoning (Flach and Kakas 2000), with multiple applications in artificial intelligence, such as diagnosis (El Ayeb et al. 1993; J. R. Josephson and S. G. Josephson 2009; Koitz-Hristov and Wotawa 2018), commonsense reasoning (Bhagavatula et al. 2020; Paul 1993), formalisation of scientific reasoning (Magnani 2011), and machine learning (Dai et al. 2019).

In logic-based abduction (Eiter and Gottlob 1995), an *abduction problem* can be generally formulated as a pair $(\Gamma, \chi)$ consisting of a set of formulas $\Gamma$ (*theory*) and a formula $\chi$ (*observation*) such that $\Gamma \models \chi$, and the task is to find formulas $\phi$ (called (*abductive*) *explanations* or *solutions*) such that $\Gamma, \phi \models \chi$. Of course, not every such formula $\phi$ is intuitively acceptable as an explanation, which is why there are usually some restrictions placed on $\phi$. In particular, it is standard to require that $\phi$ be consistent with the theory $\Gamma$ and that $\phi$ provide a non-trivial explanation in the sense that $\phi$ should not entail the observation $\chi$ by itself but only when combined with the theory $\Gamma$. Additionally, to ensure irredundant and easily comprehensible explanations, it is typical to both restrict the syntactic shape of $\phi$ and to consider only the weakest possible (or minimal) explanations, cf. discussion

Authors' Contact Information: Meghyn Bienvenu, ORCID: 0000-0001-6229-8103, meghyn.bienvenu@u-bordeaux.fr, Université de Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, Talence, France; Katsumi Inoue, ORCID: 0000-0002-2717-9122, inoue@nii.ac.jp, National Institute of Informatics, Tokyo, Japan; Daniil Kozhemiachenko, ORCID: 0000-0002-1533-8034, daniil.kozhemiachenko@lis-lab.fr, Aix-Marseille Univ, CNRS, LIS, Marseille, France and Université de Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, Talence, France.

<figure><img src="image_4.png" /></figure>

This work is licensed under a Creative Commons Attribution International 4.0 License.

© 2026 Copyright held by the owner/author(s).

DOI: 10.1613/jair.1.18874

<footnote>*Corresponding Author.</footnote>
in (Marquis 2000, §4.2) and (Aliseda 2006, §3.3). Most commonly, this is done by requiring abductive solutions to take the form of terms (conjunctions of literals). In the propositional case, this means that the logically weakest solutions are simply the subset-minimal ones. The syntactic restriction to terms is important, as otherwise there would always be a unique (but hard to interpret) entailment-minimal solution, namely, the disjunction of all solutions.

Note, however, that in classical propositional logic (CPL) any *contradictory* theory is inconsistent. Thus, there is no explanation of $\chi$ from a contradictory $\Gamma$. This can be circumvented in two ways. First, by *repairing* $\Gamma$, i.e., making it consistent and then proceeding as usual (cf., e.g., (Du et al. 2015)). Second, by moving to a *paraconsistent* logic. The characteristic feature of such logics is the failure of the explosion principle $-p, \neg p \nvDash q$.

*Abduction in Paraconsistent Logics.* The question of how to employ paraconsistent logics to perform abductive reasoning on classically inconsistent theories has already generated interest in the philosophical logic community. For example, abduction in a three-valued logic called *Logic of Formal Inconsistency (LFI1)*, obtained by expanding the language of CPL (classical propositional logic) with new connectives $\bullet\phi$ and $\circ\phi$ (read ‘$\phi$ has a non-classical value’ or ‘the information about $\phi$ is unreliable’ and ‘$\phi$ has a classical value’ or ‘the information about $\phi$ is reliable’, respectively) is considered by Carnielli (2006). More recently, abductive explanations in the *minimal Logic of Formal Inconsistency (mbC)* were considered by Bueno-Soler et al. (2017) and Chlebowski et al. (2022), and abduction in a four-valued *Logic of Evidence and Truth (LET<sub>K</sub>)* was presented by Rodrigues et al. (2023).

*Abduction in Belnap-Dunn Logic.* These studies showcase the interest of paraconsistent abduction, but as they issue from a different research community, the formulation of abductive solutions and the questions that are explored depart from those typically considered in knowledge representation and reasoning (KR). In particular, these works allow *arbitrary* formulas as solutions (rather than terms). Moreover, to the best of our knowledge, there are no results on the complexity of paraconsistent reasoning tasks (e.g., solution existence). Also, in *mbC* and *LET<sub>K</sub>*,$\circ$ and $\bullet$ do not have truth-functional semantics, which complicates the comparison with classical logic and the reuse of established techniques.

The preceding considerations motivate us to revisit paraconsistent abduction by taking a KR perspective and adopting the well-known paraconsistent propositional logic BD by (Belnap 1977a,b; Dunn 1976). The main idea of BD is to treat the values of formulas as the information an agent (or a computer (Belnap 1977b)) might have w.r.t. a given statement $\phi$. This results in four ‘Belnapian’ values:

* T – ‘the agent is only told that $\phi$ is true’;

* F – ‘the agent is only told that $\phi$ is false’;

* B – ‘the agent is told that $\phi$ is false and that it is true’;

* N – ‘the agent is not told that $\phi$ is false nor that it is true’.

Note also that, as already observed by Rodrigues et al. (2023), the {¬, ∧, ∨}-language of BD is too weak for abduction: there is no solution for $\langle\{p \lor q\}, q\rangle$ except for $q$ itself because $p \lor q, \neg p \nvDash_{BD} q$. However, if one assumes that $p$ has value F, this will explain $q$ provided $p \lor q$. To do this, one needs to expand the language of BD with new connectives.

One option is to formulate abductive solutions in $BD_\circ$, the expansion of BD with the *truth-functional* version of $\circ$, previously studied by Omori and Sano (2014) and Omori and Waragai (2011). The connective $\circ$ is interpreted as follows: $\circ\phi$ has value T if $\phi$ has value T or F, and has value F, otherwise. In this expanded language, the formula $\neg p \land \circ p$, which expresses that *there is reliable information that p is false*, yields a solution to the abduction problem $\langle\{p \lor q\}, q\rangle$. Another possibility is to adopt $BD_\Delta$, the expansion of BD with the connective $\Delta$ by Sano and Omori (2014). Here, $\Delta\phi$ can be interpreted as ‘there is information that $\phi$ is true’ and has the following semantics: $v(\Delta\phi) = T$ if $v(\phi) \in \{T, B\}$ and $v(\Delta\phi) = F$, otherwise. In this case, the formula $\neg p \land \neg\Delta p$ (which reads: *p is false and there is no information that it is true*) is a solution.
Importantly, both $BD_Δ$ and $BD_○$ will allow us to solve some abduction problems that do not admit any solutions in classical logic nor in BD. The following example, adapted from (Rodrigues et al. 2023, Example 5), shows how one can deal with explanations from *classically inconsistent theories*.

**Example 1.1.** Assume that a valuable item was stolen, and we have contradictory information about the theft: it was stolen by either Paula or Quinn, but both of them claim to have an alibi. This can be represented with $Γ = \{p ∨ q, \neg p, \neg q\}$. Classically and in BD (without $○$ or $Δ$), there is no explanation for $p$ nor $q$ w.r.t. the theory $Γ$. However, in $BD_○$, we can explain $q$ by assuming that *Paula's alibi was confirmed by a reliable source*, which can be represented by the formula $○p$. This abduction problem can also be solved in $BD_Δ$ as follows: $q$ can be explained by assuming that *Paula's alibi was not disputed — $¬Δp$*.

Furthermore, the language of BD can prove too restrictive for expressing theories. In particular, it is impossible to define a natural implication that would validate the modus ponens rule and the deduction theorem using BD connectives (cf., e.g., (Arieli and Avron 1996, 1998; Omori and Wansing 2017)). On the other hand, it is natural to have conditional statements in theories, especially, in contexts where one wishes to specify possible causes of events. Thus, in this paper, we shall also consider theories formulated in the language of $BD_⊤$ — the expansion of BD with the so-called 'internal implication' $⊤$ proposed by Arieli and Avron (1996) and defined as follows

$$v(φ ⊃ χ) = \begin{cases} T & \text{if } v(φ) \in \{N, F\} \\ v(χ) & \text{otherwise} \end{cases}$$

As one can see, the semantics of $⊤$ corresponds to the definition of the entailment in BD and also mimics the classical definition of the implication ('$φ ⊃ χ$ is true when $φ$ is not true or $χ$ is true').

Moreover, the addition of $⊤$ allows us to consider abduction in the Horn fragments of $BD_⊤$. It is known (Creignou and Zanuttini 2006) that the complexity of *classical* Horn abduction is lower than in the case of arbitrary theories. Thus, it makes sense to investigate whether *paraconsistent* abduction also becomes simpler if one only deals with Horn theories.

*Contributions.* In this paper, we formalise abductive reasoning in BD and $BD_⊤$, where the abductive solutions are defined as terms in either $BD_Δ$ or $BD_○$. To identify informative solutions, we will typically impose a properness condition, requiring that a solution does not entail the observation by itself (i.e., it must be combined with the theory to explain the observation). Moreover, we consider two kinds of entailment-based minimality, giving rise to the notions of $|_BD$-minimal solutions and theory-minimal solutions.

We compare the classes of abduction problems that can be solved in $BD_Δ$ and $BD_○$, showing them to be incomparable in the sense that we can exhibit abduction problems that have $BD_Δ$-solutions but no $BD_○$-solutions, and others that admit $BD_○$-solutions but no $BD_Δ$-solutions. Moreover, we provide syntactic characterisations of when a $BD_Δ$-solution is $BD_○$-expressible, and vice versa (Theorem 3.14).

We next demonstrate how BD and $BD_⊤$ abduction problems, with either solutions, can be reduced to abduction in classical propositional logic (Theorems 4.5 and 4.9). Importantly, this makes it possible to apply classical consequence-finding methods to generate abductive solutions in $BD_Δ$ and $BD_○$, as detailed in Theorem 4.12 and the subsequent discussion.

We analyse the complexity of standard abductive reasoning tasks (solution recognition, solution existence, and relevance and necessity of hypotheses) in $BD_Δ$ and $BD_○$, for our two entailment-based notions of minimality. Our complexity results are summarised in Table 2 alongside existing results for CPL, showing that for most of the reasoning tasks the complexities coincide. With the aim of identifying relevant tractable settings, we also investigate abduction in the Horn and definite Horn fragments of $BD_⊤$. Our results reveal that the complexity of $L_Δ$-solution existence for (definite) BD-Horn abduction problems is the same as for Horn abduction in CPL, while $L_○$-solution existence remains $Σ_2^P$-hard even for definite Horn theories (Theorems 7.6 and 7.7).
This paper is an extended version of an earlier conference publication (Bienvenu et al. 2024). The main novel
contribution is the study of the complexity of abduction in BD₂ (only BD was considered in the conference
paper) and, in particular, its Horn fragments (Section 7). We additionally include the proofs that were omitted
from the conference paper and expand the discussion.

*Plan of the paper.* The remainder of the text is organised as follows. In Section 2, we formally introduce BD and its expansions and discuss their semantical and computational properties. In Section 3, we present the notions of abduction problem and explanation in expansions of BD. Section 4 discusses embeddings of BD and BD₂ abduction problems into the classical framework. Sections 5 and 6 are dedicated to the complexity of solving BD and BD₂ abduction problems. Section 7 considers abduction in the Horn and definite Horn fragments of BD₂. Finally, in Section 8, we summarise the paper’s results and outline a plan for future work.

## 2 BD and its Expansions

In this section, we recall the definition of the four-valued paraconsistent logic BD (Belnap 1977a,b; Dunn 1976) and its expansions BD_2, BD_0, and BD_Δ with ⊃ (implication), ◦ ('the information is reliable'), and Δ ('there is information that...'), respectively. We will also state some useful properties of these logics. We start by giving the syntax and semantics of BD and the considered expansions.

*Definition 2.1 (Syntax of BD and its expansions).* The language $\mathcal{L}_{o,\Delta,\supset}$ is the set of formulas constructed from a fixed countable set of propositional variables Prop via the following grammar:

$$ \phi := p \in \text{Prop} \mid \neg\phi \mid (\phi \land \phi) \mid (\phi \lor \phi) \mid (\phi \supset \phi) \mid \circ\phi \mid \Delta\phi $$

We use $\mathcal{L}_{BD}$, $\mathcal{L}_{\supset}$, $\mathcal{L}_{0}$, and $\mathcal{L}_{\Delta}$ to denote the fragments of $\mathcal{L}_{o,\Delta,\supset}$ obtained by restricting to the sets of connectives $\{\neg, \wedge, \vee\}$, $\{\neg, \wedge, \vee, \supset\}$, $\{\neg, \wedge, \vee, \circ\}$, and $\{\neg, \wedge, \vee, \Delta\}$, respectively, and will speak of $\mathcal{L}$-formulas (with $\mathcal{L}$ any of the preceding languages). We will use Prop($\phi$) and Prop[$\Xi$] to denote the set of all variables occurring in a formula $\phi$ and a set of formulas $\Xi$, respectively and employ the following shorthands:

$$ \bullet\phi := \neg\circ\phi $$

$$ \phi \Leftrightarrow \chi := (\phi \supset \chi) \land (\chi \supset \phi) $$

$$ \phi \Leftrightarrow \chi := (\phi \Leftrightarrow \chi) \land (\neg\phi \Leftrightarrow \neg\chi) $$

*Definition 2.2 (Semantics of BD and its expansions).* We consider the set $\mathcal{S} = \{\mathbf{T}, \mathbf{B}, \mathbf{N}, \mathbf{F}\}$ of truth values and define a BD valuation as a mapping $v : \text{Prop} \to \mathcal{S}$ that is extended to complex formulas using the following truth tables.

<table><thead><tr><th></th><th>T</th><th>B</th><th>N</th><th>F</th><th></th><th>T</th><th>B</th><th>N</th><th>F</th><th></th><th>T</th><th>B</th><th>N</th><th>F</th><th></th><th>T</th><th>F</th><th>T</th><th></th></tr></thead><tbody><tr><th>T</th><td>T</td><td>B</td><td>N</td><td>F</td><td></td><td>T</td><td>T</td><td>T</td><td>T</td><td></td><td>T</td><td>B</td><td>N</td><td>F</td><td></td><td>T</td><td>F</td><td>T</td><td></td></tr><tr><th>B</th><td>B</td><td>B</td><td>F</td><td>F</td><td></td><td>B</td><td>T</td><td>B</td><td>T</td><td>B</td><td></td><td>B</td><td>B</td><td>N</td><td>F</td><td></td><td>B</td><td>F</td><td>T</td></tr><tr><th>N</th><td>N</td><td>F</td><td>N</td><td>F</td><td></td><td>N</td><td>T</td><td>T</td><td>N</td><td>N</td><td></td><td>N</td><td>T</td><td>T</td><td>T</td><td></td><td>N</td><td>N</td><td>F</td></tr><tr><th>F</th><td>F</td><td>F</td><td>F</td><td>F</td><td></td><td>F</td><td>T</td><td>B</td><td>N</td><td>F</td><td></td><td>F</td><td>T</td><td>T</td><td>T</td><td></td><td>F</td><td>T</td><td>F</td></tr></tbody></table>

A formula $\phi \in \mathcal{L}_{o,\Delta,\supset}$ is BD-valid, written $\models_{BD} \phi$, iff $\forall v : v(\phi) \in \{\mathbf{T}, \mathbf{B}\}$, and $\phi$ is BD-satisfiable iff $\exists v : v(\phi) \in \{\mathbf{T}, \mathbf{B}\}$. A set of formulas $\Gamma$ entails $\chi$, written $\Gamma \models_{BD} \chi$, iff for every valuation $v$, if $v(\phi) \in \{\mathbf{T}, \mathbf{B}\}$ for every $\phi \in \Gamma$ then $v(\chi) \in \{\mathbf{T}, \mathbf{B}\}$.

We will henceforth use $\phi \approx \chi$ ($\phi$ and $\chi$ are weakly equivalent) to denote that $\phi$ and $\chi$ entail one another and $\phi \equiv \chi$ ($\phi$ and $\chi$ are strongly equivalent) to denote that $\phi$ and $\chi$ have the same Belnapian value in every BD valuation.

*Remark 1.* We use the terms ‘BD-valid’ and ‘BD-satisfiable’ to indicate that these semantic notions are defined in terms of (four-valued) BD-valuations, but one should note that they apply not only to formulas in the base language $\mathcal{L}_{BD}$ but also to formulas expressed in $\mathcal{L}_{o,\Delta,\supset}$ or any of the intermediate languages.

By examining the truth tables in Definition 2.2, we can see that there can be no BD-valid formula $\phi \in \mathcal{L}_{BD}$, since N is preserved by $\neg$, $\wedge$, and $\vee$. However, this is only true for the base language $\mathcal{L}_{BD}$, and if we allow $\supset$, $\circ$
or $\Delta$, then we can find BD-valid formulas. For example, $p \supset (p \lor q)$ is an example of a BD-valid $\mathcal{L}_{\sqsubseteq}$ formula. In fact, it is straightforward to establish that every classical tautology over $\{\wedge, \vee, \supset\}$ is BD-valid.

Likewise, there is no BD-unsatisfiable formula $\phi \in \mathcal{L}_{BD}$ since $\mathbf{B}$ is preserved under $\neg$, $\wedge$, and $\vee$, while BD-unsatisfiable formulas do exist if we introduce $\circ$ or $\Delta$. Examples of BD-unsatisfiable formulas include $p \wedge \neg\Delta p$, which states that $p$ is true and not true<fnref n="1" />, and $\circ p \wedge \bullet p$, which states that the information about $p$ is both reliable and unreliable. Observe that just as in classical logic, every formula can be inferred from a BD-unsatisfiable theory. For instance, we have $p \wedge \neg\Delta p \models_{BD} q$ and $\circ p \wedge \bullet p \models_{BD} q$.

Let us also remark that both weak and strong equivalence can be internalised in $BD_{\supseteq}$ using $\supset$. Namely, $\phi$ and $\chi$ are weakly equivalent iff $\phi \Leftrightarrow \chi$ is BD-valid, and $\phi$ and $\chi$ are strongly equivalent iff $\phi \Leftrightarrow \chi$ is BD-valid. Note, however, that $\neg\phi \lor \chi$ is not (strongly nor weakly) equivalent to $\phi \supset \chi$, in contrast to classical logic. More generally, we can observe that $\supset$ cannot be captured in $\mathcal{L}_{BD}$, as can be readily seen by considering the BD-valid $\mathcal{L}_{\supseteq}$-formula $p \supset p$ and recalling that there are no valid $\mathcal{L}_{BD}$-formulas. It is also important to note that $\supset$ and $\Leftrightarrow$ do not allow for contraposition: $\phi \supset \chi, \neg\chi \nvDash_{BD} \neg\phi$ and $\phi \Leftrightarrow \chi, \neg\chi \nvDash_{BD} \neg\phi$.

We can further observe that there are no $\mathcal{L}_{\supseteq}$-formulas that always have value $\mathbf{T}$ or $\mathbf{F}$ since $\mathbf{B}$ is preserved by all $\mathcal{L}_{\supseteq}$ connectives. By contrast, in $BD_{\circ}$ and $BD_{\Delta}$, we can define

$$ \tau_{\mathcal{L}_{\circ}} := \circ \circ p \qquad \perp_{\mathcal{L}_{\circ}} := \bullet \circ p \qquad \tau_{\mathcal{L}_{\Delta}} := \Delta p \lor \neg \Delta p \qquad \perp_{\mathcal{L}_{\Delta}} = \Delta p \wedge \neg \Delta p $$

and check that for every valuation $v$,

$$ v(\tau_{\mathcal{L}_{\circ}}) = v(\tau_{\mathcal{L}_{\Delta}}) = \mathbf{T} \qquad v(\perp_{\mathcal{L}_{\circ}}) = v(\perp_{\mathcal{L}_{\Delta}}) = \mathbf{F} $$

It is also interesting to note that $BD_{\circ}$ and $BD_{\supseteq}$ are less expressive than $BD_{\Delta}$. Indeed, $\circ\phi \equiv (\Delta\phi \wedge \neg\Delta\neg\phi) \lor (\Delta\neg\phi \wedge \neg\Delta\phi)$ and $\phi \supset \chi \equiv \neg\Delta\phi \lor \chi$, while on the other hand, $\Delta$ cannot be defined via $\circ$ or $\supset^2$ (Omori and Sano 2015, Corollaries 6.1, 6.19, and 6.24). It is also easy to check that distributive and De Morgan laws hold w.r.t. $\neg$, $\wedge$, and $\vee$ and that the following equivalences hold for $\Delta$:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \Delta\Delta\phi \equiv \Delta\phi & \Delta\circ\phi \equiv \circ\phi & \Delta(\phi \wedge \chi) \equiv \Delta\phi \wedge \Delta\chi \\ \Delta\neg\Delta\phi \equiv \neg\Delta\phi & \Delta\circ\bullet\phi \equiv \circ\bullet\phi & \Delta(\phi \lor \chi) \equiv \Delta\phi \lor \Delta\chi \\ & \Delta\phi \supset \chi \equiv \phi \supset \chi & \Delta(\phi \supset \chi) \equiv \phi \supset \Delta\chi \end{array} \qquad (1) $$

Thus, every formula $\phi \in \mathcal{L}_{\Delta}$ (hence, every $\phi \in \mathcal{L}_{\circ, \Delta, \supseteq}$) can be transformed into a strongly equivalent formula NNF($\phi$) in negation normal form, i.e., built from literals of the form $p, \neg p, \Delta p, \neg\Delta p, \Delta\neg p$, and $\neg\Delta\neg p$ using $\wedge$ and $\vee$. From here, it follows that $\mathcal{L}_{\circ, \Delta, \supseteq}$-formulas can be transformed into conjunctive and disjunctive normal forms (cf. (Font 1997, Theorem 3.9) for the case of $\mathcal{L}_{BD}$-formulas; the proof can be straightforwardly expanded to $\mathcal{L}_{\circ, \Delta, \supseteq}$-formulas).

One can also show that contraposition holds w.r.t. $\neg$ in $BD_{\circ}$ and w.r.t. $\neg\Delta$ in $BD_{\Delta}$ and that the deduction theorem can be recovered using $\Delta$:

**PROPOSITION 2.3.** Let $\phi, \chi \in \mathcal{L}_{\circ}$ and $\varrho, \sigma, \tau \in \mathcal{L}_{\Delta}$. Then the following statements hold.

(1) $\phi \models_{BD} \chi \iff \neg\chi \models_{BD} \neg\phi$.

(2) $\varrho, \sigma \models_{BD} \tau \iff \varrho, \neg\Delta\tau \models_{BD} \neg\Delta\sigma$.

(3) $\varrho, \sigma \models_{BD} \tau \iff \varrho, \neg\Delta\sigma \lor \tau$.

**PROOF.** We begin with Statement 1. Let $v$ be a BD valuation. Define $v^{\partial}$ as follows: $v^{\partial}(p) = \mathbf{N}$ if $v(p) = \mathbf{B}$; $v^{\partial}(p) = \mathbf{B}$ if $v(p) = \mathbf{N}$; $v^{\partial}(p) = v(p)$ otherwise. It is easy to check by induction on $\psi \in \mathcal{L}_{\circ}$ that $v^{\partial}(\psi) = \mathbf{N}$ if $v(\psi) = \mathbf{B}$; $v^{\partial}(\psi) = \mathbf{B}$ if $v(\psi) = \mathbf{N}$; $v^{\partial}(\psi) = v(\psi)$ otherwise.

<footnote n="1">¹Observe that in BD this is not the same as to assert that $p$ is true and false as $\{p, \neg p\}$ is satisfied by $v(p) = \mathbf{B}$.</footnote>

<footnote n="2">²On the contrary, $\Delta$ is definable in the presence of both $\circ$ and $\supset$ as follows: $\Delta\phi \equiv (\phi \supset \perp_{BD_{\circ}}) \supset \perp_{BD_{\circ}}$.</footnote>
From here, it follows immediately that the contraposition holds. Indeed, assume that $v(\neg\chi) \in \{\mathbf{T}, \mathbf{B}\}$ and $v(\neg\phi) \notin \{\mathbf{T}, \mathbf{B}\}$. Hence, $v(\chi) \in \{\mathbf{F}, \mathbf{B}\}$ and $v(\phi) \notin \{\mathbf{F}, \mathbf{B}\}$. Consider the case when $v(\phi) = \mathbf{T}$ and $v(\chi) = \mathbf{B}$. Then, $v^\partial(\phi) = \mathbf{T}$ but $v^\partial(\chi) = \mathbf{N}$, whence $\phi \not\models_{\mathbf{BD}} \chi$, as required. Other cases can be tackled similarly.

For Statement 2, assume that $\rho, \neg\Delta\tau \not\models_{\mathbf{BD}} \neg\Delta\sigma$, i.e. $v(\rho) \in \{\mathbf{T}, \mathbf{B}\}$, $v(\neg\Delta\tau) = \mathbf{T}$ and $v(\neg\Delta\sigma) = \mathbf{F}$. It is clear from the truth tables that $v(\sigma) \in \{\mathbf{T}, \mathbf{B}\}$ but $v(\tau) \in \{\mathbf{N}, \mathbf{F}\}$. Hence, $\rho, \sigma \not\models_{\mathbf{BD}} \tau$, as required. We can proceed analogously to show the second direction of Statement 2 and Statement 3. □

It follows from Item 1 that $\phi \approx \chi$ iff $\phi \equiv \chi$ in $\mathbf{BD}_\circ$. On the other hand, this is not the case in $\mathbf{BD}_\Delta$ and $\mathbf{BD}_\Box$: $p \approx \Delta p$, but $p$ is not strongly equivalent to $\Delta p$; likewise, $p \supset p$ and $q \supset q$ are weakly equivalent but not strongly equivalent.

We finish the section by establishing faithful embeddings of classical propositional logic (CPL) into BD and its expansions. We will use terminology and notation for CPL analogous to ones introduced for BD, e.g., speaking about CPL-validity and using $\models_{\text{CPL}}$ for the classical entailment relation.

**Definition 2.4.** Given $\phi \in \mathcal{L}_{\mathbf{BD}}$, we denote by $\phi^\circ$ the result of replacing each variable $p$ in $\phi$ with $\circ p$ and by $\phi^\Delta$ the result of replacing each occurrence of a variable $p$ in $\phi$ with $\Delta p$.

**PROPOSITION 2.5.** For every $\phi \in \mathcal{L}_{\mathbf{BD}}$, $\phi$ is CPL-valid iff $\phi^\circ$ is BD-valid iff $\phi^\Delta$ is BD-valid.

**PROOF.** We start with a proof that $\phi$ is CPL-valid iff $\phi^\circ$ is BD-valid. First let $v$ be a classical valuation such that $v(\phi) = \mathbf{F}$. We construct $v_v$ as follows: $v_v(p) = \mathbf{T}$ iff $v(p) = \mathbf{T}$ and $v_v(p) = \mathbf{N}$ otherwise. Observing that $v_v(\circ p) = v(p)$ and that the connectives $\vee, \wedge, \neg$ behave classically over $\{\mathbf{T}, \mathbf{F}\}$, we obtain $v_v(\phi^\circ) = v(\phi) = \mathbf{F}$. For the converse direction, we let $v$ be a BD valuation such that $v(\phi^\circ) = \mathbf{F}$, and we define $v_v$ as $v_v(p) = v(\circ p)$. Again, it is easy to check that $v_v(\phi) = v(\phi^\circ)$.

For $\phi$ and $\phi^\Delta$, we can proceed similarly. Let $v(\phi) = \mathbf{F}$ and define $v_v(p) = v(p)$. It is clear that $v_v(\phi^\Delta) = v(\phi)$. For the converse direction, let $v(\phi^\Delta) = \mathbf{F}$ and define $v_v(p) = v(\Delta p)$. Again, it is easy to verify that $v_v(\phi) = v(\phi^\Delta)$. □

**PROPOSITION 2.6.** Let $\phi, \chi \in \mathcal{L}_{\mathbf{BD}}$ and $\text{Prop}[\{\phi, \chi\}] = \{p_1, \dots, p_n\}$. Then $\phi \models_{\text{CPL}} \chi$ iff

$$ \phi \wedge \bigwedge_{i=1}^{n} (p_i \vee \neg p_i) \models_{\mathbf{BD}} \chi \vee \bigvee_{i=1}^{n} (p_i \wedge \neg p_i). $$

**PROOF.** The ‘if’ direction is straightforward as $p \wedge \neg p$ is classically unsatisfiable and $p \vee \neg p$ is classically valid. For the ‘only if’ direction, let $v$ be such that $v \left( \phi \wedge \bigwedge_{i=1}^{n} (p_i \vee \neg p_i) \right) \in \{\mathbf{T}, \mathbf{B}\}$ and $v \left( \chi \vee \bigvee_{i=1}^{n} (p_i \wedge \neg p_i) \right) \in \{\mathbf{N}, \mathbf{F}\}$. We show that $v(p_i) \in \{\mathbf{T}, \mathbf{F}\}$ for each variable $p_i$. Now, if $v(p_i) = \mathbf{B}$ for some $p_i$, then $v \left( \chi \vee \bigvee_{i=1}^{n} (p_i \wedge \neg p_i) \right) \in \{\mathbf{T}, \mathbf{B}\}$, contrary to the assumption, and if $v(p_i) = \mathbf{N}$ for some $p_i$, then $v \left( \phi \wedge \bigwedge_{i=1}^{n} (p_i \vee \neg p_i) \right) \in \{\mathbf{N}, \mathbf{F}\}$, also contrary to our assumption. □

### 3 Abduction in BD and $\mathbf{BD}_\Box$

Since we will formulate solutions to BD abduction problems in the languages $\mathcal{L}_\Delta$ and $\mathcal{L}_\circ$, we begin our presentation with definitions of literals and terms in $\mathcal{L}_\circ$ and $\mathcal{L}_\Delta$. We remark that since $\circ$ and $\bullet$ do not distribute over $\wedge$ and $\vee$, we cannot assume that $\mathcal{L}_\circ$-literals do not contain binary connectives and that $\mathcal{L}_\circ$-terms are $\vee$-free (as in the case of CPL) if we want every formula to be representable as a disjunction of terms.

**Definition 3.1 (Literals and terms).**

* A propositional literal is a variable $p$ or its negation $\neg p$.
* An $\mathcal{L}_{\Delta}$-literal has one of the following forms: $p, \neg p, \Delta p, \neg \Delta p, \Delta \neg p, \neg \Delta \neg p$ ($p \in \text{Prop}$).

* An $\mathcal{L}_{\circ}$-literal has one of the following forms: $p, \neg p, \circ \phi, \bullet \phi$ ($\phi \in \mathcal{L}_{\circ}$).

A propositional term (resp. $\mathcal{L}_{\Delta}$-term, $\mathcal{L}_{\circ}$-term) is a conjunction of propositional (resp. $\mathcal{L}_{\Delta}^{-}$, $\mathcal{L}_{\circ}^{-}$) literals.

One can readily see from (1) that $\mathcal{L}_{\Delta}$-terms can express all $\mathcal{L}_{\Delta}$-formulas even if $\Delta$'s are over propositional literals. On the other hand, although $\mathcal{L}_{\circ}$-terms, as we have just defined them, are expressive enough to capture all $\mathcal{L}_{\circ}$-formulas, they may be difficult to interpret in natural language. Indeed, while $\circ p$ and $\bullet p$ can be understood as 'information concerning $p$ is (un)reliable', a formula such as $\bullet (p \wedge \circ(\neg q \vee \bullet(\neg r \wedge \neg s)))$ does not have any obvious natural-language interpretation. Thus, for the purposes of abduction, it makes sense to consider solutions built from atomic $\mathcal{L}_{\circ}$-literals.

**Definition 3.2.** *Atomic $\mathcal{L}_{\circ}$-literals* are formulas of a form $p, \neg p, \circ p$, or $\bullet p$ with $p \in \text{Prop.}^3$ *Atomic $\mathcal{L}_{\circ}$-terms* are conjunctions of atomic $\mathcal{L}_{\circ}$-literals.

**Convention 1.**

* For a propositional literal $l$, we set $\bar{p} = \neg p, \overline{\neg p} = p$ and $\bar{l} = l$.

* Given a formula $\phi$, we use Lit($\phi$) to denote the set of propositional literals occurring in $\phi$.

* Given an $\mathcal{L}_{\Delta}$-term $\tau$, we use Lit$_{\Delta}$(τ) to denote the set of $\mathcal{L}_{\Delta}$-literals occurring in $\tau$.

* Given an atomic $\mathcal{L}_{\circ}$-term $\tau$, we use Lit$_{\circ}$(τ) to denote the set of atomic $\mathcal{L}_{\circ}$-literals occurring in $\tau$.

We can now define abduction problems and solutions.

**Definition 3.3.** We say that $\Gamma$ BD-consistently entails $\chi$ ($\Gamma \models_{\text{BD}}^{\text{cons}} \chi$) iff $\Gamma$ is BD-satisfiable and $\Gamma \models_{\text{BD}} \chi$.

**Definition 3.4 (Abduction problems).**

* A BD abduction problem is a triple $\mathbb{P} = (\Gamma, \chi, \mathbb{H})$ with $\Gamma \cup \{\chi\} \subseteq \mathcal{L}_{\text{BD}}$, and $\mathbb{H}$ a finite set of $\mathcal{L}_{\Delta}$-literals or of atomic $\mathcal{L}_{\circ}$-literals such that $\text{Prop}[\mathbb{H}] \subseteq \text{Prop}[\Gamma \cup \{\chi\}]$. We call $\Gamma$ a *theory*, members of $\text{H hypotheses}$, and $\chi$ an *observation*.

* A BD$_{\supset}$ abduction problem is a triple $\mathbb{P} = (\Gamma, \chi, \mathbb{H})$ with $\Gamma \cup \{\chi\} \subseteq \mathcal{L}_{\supset}$, and $\mathbb{H}$ a finite set of $\mathcal{L}_{\Delta}$-literals or of atomic $\mathcal{L}_{\circ}$-literals.

**Definition 3.5 (Solutions of abduction problems).** An $\mathcal{L}_{\Delta}$-solution (resp. $\mathcal{L}_{\circ}$-solution) of $\mathbb{P}$ is an $\mathcal{L}_{\Delta}$-term (resp. atomic $\mathcal{L}_{\circ}$-term) $\tau$ composed from the literals in $\mathbb{H}$ such that $\Gamma, \tau \models_{\text{BD}}^{\text{cons}} \chi$.

* A solution $\tau$ is proper if $\tau \not\models_{\text{BD}} \chi$.

* A proper solution $\tau$ is $\models_{\text{BD}}$-minimal (or, entailment-minimal) if there is no proper solution $\phi$ such that $\phi \not\models_{\text{BD}} \tau$ and $\tau \models_{\text{BD}} \phi$.

* A proper solution $\tau$ is theory-minimal if there is no proper solution $\phi$ such that $\Gamma, \phi \not\models_{\text{BD}} \tau$ and $\Gamma, \tau \models_{\text{BD}} \phi$.

Given a BD or $BD_{\supset}$ abduction problem $\mathbb{P}$, we write $S(\mathbb{P})$, $S^{\text{P}}(\mathbb{P})$, $S^{\text{BD}}(\mathbb{P})$, and $S^{\text{Th}}(\mathbb{P})$ to denote the sets of, respectively, all solutions, all proper solutions, all $\models_{\text{BD}}$-solutions, and all theory-minimal solutions.

In our presentation of BD abduction, we restrict the language of theories to either $\mathcal{L}_{\text{BD}}$ or $\mathcal{L}_{\supset}$. This is done because we are mostly interested in explanations from ‘standard’ (albeit contradictory) propositional theories. Such theories usually do not contain statements of the form ‘we have reliable information that $p$’ or ‘we do not have information that $q$’ that correspond to $\circ p$ and $\neg \Delta q$.

Just as in classical logic, it is important to restrict the form of solutions. Indeed, if arbitrary formulas (rather than terms) were admitted as solutions, then abduction problems would always have at most one $\models_{\text{BD}}$-minimal solution (modulo weak equivalence), since it would suffice to take the disjunction of all solutions. Moreover, if we

<footnote n="3">³Note that since $\circ \neg \phi \equiv \circ \phi$, we do not need to consider literals $\circ \neg p$ and $\bullet \neg p$.</footnote>
were to allow ⊃ in solutions, then the formula $(\bigwedge_{\phi \in \Gamma} \phi) \supset \chi$ would be a $|\models_{BD}$-minimal solution of $\mathbb{P} = \langle \Gamma, \chi, \mathbb{H} \rangle$, but entirely uninformative.

As one can see, the minimality of solutions is defined w.r.t. weak equivalence. Since $p \approx \Delta p$, this means that $\Delta p$ is a minimal solution iff $p$ is. The next statement shows how to normalise $\mathcal{L}_{\Delta}$-solutions.

**Definition 3.6.** Let $\tau, \tau',$ and $\tau''$ be $\mathcal{L}_{\Delta}$-terms and $l$ a propositional literal. We define $\tau^b$ inductively as follows:

$l^b = l$

$(\Delta l)^b = l$

$(\neg \Delta l)^b = \neg \Delta l$

$(\tau' \wedge \tau'')^b = \tau'^b \wedge \tau''^b$

**PROPOSITION 3.7.** Let $\tau$ be an $\mathcal{L}_{\Delta}$-term. Then, $\tau \approx \tau^b$.

**PROOF.** Consider some $\mathcal{L}_{\Delta}$-term, which we can express w.l.o.g. as follows for some $k, k', l, l', m, n \ge 0$:

$$ \tau = \bigwedge_{i=1}^{k} p_i \wedge \bigwedge_{i=1}^{l} \neg q_i \wedge \bigwedge_{i=1}^{k'} \Delta p_i' \wedge \bigwedge_{i=1}^{l'} \neg q_i' \wedge \bigwedge_{i=1}^{m} \neg \Delta r_i \wedge \bigwedge_{i=1}^{n} \neg \Delta \neg s_i $$

It follows that

$$ \tau^b = \bigwedge_{i=1}^{k} p_i \wedge \bigwedge_{i=1}^{l} \neg q_i \wedge \bigwedge_{i=1}^{k'} p_i' \wedge \bigwedge_{i=1}^{l'} \neg q_i' \wedge \bigwedge_{i=1}^{m} \neg \Delta r_i \wedge \bigwedge_{i=1}^{n} \neg \Delta \neg s_i $$

Now observe from Definition 2.2 that for a given valuation $v$, we have $v(\tau) \in \{\mathbf{T}, \mathbf{B}\}$ iff $v(p_i), v(p_i') \in \{\mathbf{T}, \mathbf{B}\}$, $v(q_i), v(q_i') \in \{\mathbf{B}, \mathbf{F}\}$, $v(r_i) \in \{\mathbf{N}, \mathbf{F}\}$, and $v(s_i) \in \{\mathbf{T}, \mathbf{N}\}$. Similarly, $v(\tau^b) \in \{\mathbf{T}, \mathbf{B}\}$ iff $v(p_i), v(p_i') \in \{\mathbf{T}, \mathbf{B}\}$, $v(q_i), v(q_i') \in \{\mathbf{B}, \mathbf{F}\}$, $v(r_i) \in \{\mathbf{N}, \mathbf{F}\}$, and $v(s_i) \in \{\mathbf{T}, \mathbf{N}\}$. It follows that $v(\tau) \in \{\mathbf{T}, \mathbf{B}\}$ iff $v(\tau^b) \in \{\mathbf{T}, \mathbf{B}\}$. Hence, $\tau \approx \tau^b$, as required. □

**Convention 2.** Given an abduction problem $\mathbb{P}$, we will use $\mathcal{S}(\mathbb{P})$, $\mathcal{S}^p(\mathbb{P})$, $\mathcal{S}^{BD}(\mathbb{P})$, and $\mathcal{S}^{Th}(\mathbb{P})$ to denote the sets of all solutions, all proper solutions, all $|\models_{BD}$-minimal solutions, and all theory-minimal solutions of $\mathbb{P}$, respectively.

**Convention 3.** To simplify the presentation of examples, we shall sometimes omit $\mathbb{H}$ when specifying abduction problems. In such cases, it is assumed that $\mathbb{H}$ contains all possible $\mathcal{L}_{\Delta}$-literals or atomic $\mathcal{L}_{\circ}$-literals (depending on which language we are considering).

Observe that we have defined two different notions of minimality. The first one ($|\models_{BD}$-minimality or, entailment-minimality) generalises subset-minimality from (Eiter and Gottlob 1995) to the BD setting. As we will see in Section 5.1, even though entailment between $\mathcal{L}_{\Delta}$-terms and atomic $\mathcal{L}_{\circ}$-terms is polynomially decidable, it is not equivalent to the containment of one term in the other, whence we need a more general criterion. This approach to minimality is also presented by Aliseda (2006). Theory-minimal solutions are, essentially, least specific solutions in the terminology of Sakama and Inoue (1995) and Stickel (1990) or least presumptive solutions in the terminology of Poole (1989). Theory-minimal solutions can also be seen as duals of theory prime implicates by Marquis (1995).

It is also instructive to note that we need the properness requirement in the notion of minimal solutions. This is particularly important for the problems $\mathbb{P} = \langle \Gamma, \chi, \mathbb{H} \rangle$ such that $\text{Prop}(\chi) \cap \text{Prop}[\mathbb{H}] \neq \emptyset$. For instance, consider the following formulation: $\Gamma = \{p \supset r, q \supset s, r \supset t\}$, $\chi = s \wedge (t \vee u)$. Clearly, if $\{s, t\} \subseteq \mathbb{H}$, $s \wedge t$ would be the ‘minimal’ but non-proper (and not informative) solution. In the framework of Definition 3.5 and if we set $\mathbb{H} = \{p, q, r\}$, the theory-minimal solution is $q \wedge r$ although $\Gamma, q \wedge r |\models_{BD} s \wedge t$.

In addition, it is easy to see that even though a theory-minimal solution is $|\models_{BD}$-minimal, the converse need not hold. Indeed, consider the following example.

**Example 3.8.** Imagine that a crime was committed by two people and the prosecution has three suspects: Paula, Quinn, and Rose. There is evidence against Rose, and it is known that Paula has committed the crime if and only if she had a motive (so, if she did not have a motive, she would not have done it). Still, it is unclear who the
second perpetrator is, as there is neither evidence against Paula nor an alibi for her. The prosecution, however, wishes to charge Quinn and Rose. The situation can be formalised as $P_{sus} = \langle \Gamma_{sus}, \chi_{sus}, H_{sus} \rangle$ with:

$$ \Gamma_{sus} = \{ \neg p \Leftrightarrow (q \wedge r), \neg q \Leftrightarrow (p \wedge r), \neg r \Leftrightarrow (p \wedge q), m \supset p, \neg m \supset \neg p, r \} \quad \chi_{sus} = q \wedge r \quad H_{sus} = \{m, \neg m, q, \neg q\} $$

Now, the prosecution may want to present the simplest (i.e., minimal) explanation. In both $\mathcal{L}_{\Delta}$ and $\mathcal{L}_{\circ}$, there are two $\models_{BD}$-minimal solutions: $q$ (evidence against Quinn) and $\neg m$ (a claim that Paula did not have a motive). Observe, however, that $q$ is weaker than $\neg m$ w.r.t. $\Gamma_{sus}$:

$$ \Gamma_{sus}, \neg m \models_{BD} q \quad \text{but} \quad \Gamma_{sus}, q \not\models_{BD} \neg m $$

To see why the latter holds, recall that $\supset$ and $\Leftrightarrow$ do not allow for contraposition: $\phi \supset \chi, \neg \chi \not\models_{BD} \neg \phi$ and $\phi \Leftrightarrow \chi, \neg \chi \models_{BD} \neg \phi$. Thus, we can consider the following valuation witnessing $\Gamma_{sus}, q \not\models_{BD} \neg m$: $v(m) = \text{N}, v(p) = \text{F}$, and $v(q) = v(r) = \text{T}$. This will give $v(\phi) = \text{T}$ for every $\phi \in \Gamma$ and $v(\neg m) = \text{N}$. This means that $\neg m$ is not a theory-minimal solution to $P_{sus}$.

We also note that allowing any $\mathcal{L}_{\circ}$-terms (rather than only atomic $\mathcal{L}_{\circ}$-terms) results in even weaker solutions.

**Example 3.9.** Consider the following problem $\mathbb{P} = \langle \Gamma, \chi, H \rangle$ (for the sake of discussion, we locally abuse notation and terminology by admitting non-atomic $\mathcal{L}_{\circ}$-terms as solutions).

$$ \Gamma = \{ (p \wedge p') \vee (q \wedge q'), \neg (p \wedge p') \} \quad \chi = q \wedge q' \quad H = \{ p, p', \circ p, \circ p', \circ (p \wedge p') \} \quad (2) $$

It is clear that $\circ(p \wedge p')$ and $\circ p \wedge \circ p'$ solve (2) and that $\circ p \wedge \circ p' \models_{BD} \circ(p \wedge p')$. Moreover, one can see that $\circ(p \wedge p')$ is a theory-minimal solution. Furthermore, some abduction problems cannot be solved if we only allow atomic terms. Indeed, one can check that no atomic $\mathcal{L}_{\circ}$-term over $p$ and $q$ properly solves $\langle \{p \vee q\}, (p \vee \neg p) \wedge (q \vee \neg q) \rangle$. On the other hand, $\circ p \wedge \circ ((p \vee \neg p) \wedge (q \vee \neg q))$ is a proper solution.

In what follows, we will illustrate the differences between abduction in BD and classical logic. First, we can observe that some problems have abductive solutions both in $\mathcal{L}_{\Delta}$ and $\mathcal{L}_{\circ}$ but no classical solutions (cf. Example 1.1). On the other hand, some problems can be solved only in $\mathcal{L}_{\circ}$. That is, there are no solutions in the form of $\mathcal{L}_{\Delta}$-terms<fnref n="4" /> even though there are $\mathcal{L}_{\circ}$-terms that solve the problem.

**Example 3.10.** As in Example 1.1, either Paula or Quinn is culpable, but now there is also evidence that implicates Paula $- p$. In this case, we want to justify that *Paula is innocent* $- \neg p$. There is, of course, no classical solution for $\langle \{p \vee q, p\}, \neg p \rangle$. Likewise, one can check that this problem admits no proper solutions in $\mathcal{L}_{\Delta}$, as $\tau \models_{BD} \neg p$ for any $\mathcal{L}_{\Delta}$-term $\tau$ such that $p \vee q, p, \tau \models_{BD} \neg p$.

How can we solve the problem in $BD_{\circ}$? We can add the $\mathcal{L}_{\circ}$-term $\bullet p$, i.e., assume that the *evidence against Paula is unreliable*. This way, we have $p \vee q, p, \bullet p \models_{BD} \neg p$, which is justified since one must not be convicted on unreliable evidence. It can be verified that $\bullet p$ is the unique BD-minimal proper solution for $\langle \{p \vee q, p\}, \neg p \rangle$. First, $p \vee q, p, \bullet p \models_{BD} \neg p$ and $\bullet p \not\models_{BD} \neg p$ (i.e., $\bullet p$ is a proper solution). Second, there is no atomic $\mathcal{L}_{\circ}$-term $\tau$ such that $\bullet p \models_{BD} \tau$ (whence, $\bullet p$ is an entailment-minimal solution). Finally, there is no other solution (except for $\neg p$).

Conversely, some problems can be solved only in $\mathcal{L}_{\circ}$.

**Example 3.11.** Consider $\mathbb{P} = \langle \{p \vee \neg p \vee q\}, q \rangle$. To infer $q$ from $p \vee \neg p \vee q$, one needs to assume that $p$ has value $\text{N}$, i.e. we need a formula $\phi$ such that $v(\phi) \in \{\text{T}, \text{B}\}$ iff $v(p) = \text{N}$ for all valuations $v$. In $\mathcal{L}_{\Delta}$, we can take $\phi = \neg \Delta p \wedge \neg \Delta \neg p$ and verify that it is a theory-minimal proper solution. On the other hand, one can see that there is no atomic $\mathcal{L}_{\circ}$-term (and, in fact, no $\mathcal{L}_{\circ}$-formula at all) that is a proper solution to $\langle \{p \vee \neg p \vee q\}, q \rangle$.

Indeed, suppose for a contradiction that we have $\phi \in \mathcal{L}_{\circ}$ such that $v(\phi) = \text{T}$ iff $v(p) = \text{N}$ for all valuations $v$. Take some valuation $v_{\text{N}}$ such that $v_{\text{N}}(p) = \text{N}$, hence $v_{\text{N}}(\phi) = \text{T}$. Define $v_{\text{N}}^{\partial}$ as the valuation obtained from $v_{\text{N}}$ by

<footnote n="4">⁴Of course, there are $\mathcal{L}_{\Delta}$-formulas that can solve the problem but we are interested in solutions in the form of terms.</footnote>
swapping N with B, and preserving T and F. As seen in the proof of Proposition 2.3, the valuation $v_N^\partial$ is such that $v_N^\partial(p) = B$ and $v_N^\partial(\phi) = T$, contradicting our earlier assumption.

Note that $\neg\Delta p \wedge \neg\Delta\neg p$ can be the only solution even if the theory does not contain CPL-valid clauses. Consider $\mathbb{P}' = \langle\{p \lor q, \neg p \lor r\}, q \land r, \{p, \neg p, \neg\Delta p, \neg\Delta\neg p, \circ p, \bullet p\}\rangle$. One can see that the only solution to $\mathbb{P}'$ is $\neg\Delta p \wedge \neg\Delta\neg p$.

The previous examples show that $\mathcal{L}_o$- and $\mathcal{L}_\Delta$-solutions to BD abduction problems are incomparable. The intuitive reason for this is that $\mathcal{L}_o$- and $\mathcal{L}_\Delta$-terms are able to define different sets of allowed values for the variables. Hence, it makes sense to ask which $\mathcal{L}_o$-solutions can be represented as $\mathcal{L}_\Delta$-solutions and vice versa. In the remainder of the section, we answer this question.

**Definition 3.12.**

* A BD-satisfiable $\mathcal{L}_\Delta$-term $\tau$ is N-free if for every literal $\neg\Delta l$ occurring in $\tau$, either $\Delta\bar{l}$ or $\bar{l}$ also occurs in $\tau$.

* A BD-satisfiable atomic $\mathcal{L}_o$-term $\tau$ is determined if for every $p$ such that $\circ p$ or $\bullet p$ occurs in $\tau$, either $p$ or $\neg p$ also occurs in $\tau$.

* An $\mathcal{L}_o$-solution (resp. $\mathcal{L}_\Delta$-solution) $\rho$ of a BD abduction problem $\mathbb{P}$ is $\mathcal{L}_\Delta$-representable (resp. $\mathcal{L}_o$-representable) if there exists an $\mathcal{L}_\Delta$-solution (resp. $\mathcal{L}_o$-solution) $\sigma$ of $\mathbb{P}$ such that $\rho \approx \sigma$.

**LEMMA 3.13.** *There is no $\mathcal{L}_\Delta$-term $\tau$ such that $\tau \approx \circ p$ or $\tau \approx \bullet p$.*

**PROOF.** Let $\phi$ be a formula such that $\text{Prop}(\phi) = \{p\}$. We say that $\phi$ defines a set of values $\mathcal{V} \subseteq \{\text{T}, \text{B}, \text{N}, \text{F}\}$ if $v(\phi) \in \{\text{T}, \text{B}\}$ iff $v(p) \in \mathcal{V}$. It is clear that two formulas over a single variable are weakly equivalent iff they define the same set of values. It is also evident that $\circ p$ defines $\{\text{T}, \text{F}\}$ and $\bullet p$ defines $\{\text{B}, \text{N}\}$.

On the other hand, $p$ and $\Delta p$ define $\{\text{T}, \text{B}\}$; $\neg p$ and $\Delta\neg p$ define $\{\text{B}, \text{F}\}$; $\neg\Delta p$ defines $\{\text{N}, \text{F}\}$, and $\neg\Delta\neg p$ defines $\{\text{T}, \text{N}\}$. $\mathcal{L}_\Delta$-terms can define only intersections of these sets of values, and thus, there is no $\mathcal{L}_\Delta$-term that would define $\{\text{T}, \text{F}\}$ or $\{\text{B}, \text{N}\}$. $\square$

**THEOREM 3.14.**

(1) An $\mathcal{L}_o$-solution is $\mathcal{L}_\Delta$-representable iff it is determined.

(2) An $\mathcal{L}_\Delta$-solution is $\mathcal{L}_o$-representable iff it is N-free.

**PROOF.** For Statement 1, let $\tau$ be an $\mathcal{L}_o$-solution of some abduction problem. By definition, $\tau$ is BD-satisfiable and hence does not contain $p \wedge \neg p \wedge \circ p$, nor $\circ p \wedge \bullet p$, for any $p$. Suppose that $\tau$ is determined. As $p \wedge \neg p \equiv \neg p \wedge \bullet p \equiv p \wedge \circ p \equiv p \wedge \neg p \wedge \bullet p$, we can assume w.l.o.g. that $\tau$ has the following form:

$$ \tau = \bigwedge_{i=1}^{m} (l_i \wedge \circ l_i) \wedge \bigwedge_{i'=1}^{m'} (l'_{i'} \wedge \circ l''_{i'}) \wedge \bigwedge_{j=1}^{n} l''_{j} $$

where the $l_i$, $l''_{i'}$, and $l''_{j}$ are propositional literals. Now, we observe that $l \wedge \circ l \equiv \Delta l \wedge \neg\Delta\bar{l}$. Thus, $\tau$ can be represented by the following N-free $\mathcal{L}_\Delta$-term $\tau^{\circ\Delta}$:

$$ \tau^{\circ\Delta} = \bigwedge_{i=1}^{m} (\Delta l_i \wedge \neg\Delta\bar{l}_i) \wedge \bigwedge_{i'=1}^{m'} (l'_{i'} \wedge \neg\Delta\bar{l}'_{i'}) \wedge \bigwedge_{j=1}^{n} l''_{j} $$

For the converse, suppose $\tau$ is not determined, i.e., there is some $\circ p$ such that neither $p$ nor $\neg p$ occurs in $\tau$, or there is some $\bullet q$ such that neither $q$ nor $\neg q$ occurs in $\tau$. By Lemma 3.13, we have that there is no conjunction of $\mathcal{L}_\Delta$-literals that is weakly equivalent to $\circ p$ or $\bullet q$. Hence, $\tau$ is not $\mathcal{L}_\Delta$-representable.
For Statement 2, consider an $\mathcal{L}_\Delta$-solution $\tau$. First, suppose that $\tau$ is an N-free term, and let $\tau^b$ be as in Definition 3.6. We have that $\tau^b \simeq \tau$ with $\tau^b$ having the following form:

$$ \tau^b = \bigwedge_{i=1}^{m} (l_i \wedge \neg \Delta \bar{l}_i) \wedge \bigwedge_{j=1}^{n} l'_j $$

It is clear that the following atomic $\mathcal{L}_\circ$-term represents $\tau^b$ (and hence, $\tau$):

$$ \tau^{\Delta\circ} = \bigwedge_{i=1}^{m} (l_i \wedge \circ l_i) \wedge \bigwedge_{j=1}^{n} l'_j $$

For the converse, suppose $\tau$ is not N-free, and w.l.o.g. let $\neg \Delta p$ occur in $\tau^b$ but $p$ not occur. From (Omori and Sano 2015, Propositions 6.23 and 6.23), we know that $\neg \Delta p$ (by itself, without $p$) is not definable in $BD_\circ$. As $\tau$ is satisfiable (being a solution), this means $\tau$ is not $\mathcal{L}_\circ$-representable. $\square$

We finish the section with a few observations. First, due to Theorem 3.14 and the simple syntactic definition of determined and N-free terms, $\mathcal{L}_\Delta$- and $\mathcal{L}_\circ$-recognisability can be tested in polynomial time. Next, observe that none of the solutions given in Examples 1.1–3.11 is representable in the other language. In Example 1.1, $\neg \Delta p$ is not $\mathcal{L}_\circ$-representable and $\circ p$ is not $\mathcal{L}_\Delta$-representable. In Example 3.10, an $\mathcal{L}_\circ$-solution $\bullet p$ is not $\mathcal{L}_\Delta$-representable. In Example 3.11, $\neg \Delta p \wedge \neg \Delta \neg p$ is not $\mathcal{L}_\circ$-representable. This shows that even though $BD_\circ$ is less expressive than $BD_\Delta$, their sets of solutions are incomparable. We can further remark that even if a problem has solutions in both languages, the solutions need not be (weakly or strongly) equivalent, especially if we consider BD- or theory-minimal solutions. Indeed, one can see that the solutions in Example 1.1 are theory-minimal, yet they are not weakly equivalent. More than that, none of them implies the other.

## 4 Generating Solutions to BD Abduction Problems by Reduction to CPL

In this section, we show how to apply classical consequence-finding procedures to generate solutions for $BD_\Delta$ abduction problems by reducing $BD_\Delta$ abduction to CPL abduction. We adapt the definition of classical abduction problems by Creignou and Zanuttini (2006) and Eiter and Gottlob (1995) to our notation.

**Definition 4.1.** A classical abduction problem is a triple $\mathbb{P} = (\Gamma, \chi, H)$ such that $\Gamma \cup \{\chi\} \subseteq \mathcal{L}_{BD}$ and $H$ is a set of propositional literals such that $\text{Prop}[H] \subseteq \text{Prop}[\Gamma \cup \{\chi\}]$.

* A solution of $\mathbb{P}$ is a conjunction $\tau$ of literals from $H$ such that $\Gamma, \tau \models_{CPL} \chi$ and $\Gamma, \tau \not\models_{CPL} \chi$.

* A solution $\tau$ is proper if $\tau \not\models_{CPL} \chi$.

* A proper solution $\tau$ is $\models_{CPL}$-minimal if there is no proper solution $\phi$ such that $\tau \models_{CPL} \phi$ and $\not\models_{CPL} \phi \leftrightarrow \tau$.

* A proper solution $\tau$ is theory-minimal if there is no proper solution $\phi$ such that $\Gamma, \tau \models_{CPL} \phi$ and $\Gamma, \phi \not\models_{CPL} \tau$.

The reduction of $BD_\Delta$ abduction with $\mathcal{L}_\Delta$-solutions to CPL abduction is formally stated in Theorem 4.5. It relies upon the following translation of $\mathcal{L}_\Delta$-formulas into classical logic. The translation uses that the truth and falsity of formulas in Belnap-Dunn logic are independent. Thus, $p$ and $\neg p$ are represented via two fresh variables $p^+$ and $p^-$, respectively. This makes it possible to represent the paraconsistent behaviour of $\neg$ in classical logic.

**Definition 4.2 (Translating $\mathcal{L}_\Delta$ formulas into CPL).** Let $\phi \in \mathcal{L}_\Delta$ be in NNF and let $\sim$ denote the classical negation.<fnref n="5" /> We define the formula $\phi^{cl}$ as follows:

$$ \begin{align*} p^{cl} &= p^+ \\ (\Delta p)^{cl} &= p^+ \end{align*} \qquad \begin{align*} (\neg p)^{cl} &= p^- \\ (\Delta \neg p)^{cl} &= p^- \end{align*} $$

<footnote n="5">⁵While we may assume that CPL is given over $\mathcal{L}_{BD}$, we sometimes use $\sim$ rather than $\neg$ to make clear we are working in CPL.</footnote>
$$(\neg\Delta p)^{cl} = \sim p^+$$

$$(\chi \wedge \psi)^{cl} = \chi^{cl} \wedge \psi^{cl}$$

$$(\neg\Delta\neg p)^{cl} = \sim p^-$$

$$(\chi \vee \psi)^{cl} = \chi^{cl} \vee \psi^{cl}$$

If $\phi \in \mathcal{L}_{\Delta}$, then $\phi^{cl}$ is defined as $(\phi_{\Delta})^{cl}$, where $\phi_{\Delta}$ is the NNF of the strongly equivalent $\mathcal{L}_{\Delta}$-formula obtained by replacing each subformula $\chi \supset \psi$ of $\phi$ by $\neg\Delta\chi \vee \psi$.

The next definition shows how to translate between BD valuations and classical valuations. It is phrased for $\mathcal{L}_{\Delta}$-formulas but will be later adapted to $\mathcal{L}_{\circ}$ formulas (see proof of Lemma 4.8).

**Definition 4.3 (Translating between BD and classical valuations).**

* Let $\phi \in \mathcal{L}_{\Delta}$ and $v$ be a BD valuation. We define the valuation $v^{cl}$ of $\phi^{cl}$ as follows:

$$v^{cl}(p^+) = \mathbf{T} \text{ iff } v(p) \in \{\mathbf{T}, \mathbf{B}\}$$

$$v^{cl}(p^-) = \mathbf{T} \text{ iff } v(p) \in \{\mathbf{F}, \mathbf{B}\}$$

* Let $v$ be a classical valuation of $\{p^+, p^- \mid p \in \text{Prop}\}$. We define $v^4$ as follows:

$$v^4(p) = \begin{cases} \mathbf{T} & \text{iff } v(p^+) = \mathbf{T} \text{ and } v(p^-) = \mathbf{F} \\ \mathbf{B} & \text{iff } v(p^+) = \mathbf{T} \text{ and } v(p^-) = \mathbf{T} \\ \mathbf{N} & \text{iff } v(p^+) = \mathbf{F} \text{ and } v(p^-) = \mathbf{F} \\ \mathbf{F} & \text{iff } v(p^+) = \mathbf{F} \text{ and } v(p^-) = \mathbf{T} \end{cases}$$

**LEMMA 4.4.** Let $\phi, \chi \in \mathcal{L}_{\Delta}$ be in NNF. Then $\phi \models_{\mathbf{BD}} \chi \text{ iff } \phi^{cl} \models_{\mathbf{CPL}} \chi^{cl}$.

**PROOF.** Suppose that $\phi \not\models_{\mathbf{BD}} \chi$, and let $v$ be a BD valuation such that $v(\phi) \in \{\mathbf{T}, \mathbf{B}\}$ and $v(\chi) \notin \{\mathbf{T}, \mathbf{B}\}$. It can be readily checked by structural induction that for every $\psi \in \mathcal{L}_{\Delta}$, $v(\psi) \in \{\mathbf{T}, \mathbf{B}\}$ iff $v^{cl}(\psi^{cl}) = \mathbf{T}$. We thus obtain $v^{cl}(\phi^{cl}) = \mathbf{T}$ and $v^{cl}(\chi^{cl}) = \mathbf{F}$, as desired.

For the converse direction, we let $v$ be a classical valuation of the variables $\{p^+, p^- \mid p \in \text{Prop}\}$ such that $v(\phi^{cl}) = \mathbf{T}$ and $v(\chi^{cl}) = \mathbf{F}$. Again, a routine inductive argument shows that for every $\psi \in \mathcal{L}_{\Delta}$, $v^4(\psi) \in \{\mathbf{T}, \mathbf{B}\}$ iff $v(\psi^{cl}) = \mathbf{T}$. It follows that $v^4(\phi) \in \{\mathbf{T}, \mathbf{B}\}$ and $v^4(\chi) \notin \{\mathbf{T}, \mathbf{B}\}$, as desired. $\square$

**THEOREM 4.5.** Let $\mathbb{P} = (\Gamma, \chi, \mathbf{H})$ be a BD$_{\Delta}$ abduction problem. The following are equivalent:

* $\phi$ is a ($\models_{\mathbf{BD}}$, theory-minimal, proper) $\mathcal{L}_{\Delta}$-solution of $\mathbb{P}$

* $\phi^{cl}$ is a ($\models_{\mathbf{CPL}}$, theory-minimal, proper) solution of $\mathbb{P}^{cl}_{\Delta} = (\Gamma^{cl}, \chi^{cl}, H^{cl}_{\Delta})$

where $H^{cl}_{\Delta} = \{p^+ \mid p \in \mathbf{H}\} \cup \{p^- \mid \neg p \in \mathbf{H}\} \cup \{\sim p^+ \mid \neg\Delta p \in \mathbf{H}\} \cup \{\sim p^- \mid \neg\Delta\neg p \in \mathbf{H}\}$.

**PROOF.** Let $\mathbb{P}$ be a BD$_{\Delta}$ abduction problem and $\phi$ its ($\models_{\mathbf{BD}}$, theory-minimal, proper) $\mathcal{L}_{\Delta}$-solution. From Lemma 4.4, we have that $\Gamma, \phi \models_{\mathbb{BD}}^{\text{cons}} \chi \text{ iff } \Gamma^{cl}, \phi^{cl} \models_{\mathbb{BD}}^{\text{cons}} \chi^{cl}$. This means that $\phi$ is an $\mathcal{L}_{\Delta}$-solution of $\mathbb{P}$ iff $\phi^{cl}$ is a solution of $\mathbb{P}^{cl}_{\Delta}$. For properness, observe again from Lemma 4.4 that $\phi \models_{\mathbb{BD}} \chi \text{ iff } \phi^{cl} \models_{\mathbf{CPL}} \chi^{cl}$.

For $\models_{\mathbb{BD}}$ and $\models_{\mathbf{CPL}}$-minimality, assume that there is some $\mathcal{L}_{\Delta}$-solution $\tau$ such that $\phi \models_{\mathbb{BD}} \tau$ and $\phi \neq \tau$. This means that $\phi^{cl} \models_{\mathbf{CPL}} \tau^{cl}$ but $\models_{\mathbf{CPL}} \tau^{cl} \leftrightarrow \phi^{cl}$ (i.e., $\phi^{cl}$ is not a $\models_{\mathbf{CPL}}$-minimal solution to $\mathbb{P}^{cl}_{\Delta}$). Conversely, let there be a classical term $\tau$ over $H^{cl}_{\Delta}$ such that $\tau$ is a solution to $\mathbb{P}^{cl}_{\Delta}$, $\models_{\mathbf{CPL}} \phi^{cl} \leftrightarrow \tau$, and $\phi^{cl} \models_{\mathbf{CPL}} \tau$. Now, consider $\tau^{BD}$ obtained from $\tau$ by replacing $p^+$'s with $p$'s, $p^-$'s with $\neg p$'s and $\sim$'s with $\neg\Delta$'s. It is clear that $(\tau^{BD})^{cl} = \tau$. Hence, $\tau^{BD}$ is a solution to $\mathbb{P}$ such that $\phi \models_{\mathbb{BD}} \tau^{BD}$ but $\tau^{BD} \neq \phi$ (i.e., $\phi$ is not a $\models_{\mathbb{BD}}$-minimal solution).

Finally, theory-minimality can be handled in the same way as entailment-minimality. $\square$

The following example illustrates how the embedding works.

**Example 4.6.** Recall Example 1.1. We consider $\mathbb{P}_{\Delta} = (\Gamma, q, H_{\Delta})$ with

$$\Gamma = \{p \vee q, \neg p, \neg q\}$$

$$H_{\Delta} = \{p, \neg p, \neg\Delta p, \neg\Delta\neg p\}$$
Applying Theorem 4.5, we obtain the following classical problem $\mathbb{P}_{\Delta}^{\text{cl}} = \langle \Gamma^{\text{cl}}, q^{+}, H_{\Delta}^{\text{cl}} \rangle$ where:

$$ \Gamma^{\text{cl}} = \{p^{+} \lor q^{+}, p^{-}, q^{-}\} $$

$$ H_{\Delta}^{\text{cl}} = \{p^{+}, p^{-}, \sim p^{+}, \sim p^{-}\} $$

It is easy to see that $\sim p^{+}$ is the unique theory-minimal classical solution of $\mathbb{P}_{\Delta}^{\text{cl}}$. It corresponds to $\neg \Delta p$ which is (as expected) the unique theory-minimal $\mathcal{L}_{\Delta}$-solution of $\mathbb{P}_{\Delta}$.

We observe that in general, $\mathcal{L}_{\Delta}$-solutions are not uniquely generated from classical abductive solutions since $p^{\text{cl}} = (\Delta p)^{\text{cl}} = p^{+}$. However, we know from Proposition 3.7 that $\mathcal{L}_{\Delta}$-terms can be normalised using $^{\circ b}$. Thus, for practical purposes, it makes sense to convert each classical solution $\phi$ into the unique $\mathcal{L}_{\Delta}$-solution $\tau$ such that $\tau^{\text{cl}} = \phi$ and $\tau = \tau^{\circ b}$.

For BD$_{o}$, we observe from Definition 2.2 that $\circ \phi$ expresses the statement ‘$\phi$ is true iff it is not false’ which does not correspond to a term in classical logic. This is intuitively why reducing BD$_{o}$ abduction to CPL abduction is more complicated.

**Definition 4.7.** Let $X_+$, $X_-$, $X_o$, $X_\bullet$ $\subseteq$ Prop be finite sets of propositional variables and let further, $X \supseteq X_+ \cup X_- \cup X_o \cup X_\bullet$. Consider the following atomic $\mathcal{L}_o$-term

$$ \phi = \bigwedge_{p \in X_+} p \wedge \bigwedge_{r \in X_-} \neg r \wedge \bigwedge_{s \in X_o} \circ s \wedge \bigwedge_{t \in X_\bullet} \bullet t $$

The classical counterpart of $\phi$ relative to $X$, denoted $\phi_X^{\circ}$, is defined as follows:

$$ \phi_X^{\circ} = \phi^{\sim} \wedge \phi_X^{\leftrightarrow} \qquad \phi^{\sim} = \bigwedge_{p \in X_+} p^{+} \wedge \bigwedge_{r \in X_-} r^{-} \wedge \bigwedge_{s \in X_o} s^{\circ} \wedge \bigwedge_{t \in X_\bullet} t^{\circ} $$

$$ \phi_X^{\leftrightarrow} = \bigwedge_{q \in X} (\sim q^{\circ} \leftrightarrow (q^{+} \leftrightarrow q^{-})) \quad (3) $$

where the $q^{+}$, $q^{-}$, and $q^{\circ}$'s are fresh variables (not in $X$).

Let us briefly discuss the construction of $\phi_X^{\circ}$. The idea here is to encode the semantics of $\circ$ in CPL. To do that, we utilise the fact that ‘truth’ and ‘falsity’ in BD are independent, so $p$ and $\neg p$ can be represented by two different variables in CPL, namely, $p^{+}$ and $p^{-}$. As $\circ \phi$ means that $\phi$ is either true or false (not both), to encode $\circ p$, we can use the following two formulas: a fresh variable $p^{\circ}$ and its definition $p^{\circ} \leftrightarrow (\sim p^{+} \leftrightarrow p^{-})$ in terms of $p^{+}$ and $p^{-}$. Observe further that the size of $\phi_X^{\circ}$ is linear in the cardinality of $X$. This, however, is only possible because $\phi$ is an *atomic term*, whence we do not have nested definitions of $\circ \chi$ formulas.

**LEMMA 4.8.** Let $\chi, \psi \in \mathcal{L}_o, \Xi = \text{Prop}(\chi) \cup \text{Prop}(\psi)$, and $\phi$ be an atomic $\mathcal{L}_o$-term such that $\text{Prop}(\phi) \subseteq \Xi$. Then $\phi, \chi \models_{\text{BD}} \psi$ iff $\phi_{\Xi}^{\circ}, \chi^{\text{cl}} \models_{\text{CPL}} \psi^{\text{cl}}$.

**PROOF.** For the ‘if’ direction, assume that $\phi, \chi \not\models_{\text{BD}} \psi$, and let $v$ be a BD valuation that falsifies this entailment. We show that the corresponding classical valuation $v^{\text{cl}}$ (cf. Definition 4.3) falsifies the classical entailment. It is clear that $v^{\text{cl}}(\chi^{\text{cl}}) = \text{T}$ and $v^{\text{cl}}(\psi^{\text{cl}}) = \text{F}$, so it only remains to show that $v^{\text{cl}}(\phi_{\Xi}^{\circ}) = \text{T}$. First, we extend $v^{\text{cl}}$, which was defined for variables $\{p^{+}, p^{-} | p \in \text{Prop}\}$, to the variables in $\{p^{\circ} | p \in \text{Prop}\}$ by setting

$$ v^{\text{cl}}(q^{\circ}) = \text{T} \Leftrightarrow v(q) \in \{\text{T}, \text{F}\} \quad (4) $$

This will ensure that $v^{\text{cl}}(\sim q^{\circ} \leftrightarrow (q^{+} \leftrightarrow q^{-})) = \text{T}$. It remains to show that $v^{\text{cl}}(\phi^{\sim}) = \text{T}$, which can be done by showing that $v^{\text{cl}}(l^{\text{cl}}) = \text{T}$ for every literal $l$ appearing in the $\mathcal{L}_o$-term $\phi$. We consider in turn the different kinds of literals. If $l = p \in \text{Prop}$, then it follows from our assumption $v(\phi) \in \{\text{T}, \text{B}\}$ that $v(p) \in \{\text{T}, \text{B}\}$, hence $v^{\text{cl}}(p^{\text{cl}}) = v^{\text{cl}}(p^{+}) = \text{T}$. If instead $l = \neg r$, then we must have $v(r) \in \{\text{F}, \text{B}\}$, hence $v^{\text{cl}}(\neg r^{\text{cl}}) = v^{\text{cl}}(r^{-}) = \text{T}$. Next take $l = \circ s$, in which case $v(s) \in \{\text{T}, \text{F}\}$, hence $v^{\text{cl}}(\circ s^{\circ}) = v^{\text{cl}}(s^{\circ}) = \text{T}$, using (4). Finally, if $l = \bullet t$, then $v(t) \in \{\text{B}, \text{N}\}$, so $v^{\text{cl}}(\bullet t^{\text{cl}}) = v^{\text{cl}}(\sim t^{\circ}) = \text{T}$, due to (4). We thus obtain $v^{\text{cl}}(\phi_{\Xi}^{\circ}) = \text{T}$, as required.
For the converse direction, let $\mathbf{v}$ be a classical valuation such that $\mathbf{v}(\phi_{\Xi}^{\circ}) = \mathbf{v}(\chi^{\mathrm{cl}}) = \mathbf{T}$ and $\mathbf{v}(\psi^{\mathrm{cl}}) = \mathbf{F}$. We construct the BD valuation $\mathbf{v}^4$ (cf. Definition 4.3). This gives us $\mathbf{v}^4(\chi) \in \{\mathbf{T}, \mathbf{B}\}$ and $\mathbf{v}^4(\psi) \notin \{\mathbf{T}, \mathbf{B}\}$. We check that $\mathbf{v}^4(\phi) \in \{\mathbf{T}, \mathbf{B}\}$. Since $\mathbf{v}(\phi_{\Xi}^{\circ}) = \mathbf{T}$, we immediately obtain that $\mathbf{v}(p^{+}) = \mathbf{T}$, hence $\mathbf{v}^4(p) \in \{\mathbf{T}, \mathbf{B}\}$, for every literal $p$ of $\phi$. Likewise, $\mathbf{v}(r^{-}) = \mathbf{T}$, hence $\mathbf{v}^4(r) \in \{\mathbf{F}, \mathbf{B}\}$, for every literal $\neg r$ of $\phi$. Furthermore, for every literal $\circ s$ of $\phi$, we have $\mathbf{v}(s^{\circ}) = \mathbf{T}$. As we also know that $\mathbf{v}(\sim q^{\circ} \leftrightarrow (q^{+} \leftrightarrow q^{-})) = \mathbf{T}$, it follows that $\mathbf{v}(s^{+}) \neq \mathbf{v}(s^{-})$, i.e., $\mathbf{v}^4(s) \in \{\mathbf{T}, \mathbf{F}\}$, whence $\mathbf{v}^4(\circ s) = \mathbf{T}$, as required. A similar argument can be used to show that $\mathbf{v}^4(\bullet t) = \mathbf{T}$ for every literal $\bullet t$ of $\phi$, completing the proof. $\square$

We can now use Lemma 4.8 to construct a faithful embedding of BD abduction problems with $\mathcal{L}_{\circ}$-solutions into classical abduction problems. Importantly, since atomic $\mathcal{L}_{\circ}$-terms are not always translated into conjunctions of literals, the reduction stated in Theorem 4.9 is more complex than the one we devised for $\mathcal{L}_{\Delta}$ and it preserves only theory-minimality. Intuitively, this is because $\phi^{\sim}$ does not by itself constrain the interactions between the newly introduced variables $p^{\circ}, p^{+}$, and $p^{-}$ (hence the need to include $\phi_{\Xi}^{\leftrightarrow}$).

**THEOREM 4.9.** Let $\mathbb{P} = (\Gamma, \chi, \mathbb{H})$ be a BD$_{\circ}$ abduction problem and $\Xi = \mathrm{Prop}[\Gamma \cup \{\chi\}]$. Then the following statements are equivalent:

* $\phi$ is a (theory-minimal, proper) $\mathcal{L}_{\circ}$-solution of $\mathbb{P}$;

* $\phi^{\sim}$ is a (theory-minimal, proper) solution of $\mathbb{P}_{\circ}^{\mathrm{cl}} = (\Gamma^{\mathrm{cl}} \cup \{\phi_{\Xi}^{\leftrightarrow}\}, \phi_{\Xi}^{\leftrightarrow} \supset \chi^{\mathrm{cl}}, \mathbf{H}_{\circ}^{\mathrm{cl}})$ with $\mathbf{H}_{\circ}^{\mathrm{cl}} = \{p^{+} \mid p \in \mathbb{H}\} \cup \{p^{-} \mid \neg p \in \mathbb{H}\} \cup \{p^{\circ} \mid \circ p \in \mathbb{H}\} \cup \{\sim p^{\circ} \mid \bullet p \in \mathbb{H}\}$.

**PROOF.** Let $\phi$ be an atomic $\mathcal{L}_{\circ}$-term. We are going to show that the following statements hold for $\phi^{\sim}$ (cf. Definitions 4.1 and 4.7).

(1) $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi^{\sim} \nvDash_{\mathrm{CPL}} \bot$ iff $\Gamma, \phi \nvDash_{\mathrm{BD}} \bot$.

(2) $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi^{\sim} \models_{\mathrm{CPL}} \phi_{\Xi}^{\leftrightarrow} \supset \chi^{\mathrm{cl}}$ iff $\Gamma, \phi \models_{\mathrm{BD}} \chi$.

(3) $\phi^{\sim} \nvDash_{\mathrm{CPL}} \phi_{\Xi}^{\leftrightarrow} \supset \chi^{\mathrm{cl}}$ iff $\phi \nvDash_{\mathrm{BD}} \chi$.

(4) There is a proper solution $\phi'$ of $\mathbb{P}_{\circ}^{\mathrm{cl}}$ such that $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi^{\sim} \nvDash_{\mathrm{CPL}} \phi'$ but $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi'$ $\nvDash_{\mathrm{CPL}} \phi^{\sim}$ iff there is a proper solution $\tau$ of $\mathbb{P}$ such that $\Gamma, \phi \models_{\mathrm{BD}} \tau$ but $\Gamma, \tau \nvDash_{\mathrm{BD}} \phi$.

Point 1 follows immediately from Lemma 4.8 because $\psi$ is classically unsatisfiable (and similarly, BD-unsatisfiable) iff it entails a fresh variable $p^{+}$. But then $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi^{\sim} \nvDash_{\mathrm{CPL}} p^{+}$ iff $\Gamma, \phi \nvDash_{\mathrm{BD}} p$ for a fresh $p^{+}$. This is equivalent to $\Gamma, \phi \nvDash_{\mathrm{BD}} \bot$, as required.

To check Point 2, we observe that it is equivalent (via the deduction theorem and contraction) to the following entailment: $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi^{\sim} \nvDash_{\mathrm{CPL}} \chi^{\mathrm{cl}}$. Again, by Lemma 4.8, this is equivalent to $\Gamma, \phi \models_{\mathrm{BD}} \chi$. Similarly, Point 3 is equivalent to $\phi^{\sim}, \phi_{\Xi}^{\leftrightarrow} \nvDash_{\mathrm{CPL}} \chi^{\mathrm{cl}}$. By Lemma 4.8, this is equivalent to $\phi \nvDash_{\mathrm{BD}} \chi$, as required.

Points 1–3 imply that $\phi \in \mathcal{S}^{\mathbb{P}}(\mathbb{P})$ iff $\phi^{\sim} \in \mathcal{S}^{\mathbb{P}}(\mathbb{P}_{\circ}^{\mathrm{cl}})$. It remains to show that the same holds for theory-minimal solutions, too.

For Point 4, assume first that there exists another proper solution $\phi' = \bigwedge_{i=1}^{k} p_i^{+} \wedge \bigwedge_{i=1}^{k'} q_i^{-} \wedge \bigwedge_{i=1}^{l} r_i^{\circ} \wedge \bigwedge_{i=1}^{l'} \sim s_i^{\circ}$ to $\mathbb{P}_{\circ}^{\mathrm{cl}}$ such that $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi^{\sim} \nvDash_{\mathrm{CPL}} \phi'$ but $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi'$ $\nvDash_{\mathrm{CPL}} \phi^{\sim}$. Now let $\tau = \bigwedge_{i=1}^{k} p_i \wedge \bigwedge_{i=1}^{k'} \neg q_i \wedge \bigwedge_{i=1}^{l} \circ r_i \wedge \bigwedge_{i=1}^{l'} \bullet s_i$. Observe that $\tau \sim = \phi'$. Thus, by Lemma 4.8, we have that $\tau$ is a proper solution of $\mathbb{P}$. We now show that (i) $\Gamma, \phi \models_{\mathrm{BD}} \tau$ but (ii) $\Gamma, \tau \nvDash_{\mathrm{BD}} \phi$. For (i), suppose for a contradiction that $\mathbf{v}$ is a BD-valuation witnessing $\Gamma, \phi \nvDash_{\mathrm{BD}} \tau$. By using a similar argument to the proof of Lemma 4.8, one can show that the corresponding classical valuation $\mathbf{v}^{\mathrm{cl}}$ (see Definition 4.3 and proof of Lemma 4.8) would witness $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi^{\sim} \nvDash_{\mathrm{CPL}} \phi'$, contradicting our assumption. Similarly, for (ii), let $\mathbf{v}$ be a CPL-valuation witnessing $\Gamma^{\mathrm{cl}}, \phi_{\Xi}^{\leftrightarrow}, \phi'$ $\nvDash_{\mathrm{CPL}} \phi^{\sim}$. Again, it can be verified that $\mathbf{v}^4$ (cf. Definition 4.3) will witness $\Gamma, \tau \nvDash_{\mathrm{BD}} \phi$, contradicting our earlier assumption. For the converse direction, we consider a proper solution $\tau$ of $\mathbb{P}$ such that $\Gamma, \phi \models_{\mathrm{BD}} \tau$ but $\Gamma, \tau \nvDash_{\mathrm{BD}} \phi$ and perform a similar reasoning using Lemma 4.8. $\square$
Note that we need to repeat $\phi_{\Xi}^{\leftrightarrow}$ both in the theory and the antecedent of the observation to preserve properness. As one can see from Definition 4.7, atomic $\mathcal{L}_o$-terms are not translated into classical terms. Thus, we need to account for the semantics of $\circ p$'s and $\bullet p$'s which are translated using the propositional variables $p^o$'s. This can be done by adding $\phi_{\Xi}^{\leftrightarrow}$ to the theory. But when we check that the translated solution does not entail the observation in classical logic, we cannot use the theory, whence, we circumvent this problem by using the deduction theorem and putting $\phi_{\Xi}^{\leftrightarrow}$ as the antecedent of the observation. One can also see that to preserve arbitrary solutions, it suffices to add $\phi_{\Xi}^{\leftrightarrow}$ to the theory only.

**Example 4.10.** Recall again Example 1.1 and consider $\mathbb{P}_o = \langle \Gamma, q, H_o \rangle$, where:

$$ \Gamma = \{p \lor q, \neg p, \neg q\} \qquad H_o = \{p, \neg p, \circ p, \bullet p\} $$

Applying Theorem 4.9, we obtain $\mathbb{P}_o^{\text{cl}} = \langle \Gamma^o, \phi_{\{p,q\}}^{\leftrightarrow} \supset q^+, H_o^{\text{cl}} \rangle$, where:

$$ \Gamma^{\text{cl}} = \{p^+ \lor q^+, p^-, q^-\} \qquad \phi_{\{p,q\}}^{\leftrightarrow} = \bigwedge_{r \in \{p,q\}} (\sim r^o \leftrightarrow (r^+ \leftrightarrow r^-)) $$

$$ \Gamma^o = \Gamma^{\text{cl}} \cup \{\phi_{\{p,q\}}^{\leftrightarrow}\} \qquad H_o^{\text{cl}} = \{p^+, p^-, p^o, \sim p^o\} $$

It is easy to check that $p^o$ is the unique theory-minimal classical solution of $\mathbb{P}_o^{\text{cl}}$. It corresponds to $\circ p$ – the unique theory-minimal $\mathcal{L}_o$-solution of $\mathbb{P}^o$.

**Remark 2.** Notice that the translations presented in Definitions 4.2 and 4.7 can be extended to abduction problems formulated in $\mathcal{L}_o$ and $\mathcal{L}_\Delta$. There is, however, an important difference: while $\mathcal{L}_\Delta$-formulas have negation normal forms which can be translated to classical logic, this is not the case for $\mathcal{L}_o$-formulas. Indeed, if we generalise the translation in Definition 4.7 to arbitrary $\mathcal{L}_o$-formulas, $\circ\phi$ will correspond to $\sim q_\phi^o \leftrightarrow (\phi^{\text{cl}} \leftrightarrow (\neg\phi)^{\text{cl}})$ with $q_\phi^o$ being a fresh variable and $\phi^{\text{cl}}$ and $(\neg\phi)^{\text{cl}}$ being translations of $\phi$ and $\neg\phi$. One can see that if $\circ$'s are nested, this translation results in an exponential increase in the length of the formula.

Theorems 4.5 and 4.9 show that we can use classical techniques of abductive reasoning to solve BD abduction problems. Among the best-known techniques are those based upon consequence finding, cf. (del Val 2000; Inoue 2002, 1992; Marquis 2000, 1995; Val 1999). We recall that consequence finding is concerned with generating the logically strongest clauses entailed from a given input theory. Such clauses are known as prime implicates, and several more refined notions of prime implicates have also been studied in the consequence finding literature.

In the remainder of this section, we will clarify how classical consequence finding procedures can be employed to solve BD abduction problems. We first recall the notion of $\langle H, \phi \rangle$ prime implicates and introduce the notion of $\langle H, \phi \rangle$ theory prime implicates that refines theory prime implicates proposed by Marquis (1995). In this setting, H is the set of variables one can use to construct an implicate, and $\phi$ is the formula from which the implicate should not follow. This simulates the properness requirement on abductive solutions.

**Definition 4.11 (Prime implicates).** Let $\phi, \chi, \psi \in \mathcal{L}_{\text{BD}}, \kappa$ a propositional clause, and $H \subseteq \text{Lit}$ be finite. We say that

* $\kappa$ is an $\langle H, \phi \rangle$ prime implicate of $\chi$ iff $\phi \land \chi \models_{CPL} \kappa, \phi \not\models_{CPL} \kappa, \text{Lit}(\kappa) \subseteq H$, and there is no propositional clause $\kappa'$ such that $\phi \land \chi \models_{CPL} \kappa', \kappa' \models_{CPL} \kappa$, and $\kappa \not\models_{CPL} \kappa'$;

* $\kappa$ is an $\langle H, \phi \rangle$ theory prime implicate of $\chi$ w.r.t. $\psi$ iff $\phi \land \chi \land \psi \models_{CPL} \kappa, \phi \land \psi \not\models_{CPL} \kappa, \text{Lit}(\kappa) \subseteq H$, and there is no propositional clause $\kappa'$ such that $\phi \land \chi \land \psi \models_{CPL} \kappa', \text{Lit}(\kappa') \subseteq H$, and $\psi \land \kappa' \models_{CPL} \kappa$, but $\psi \land \kappa \not\models_{CPL} \kappa'$.

As one can see from the previous definition, the notion of $\langle H, \phi \rangle$ prime implicates is dual to the notion of (classical) entailment-minimal solutions to abduction problems. Similarly, $\langle H, \phi \rangle$ theory prime implicates dualise theory-minimal solutions when $\phi = \psi$. Indeed, in this case, the notion simplifies as follows:
Item 1 of Theorem 4.12 indicates that to generate a BD-minimal $\mathcal{L}_{\Delta}$-solution, we need to compute a $\langle H, \phi \rangle$ prime implicate of $\chi$ (where $H := \sim H^{\text{cl}}$, $\phi := \psi^{\text{cl}}$ and $\chi := \sim \chi^{\text{cl}}$), which is a minimal clause $\kappa$ such that $\phi \wedge \chi \models \kappa$ and $\phi \not\models \kappa$. That is, a consequence finding procedure needs to find a 'new' consequence of $\phi \wedge \chi$ which is not an 'old' consequence of $\phi$. Next, to ensure the properness of a solution, we need to verify that an obtained prime implicate $\kappa$ does not follow from $\chi$, i.e., $\chi \not\models \kappa$. When an observation is a term, this is easy since its negation $\chi$ is a clause, and we can just check if $\chi$ does not subsume $\kappa$, i.e., $\chi \not\subseteq \kappa$. On the other hand, if $\chi$ is an arbitrary formula, we can check if $\kappa$ is a 'new' characteristic clause of $\chi$ w.r.t. $\phi$ and H using SOL resolution.

According to Items 2–4 of Theorem 4.12, to generate theory-minimal $\mathcal{L}_{\Delta}$-solutions or either kind of minimal $\mathcal{L}_{\circ}$-solution, we need a procedure to compute theory prime implicates. While theory prime implicate generation has been considered before by Marquis and Sadaoui (1996), to the best of our knowledge, there does not exist a procedure that will compute the more refined notion of $\langle H, \phi \rangle$ theory prime implicates with respect to $\psi$ (cf. Definition 14) employed in our characterisations. However, we can suggest two approaches to adapt existing methods for this computation. The first method is naïve: we use the procedure by Marquis and Sadaoui (1996) to generate all theory prime implicates, then pick those that only contain the literals from H, and finally, check that they do not follow from $\phi$, which is $\psi^{\text{cl}}$, $\psi^{\text{cl}} \wedge \phi_{\Xi}^{\leftarrow}$, or $\phi_{\Xi}^{\leftarrow}$ depending on the solution we need. Alternatively, theory-minimal solutions (least specific explanations) can be computed by SOL-S resolution by Inoue (1992) in the case of Theorem 4.12 (2) and (4), where $\langle H, \phi \rangle$ theory prime implicates (w.r.t. $\phi$) are concerned. In a nutshell, the idea is as follows: if the resolution procedure selects a literal belonging to the specified vocabulary H for expansion by resolution with other clauses in $\phi$, that option for expansion is ignored (called 'cut'), and the literal becomes a part of a found clause. Then, such a 'cut' clause entails, together with $\phi$, a clause that would be obtained by further expanding by resolution. This procedure is guaranteed to produce, for every $\langle H, \phi \rangle$ theory prime implicate $\kappa'$ w.r.t. $\phi$, some implicate $\kappa$ such that $\phi \wedge \kappa \models \kappa'$ (Inoue 1992, Theorem 5.1).

# 5 Complexity of Term Entailment

This section contains some technical results concerning entailment from and between $\mathcal{L}_{\Delta}$- and $\mathcal{L}_{\circ}$-terms that will facilitate the proofs of the complexity results for abductive reasoning tasks in Section 6. Recall from Definition 3.5 that a proper solution of an abduction problem $\mathbb{P} = \langle \Gamma, \chi, H \rangle$ is a term $\phi$ that is consistent with $\Gamma$ and such that $\Gamma \cup \{\phi\}$ entails $\chi$ but $\phi$ alone does not. Additionally, if we want $\phi$ to be a minimal solution, we also need to check that no other solution is entailed by $\phi$. Thus, to determine the complexity of recognising solutions, we start by determining the complexity of these entailment problems. We summarise the results of this section in Table 1.

## 5.1 Entailment Between Terms

We first study the complexity of entailment between terms. In the next two theorems, we show that this task can be decided in polynomial time, both for $\mathcal{L}_{\Delta}$-terms and atomic $\mathcal{L}_{\circ}$-terms. We begin with the following lemma.

**LEMMA 5.1.** For any BD-satisfiable atomic $\mathcal{L}_{\circ}$-terms $\sigma$ and $\sigma'$, it holds that $\sigma \models_{BD} \sigma'$ iff

(1) every literal $\circ p$ that occurs in $\sigma'$ also occurs in $\sigma$;

(2) for every literal $\bullet p$ occurring in $\sigma'$, $\bullet p$ occurs in $\sigma$ or $p$ and $\neg p$ occur in $\sigma$;

(3) for every propositional literal $l$ occurring in $\sigma'$, $l$ occurs in $\sigma$ or $\bar{l}$ and $\bullet l$ occur in $\sigma$.
<table><caption>Table 1. Complexity of entailment tasks, where $\Gamma \cup \{\psi\} \subseteq \mathcal{L}_{\text{BD}}$, $\Delta \cup \{\chi\} \subseteq \mathcal{L}_{\text{O}}$, and $\sigma$ and $\tau$ are terms in the considered language ($\mathcal{L}_{\Delta}$ or $\mathcal{L}_{\circ}$). We use 'NP-c.' and 'coNP-c.' as shorthands for NP-complete and coNP-complete.</caption><thead><tr><th>Decision problem</th><th><i>L</i><sub>Δ</sub></th><th><i>L</i><sub>Ο</sub></th><th></th></tr></thead><tbody><tr><td>τ |=<sub>BD</sub> ψ?</td><td>in P</td><td>coNP-c.</td><td>Theorems 5.11 and 5.10</td></tr><tr><td>τ |=<sub>BD</sub> χ?</td><td>coNP-c.</td><td>coNP-c.</td><td>Theorems 5.12 and 5.10</td></tr><tr><td>τ |=<sub>BD</sub> σ?</td><td>in P</td><td>in P</td><td>Theorems 5.3 and 5.2</td></tr><tr><td>Γ, τ |=<sub>BD</sub> σ?</td><td>in P</td><td>coNP-c.</td><td>Theorems 5.6 and 5.4</td></tr><tr><td>Γ, τ !=<sub>BD</sub> ⊥?</td><td>in P</td><td>NP-c.</td><td>Corollaries 5.7 and 5.5</td></tr><tr><td>Γ, τ |=<sub>BD</sub> ψ?</td><td>coNP-c.</td><td>coNP-c.</td><td>Theorem 5.13</td></tr><tr><td>Δ, τ |=<sub>BD</sub> σ?</td><td>coNP-c.</td><td>coNP-c.</td><td>Theorem 5.13</td></tr><tr><td>Δ, τ |=<sub>BD</sub> ψ?</td><td>coNP-c.</td><td>coNP-c.</td><td>Theorem 5.13</td></tr></tbody></table>

PROOF. The 'if' direction is evident since $p \wedge \neg p \models_{BD} \bullet p$ and $\tilde{l} \wedge \bullet l \models_{BD} l$. For the 'only if' direction, we show that if one of the conditions (1), (2), or (3) does not hold, then $\sigma \not\models_{BD} \sigma'$. Let $v$ be any satisfying valuation for $\sigma$. We are going to modify $v$ so that we retain $v(\sigma) \in \{\text{T}, \text{B}\}$ while ensuring $v(\sigma') \notin \{\text{T}, \text{B}\}$. We consider three cases. (1) If there is some $\circ p$ in $\sigma'$ but not in $\sigma$, we set $v(p) = \text{B}$. This gives $v(\sigma') = \text{F}$. (2) If $\bullet p$ occurs in $\sigma'$ but neither $\bullet p$ nor $p$ together with $\neg p$ do, we set $v(p) = \text{T}$ if $p$ occurs in $\sigma$ and $v(p) = \text{F}$, otherwise. Again, we have $v(\sigma') = \text{F}$. (3) Finally, if there is some $l$ in $\sigma'$ such that neither $l$ nor $\tilde{l}$ together with $\bullet l$ occur in $\sigma$, we consider two cases: (i) neither $l$ nor $\tilde{l}$ occurs in $\sigma$ and (ii) neither $l$ nor $\bullet l$ occurs in $\sigma$. If (i) is the case, we set $v(l) = \text{N}$; if (ii) is the case, we set $v(l) = \text{F}$. □

THEOREM 5.2. *Entailment between atomic *L*<sub>Ο</sub>-terms is decidable in deterministic polynomial time.*

PROOF. Let $\sigma$ and $\sigma'$ be atomic $L_{\circ}$-terms. We begin by noting that $\sigma$ is BD-unsatisfiable iff (i) $p, \neg p$, and $\circ p$ occur in $\sigma$; or (ii) $\circ p$ and $\bullet p$ occur in $\sigma$. The 'if' direction is evident since $p \wedge \neg p \wedge \circ p$ and $\circ p \wedge \bullet p$ are unsatisfiable. For the 'only if' direction, assume that there is no variable $p$ such that $p, \neg p$, and $\circ p$ occur in $\sigma$, nor any variable $q$ such that $\circ q$ and $\bullet q$ occur in $\sigma$. We construct a satisfying valuation $v$ as follows:

* $v(r) = \text{T}$ iff $r$ occurs in $\sigma$ but $\neg r$ and $\bullet r$ do not, or only $\circ r$ occurs in $\sigma$;

* $v(r) = \text{F}$ iff $\neg r$ occurs in $\sigma$ but $r$ and $\bullet r$ do not;

* $v(r) = \text{B}$ otherwise.

It is clear that $v(\sigma) \in \{\text{T}, \text{B}\}$. Indeed, it is easy to check that every literal occurring in $\sigma$ has value $\text{T}$ or $\text{B}$ and that $v$ is well defined.

It follows from this characterisation that the satisfiability of an atomic $L_{\circ}$-term can be decided in polynomial time. In addition, observe that $\sigma \models_{BD} \sigma'$ if $\sigma$ is unsatisfiable and $\sigma \not\models_{BD} \sigma'$ if $\sigma$ is satisfiable but $\sigma'$ is not. Finally, it follows from Lemma 5.1 that entailment between satisfiable atomic $L_{\circ}$-terms is decidable in polynomial time. □

A similar property of $L_{\Delta}$-terms follows immediately from Lemma 4.4.

THEOREM 5.3. *Entailment between $L_{\Delta}$-terms is decidable in deterministic polynomial time.*

To check that $\tau$ is a theory-minimal solution of $\langle\Gamma, \chi, \mathcal{H}\rangle$, we need to establish that there is no other solution $\sigma$ such that $\Gamma, \tau \models_{BD} \sigma$ but $\Gamma, \sigma \not\models_{BD} \tau$. The next results show that the complexity of checking term entailment w.r.t. a background $L_{\text{BD}}$-theory differs depending on whether we consider $L_{\circ}$ or $L_{\Delta}$.

THEOREM 5.4. *It is coNP-complete to decide whether $\Gamma, \rho \models_{BD} \sigma$, given $\Gamma \subseteq L_{\text{BD}}$ and atomic $L_{\circ}$-terms $\rho$ and $\sigma$.*
PROOF. Membership is evident since BD<sub>o</sub> has truth-table semantics. For hardness, observe that Γ is classically unsatisfiable iff Γ, $\bigwedge_{p \in \text{Prop}[\Gamma]} \circ p \models_{\text{BD}} q$ with $q \notin \text{Prop}[\Gamma]$. □

COROLLARY 5.5. It is NP-complete to decide whether Γ, τ ̸|∈<sub>BD</sub> ⊥ given Γ ⊆ L<sub>BD</sub> and an atomic L<sub>o</sub>-term τ.

PROOF. The statement follows from Theorem 5.4 since ⊥ ≡ ○p ∧ ●p.

In L<sub>Δ</sub>, however, this problem is tractable.

THEOREM 5.6. It can be decided in polynomial time whether Γ, ϱ |=$_{BD}$ σ, given Γ ⊆ L<sub>BD</sub> and L<sub>Δ</sub>-terms ϱ and σ.

PROOF. It suffices to show the result for the case where σ is an L<sub>Δ</sub>-literal. Due to Propositions 2.3 and 3.7, Γ, ϱ |=$_{BD}$ σ iff Γ, ϱ, (¬Δσ)<sup>b</sup> |=$_{BD}$ ⊥, so we may focus on solving the latter task. First, we assume w.l.o.g. that all formulas in Γ are in NNF and that ϱ ∧ (¬Δσ)<sup>b</sup> is BD-satisfiable (this can be checked in polynomial time by Theorem 5.3). By Lemma 4.4, we have that Γ, ϱ, (¬Δσ)<sup>b</sup> |=$_{BD}$ ⊥ iff Γ<sup>cl</sup>, ϱ<sup>cl</sup>, ((¬Δσ)<sup>b</sup>)<sup>cl</sup> |=$_{CPL}$ ⊥. Since Γ ⊆ L<sub>BD</sub>, Γ<sup>cl</sup> is ~-free (cf. Definition 4.2). As ϱ ∧ (¬Δσ)<sup>b</sup> is BD-satisfiable by assumption, then so is ϱ<sup>cl</sup> ∧ ((¬Δσ)<sup>b</sup>)<sup>cl</sup> (by Lemma 4.4). Thus, there is no variable r such that r and ~r occur in ϱ<sup>cl</sup> ∧ ((¬Δσ)<sup>b</sup>)<sup>cl</sup>. Now take Γ<sup>cl</sup> and substitute every p that occurs in ϱ<sup>cl</sup> ∧ ((¬Δσ)<sup>b</sup>)<sup>cl</sup> positively (resp. negatively) with τ (resp. ⊥). We then exhaustively apply the following CPL-equivalence-preserving transformations to all subformulas of $\bigwedge_{\phi \in \Gamma^{\text{cl}}} \phi$, denoting the result by (Γ<sup>cl</sup>)<sup>⊗</sup>:

$$ \tau \wedge \psi \rightsquigarrow \psi \qquad \tau \vee \psi \rightsquigarrow \tau \qquad \bot \wedge \psi \rightsquigarrow \bot \qquad \bot \vee \psi \rightsquigarrow \psi \qquad (5) $$

Clearly, (Γ<sup>cl</sup>)<sup>⊗</sup> can be computed in polynomial time in the size of Γ<sup>cl</sup>. Moreover, one can see that if (Γ<sup>cl</sup>)<sup>⊗</sup> = ⊥, then Γ<sup>cl</sup>, ϱ<sup>cl</sup>, ((¬Δσ)<sup>b</sup>)<sup>cl</sup> |=$_{CPL}$ ⊥ holds. To complete the proof, we show that if (Γ<sup>cl</sup>)<sup>⊗</sup> ≠ ⊥, then Γ<sup>cl</sup>, ϱ<sup>cl</sup>, ((¬Δσ)<sup>b</sup>)<sup>cl</sup> |=$_{CPL}$ ⊥. Let us assume (Γ<sup>cl</sup>)<sup>⊗</sup> ≠ ⊥ and set v(r) = T for every r ∈ Prop((Γ<sup>cl</sup>)<sup>⊗</sup>). It is clear that v((Γ<sup>cl</sup>)<sup>⊗</sup>) = T since (Γ<sup>cl</sup>)<sup>⊗</sup> is ~-free (cf. Definition 4.2). Now, we extend v to the variables occurring in ϱ<sup>cl</sup> and ((¬Δσ)<sup>b</sup>)<sup>cl</sup> as expected: if s occurs, we set v(s) = T, if ~s occurs, we set v(s) = F. As ϱ<sup>cl</sup> ∧ ((¬Δσ)<sup>b</sup>)<sup>cl</sup> is CPL-satisfiable, we now have $v\left(\bigwedge_{\phi \in \Gamma^{\text{cl}}} \phi \wedge \varrho^{\text{cl}} \wedge ((\neg \Delta \sigma)^b)^{\text{cl}}\right) = T$, as required. □

COROLLARY 5.7. It can be decided in polynomial time whether Γ, τ ̸|∈<sub>BD</sub> ⊥ given Γ ⊆ L<sub>BD</sub> and an L<sub>Δ</sub>-term τ.

PROOF. The statement follows from Theorem 5.6 since ⊥ ≡ △p ∧ ¬△p.

On the other hand, if the background theory is given in L<sub>⊤</sub>, term entailment becomes intractable in L<sub>Δ</sub> too.

LEMMA 5.8. Let φ be a formula in CNF such that the clauses of the form $\bigvee_{i=1}^{m} \sim p_i \vee \bigvee_{j=1}^{n} q_j$ are represented as $\bigwedge_{i=1}^{m} p_i \supset \bigvee_{j=1}^{n} q_j$ and the clauses $\bigvee_{i=1}^{m} \sim p_i$ are represented as $\bigwedge_{i=1}^{m} p_i \supset \bot$. Define φ<sup>#</sup> as φ where ⊥ is replaced with r ∉ Prop(φ). Then φ is CPL-unsatisfiable iff φ<sup>#</sup>, ¬△r |=$_{BD}$ ⊥.

PROOF. If φ is CPL-satisfiable, let v be a classical valuation such that v(φ) = T. Now, define v(r) = F. It is clear that v(φ<sup>#</sup>) = v(¬△r) = T but v(⊥) = F. Hence, φ<sup>#</sup>, ¬△r ̸|=$_{BD}$ ⊥. Conversely, let φ<sup>#</sup>, ¬△r ̸|=$_{BD}$ ⊥ and v be a BD valuation such that v(φ<sup>#</sup> ∧ ¬△r) ∈ {T, B}. Now, define v<sup>cl</sup>(p) = T iff v(p) ∈ {T, B}. It is easy to see that v<sup>cl</sup>(φ) = T, as required. □

THEOREM 5.9. It is coNP-complete to decide whether Γ, ϱ |=$_{BD}$ σ, given Γ ⊆ L<sub>⊤</sub> and L<sub>Δ</sub>-terms ϱ and σ.
**PROOF.** Membership is straightforward, so we only give hardness, which is by reduction from classical unsatisfiability of propositional CNF formulas. Let $\phi$ be in CNF represented as in Lemma 5.8 and $s \notin \text{Prop}(\phi) \cup \{r\}$. It is immediate from Lemma 5.8 that $\phi$ is CPL-unsatisfiable iff $\phi^{\#}, \neg\Delta r \models_{\text{BD}} s$. Indeed, $\phi$ is CPL-unsatisfiable iff $\phi^{\#} \wedge \neg\Delta r$ is BD-unsatisfiable. But this is equivalent to $\phi^{\#}, \neg\Delta r \models_{\text{BD}} s$. $\square$

## 5.2 Entailment of Formulas From Terms

Let us now consider the complexity of entailment of $\mathcal{L}_{\text{BD}}$- and $\mathcal{L}_{\sqsuperscript{}}$-formulas$^6$ by $\mathcal{L}_{\circ}$-terms and $\mathcal{L}_{\Delta}$-terms. We begin with $\mathcal{L}_{\circ}$-terms. The following statement is straightforward.

**THEOREM 5.10.** It is coNP-complete to decide whether $\phi \models_{\text{BD}} \chi$, given an atomic $\mathcal{L}_{\circ}$-term $\phi$ and $\chi \in \mathcal{L}_{\text{BD}}$.

**PROOF.** Membership is immediate as $\text{BD}_{\circ}$-entailment is in coNP. To show coNP-hardness, observe that $\chi$ is CPL-valid iff $\bigwedge \circ p \models_{\text{BD}} \chi$ since $\circ p$ ensures $v(p) \in \{\text{T}, \text{F}\}$ and $\wedge, \vee$, and $\neg$ behave classically on $\text{T}$ and $\text{F}$. $\square$

On the other hand, if $\phi$ is an $\mathcal{L}_{\Delta}$-term, $\phi \models_{\text{BD}} \chi$ can be decided in deterministic polynomial time.

**THEOREM 5.11.** It can be decided in polynomial time whether $\phi \models_{\text{BD}} \chi$, given an $\mathcal{L}_{\Delta}$-term $\phi$ and $\chi \in \mathcal{L}_{\text{BD}}$.

**PROOF.** Note first that if $\phi$ is BD-unsatisfiable, then $\phi \not\models_{\text{BD}} \chi$. By Theorem 5.3, it takes polynomial time to determine whether an $\mathcal{L}_{\Delta}$-term is unsatisfiable. Thus, we consider the case when $\phi$ is satisfiable. The proof is dual to that of Theorem 5.6.

We assume w.l.o.g. that $\chi$ is in NNF. By Lemma 4.4, we have that $\phi \models_{\text{BD}} \chi$ is equivalent to $\phi^{\text{cl}} \models_{\text{CPL}} \chi^{\text{cl}}$. Now, we take $\chi^{\text{cl}}$ and substitute every variable $p$ that occurs positively (resp. negatively) in $\phi^{\text{cl}}$ with $\top$ (resp. $\bot$), then apply reductions from (5). Note that the reductions can be performed in polynomial time w.r.t. the length of $\chi$. Furthermore, it is clear that, for the resulting formula $(\chi^{\text{cl}})^{\circ}$, if $(\chi^{\text{cl}})^{\circ} = \top$, then $\phi^{\text{cl}} \models_{\text{CPL}} \chi^{\text{cl}}$. On the other hand, if $(\chi^{\text{cl}})^{\circ} \neq \top$, then either $(\chi^{\text{cl}})^{\circ} = \bot$ (in which case, the entailment evidently fails) or $(\chi^{\text{cl}})^{\circ} = \psi$ for some $\sim$-free $\psi \in \mathcal{L}_{\text{BD}}$. We construct a falsifying valuation as follows: for every $p \in \text{Prop}(\psi)$, we set $v(p) = \text{F}$ and for every $q \in \text{Prop}(\phi^{\text{cl}})$, we set $v(q) = \text{T}$ iff $\sim q$ does not occur in $\phi^{\text{cl}}$. As reductions in (5) preserve CPL-equivalence, we have that $v(\phi^{\text{cl}}) = \text{T}$ and $v(\chi^{\text{cl}}) = \text{F}$. It follows that we obtain a polynomial-time entailment procedure by first checking satisfiability of $\phi$, then computing $(\chi^{\text{cl}})^{\circ}$ and checking whether it is equal to $\top$. $\square$

Again, just as in the case of $\mathcal{L}_{\sqsuperscript{}}$-theories, the entailment of $\mathcal{L}_{\sqsuperscript{}}$-formulas from $\mathcal{L}_{\Delta}$-terms is also intractable. The following statement is dual to Theorem 5.9.

**THEOREM 5.12.** It is coNP-complete to decide whether $\tau \models_{\text{BD}} \chi$ given an $\mathcal{L}_{\Delta}$-term $\tau$ and $\chi \in \mathcal{L}_{\sqsuperscript{}}$.

**PROOF.** We prove coNP-hardness by a reduction from CPL validity. Let $\chi$ be a formula over $\{\bot, \wedge, \vee, \sqsuperscript{\top}\}$ and $r \notin \text{Prop}(\chi)$. We show that $\chi$ is CPL-valid iff $\neg\Delta r \models_{\text{BD}} \chi^{\#}$ (cf. Lemma 5.8 for the definition of $\chi^{\#}$). The argument is analogous to that in Lemma 5.8. Indeed, let $\neg\Delta r \not\models_{\text{BD}} \chi^{\#}$. Then there is a BD valuation $v$ such that $v(\neg\Delta r) = \text{T}$ and $v(\chi^{\#}) \notin \{\text{T}, \text{B}\}$. Defining $v^{\text{cl}}$ as in Lemma 5.8, we immediately have that $v^{\text{cl}}(\chi^{\#}) = \text{F}$, whence, $v^{\text{cl}}(\chi) = \text{F}$. Conversely, if $v(\chi) = \text{F}$ for some classical valuation $v$, we additionally define $v(r) = \text{F}$. It is clear that $v(\chi^{\#}) = \text{F}$ and $v(\neg\Delta r) = \text{T}$, i.e., $\neg\Delta r \not\models_{\text{BD}} \chi^{\#}$, as required. $\square$

Finally, we observe that in the presence of a theory $\Gamma$, the entailment of $\mathcal{L}_{\text{BD}}$-formulas (and thus, $\mathcal{L}_{\sqsuperscript{}}$-formulas, as well) from terms becomes coNP-complete.

**THEOREM 5.13.** It is coNP-complete to decide whether $\Gamma, \tau \models_{\text{BD}} \psi$, given $\Gamma \cup \{\psi\} \in \mathcal{L}_{\text{BD}}$ and an $\mathcal{L}_{\Delta}$-term or an atomic $\mathcal{L}_{\circ}$-term $\tau$.

<footnote>$^6$Recall that in the abduction problems we consider, the theory and observation are formulated in $\mathcal{L}_{\text{BD}}$ or $\mathcal{L}_{\sqsuperscript{}}$ while solutions are formulated in $\mathcal{L}_{\circ}$ or $\mathcal{L}_{\Delta}$.</footnote>
PROOF. The proof is a straightforward reduction from the coNP-complete entailment problem for $\mathcal{L}_{BD}$-formulas: $\phi \models_{BD} \chi$ iff $\phi, p \models_{BD} \chi$ with $p \notin \text{Prop}(\phi \wedge \chi)$. □

## 5.3 Consistent Entailment

Finally, we consider the complexity of determining whether a theory and a term entail another formula consistently.

LEMMA 5.14. Given $\Gamma \cup \{\chi\} \subseteq \mathcal{L}_{BD}$, $\sigma$ an $\mathcal{L}_{\Delta}$-term, and $\tau$ an atomic $\mathcal{L}_{\circ}$-term:

(1) deciding whether $\Gamma$, $\sigma \models_{BD}^{\text{cons}} \chi$ is coNP-complete;

(2) deciding whether $\Gamma, \tau \models_{BD}^{\text{cons}} \chi$ is DP-complete.

PROOF. We begin with Statement 1. coNP-membership is immediate since entailment is in coNP and verifying the consistency of $\Gamma$, $\sigma$ can be done in polynomial time using Corollary 5.7. For hardness, we reduce BD-entailment to BD-consistent entailment as follows:

$$ \phi \models_{BD} \chi \text{ iff } \phi \lor p, q \models_{BD}^{\text{cons}} \chi \lor p \qquad (p, q \notin \text{Prop}[\{\phi, \chi\}], \sigma = q) $$

Let $\phi \not\models_{BD} \chi$. We can thus find $v$ such that $v(\phi) \in \{\mathbf{T}, \mathbf{B}\}$ and $v(\chi) \notin \{\mathbf{T}, \mathbf{B}\}$. Since $p$ and $q$ are fresh, we let $v(p) = \mathbf{F}$ and $v(q) = \mathbf{T}$ which falsifies the consistent entailment. Conversely, let $\phi \lor p, q \not\models_{BD}^{\text{cons}} \chi \lor p$. It is clear that $\{\phi \lor p, q\}$ is BD-satisfiable. Thus, there is a valuation such that $v(\phi \lor p) \in \{\mathbf{T}, \mathbf{B}\}$, $v(q) \in \{\mathbf{T}, \mathbf{B}\}$ but $v(\chi \lor p) \notin \{\mathbf{T}, \mathbf{B}\}$. Hence, $v(\phi) \in \{\mathbf{T}, \mathbf{B}\}$ and $v(\chi) \notin \{\mathbf{T}, \mathbf{B}\}$, as required.

For Statement 2, membership follows from Corollary 5.5 and Theorem 5.13. To show hardness, we reduce the DP-complete Sat-UnSat problem for CPL to BD-consistent entailment. Let $\phi, \chi$ be propositional formulas and assume w.l.o.g. that $\text{Prop}(\phi) \cap \text{Prop}(\chi) = \emptyset$. Set $\Xi = \text{Prop}(\phi) \cup \text{Prop}(\chi)$ and pick $p \notin \Xi$. We show that $\phi$ is CPL-satisfiable and $\chi$ is CPL-unsatisfiable iff $\phi, p \wedge \bigwedge_{q \in \Xi} \circ q \models_{BD}^{\text{cons}} p \wedge \neg \chi$.

If $\phi$ is CPL-unsatisfiable, then $\phi \wedge p \wedge \bigwedge_{q \in \Xi} \circ q$ is BD-unsatisfiable, so the consistent entailment fails. If $\chi$ is CPL-satisfiable, let $v$ be a classical valuation such that $v(\chi) = \mathbf{T}$ (whence, $v(p \wedge \neg \chi) = \mathbf{F}$) and $v(\phi \wedge p) = \mathbf{T}$ (recall that $\text{Prop}(\phi) \cap \text{Prop}(\chi) = \emptyset$, so such valuation must exist unless $\phi$ is CPL-unsatisfiable). Again, the consistent entailment fails.

For the converse, let $\phi$ be CPL-satisfiable and $\chi$ be CPL-unsatisfiable. It is clear that $\phi, p \wedge \bigwedge_{q \in \Xi} \circ q \models_{BD}^{\text{cons}} p \wedge \neg \chi$ because $p \wedge \bigwedge_{q \in \Xi} \circ q \models_{BD} p \wedge \neg \chi$ and $\phi \wedge p \wedge \bigwedge_{q \in \Xi} \circ q$ is BD-satisfiable as $p \notin \text{Prop}(\phi)$ and $\phi$ is CPL-satisfiable. □

If the theory is given in $\mathcal{L}_{\succ}$, consistent entailment becomes DP-hard even with $\mathcal{L}_{\Delta}$-terms.

LEMMA 5.15. Given $\Gamma \subseteq \mathcal{L}_{\succ}, \chi \in \mathcal{L}_{BD}$, and an $\mathcal{L}_{\Delta}$-term $\tau$, it is DP-complete to decide whether $\Gamma, \tau \models_{BD}^{\text{cons}} \chi$.

PROOF. Membership is straightforward, so we consider hardness. The idea is the same as in Lemma 5.14. We establish a reduction from Sat-UnSat. Let $\text{Prop}(\phi) \cap \text{Prop}(\chi) = \emptyset$. We recall the definition of $\phi^{\#}$ from Lemma 5.8 and show that $\phi$ is CPL-satisfiable and $\chi$ is CPL-unsatisfiable iff

$$ \phi^{\#}, \bigwedge_{p \in \text{Prop}(\chi)} (p \lor \neg p), \neg \Delta r \models_{BD}^{\text{cons}} \neg \chi \lor \bigvee_{p \in \text{Prop}(\chi)} (p \wedge \neg p) $$

For the ‘if’ direction, it is immediate that $\phi^{\#}, \bigwedge_{p \in \text{Prop}(\chi)} (p \lor \neg p), \neg \Delta r \not\models_{BD} \bot$ — we just take the classical valuation $v$ that satisfies $\phi$ and define $v(r) = \mathbf{F}$ and $v(p) = \mathbf{T}$ for every $p \in \text{Prop}(\chi)$. Moreover, since $\chi$ is CPL-unsatisfiable, $\neg \chi$ is classically valid. Hence, by Proposition 2.6, we have that $\bigwedge_{p \in \text{Prop}(\chi)} (p \lor \neg p) \models_{BD} \neg \chi \lor \bigvee_{p \in \text{Prop}(\chi)} (p \wedge \neg p)$. □
<table><caption>Table 2. Complexity of abductive reasoning problems. All results hold both for BD and $BD_2$, except the result in the top left-most corner, where the coNP-completeness result is for BD problems, and the DP-completeness (in brackets) is for $BD_2$. Notation for different types of solution sets (e.g. $S(\mathbb{P})$) can be found in Convention 2. We use 'X-c.' to abbreviate X-complete.</caption><thead><tr><th>Recognition</th><th>L<sub>Δ</sub></th><th>L<sub>o</sub></th><th>CPL</th></tr></thead><tbody><tr><td>τ ∈ S(ℝ)?</td><td>coNP-c. [DP-c.]</td><td>DP-c.</td><td>Thm. 6.1, 6.2, 6.3</td></tr><tr><td>τ ∈ S<sup>P</sup>(ℝ)?</td><td>coNP-c. [DP-c.]</td><td>DP-c.</td><td>Thm. 6.1, 6.2, 6.3</td></tr><tr><td>τ ∈ S<sup>BD</sup>(ℝ)?</td><td>DP-c.</td><td>DP-c.</td><td>Thm. 6.5</td></tr><tr><td>τ ∈ S<sup>Th</sup>(ℝ)?</td><td>in Π<sub>2</sub><sup>P</sup></td><td>in Π<sub>2</sub><sup>P</sup></td><td>Thm. 6.6</td></tr><tr><td>Existence</td><td>L<sub>Δ</sub></td><td>L<sub>o</sub></td><td>CPL</td></tr><tr><td>S(ℝ) ≠ Ø?</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Thm. 6.7</td></tr><tr><td>S<sup>P</sup>(ℝ) ≠ Ø?</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Thm. 6.7</td></tr><tr><td>Relevance</td><td>L<sub>Δ</sub></td><td>L<sub>o</sub></td><td>CPL</td></tr><tr><td>w.r.t. S(ℝ)</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Thm. 6.8</td></tr><tr><td>w.r.t. S<sup>P</sup>(ℝ)</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Thm. 6.8</td></tr><tr><td>w.r.t. S<sup>BD</sup>(ℝ)</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Σ<sub>2</sub><sup>P</sup>-c.</td><td>Thm. 6.8</td></tr><tr><td>w.r.t. S<sup>Th</sup>(ℝ)</td><td>in Σ<sub>3</sub><sup>P</sup></td><td>in Σ<sub>3</sub><sup>P</sup></td><td>Thm. 6.9</td></tr><tr><td>Necessity</td><td>L<sub>Δ</sub></td><td>L<sub>o</sub></td><td>CPL</td></tr><tr><td>w.r.t. S(ℝ)</td><td>Π<sub>2</sub><sup>P</sup>-c.</td><td>Π<sub>2</sub><sup>P</sup>-c.</td><td>Thm. 6.8</td></tr><tr><td>w.r.t. S<sup>P</sup>(ℝ)</td><td>Π<sub>2</sub><sup>P</sup>-c.</td><td>Π<sub>2</sub><sup>P</sup>-c.</td><td>Thm. 6.8</td></tr><tr><td>w.r.t. S<sup>BD</sup>(ℝ)</td><td>Π<sub>2</sub><sup>P</sup>-c.</td><td>Π<sub>2</sub><sup>P</sup>-c.</td><td>Thm. 6.8</td></tr><tr><td>w.r.t. S<sup>Th</sup>(ℝ)</td><td>in Π<sub>3</sub><sup>P</sup></td><td>in Π<sub>3</sub><sup>P</sup></td><td>Thm. 6.9</td></tr></tbody></table>

For the converse direction, assume first that $\chi$ is CPL-satisfiable and let $v(\chi) = T$ for some fixed classical valuation $v$. It is clear that $v(\bigwedge_{p \in \text{Prop}(\chi)} (p \lor \neg p)) = T$. Moreover, since $\text{Prop}(\phi^{\#}) \cap \text{Prop}(\chi) = \emptyset$, we immediately have that $\phi^{\#}, \bigwedge_{p \in \text{Prop}(\chi)} (p \lor \neg p), \neg \Delta r \notin_{BD}^{\text{cons}} \neg \chi \lor \bigvee_{p \in \text{Prop}(\chi)} (p \land \neg p)$. Indeed, if $\phi^{\#} \land \neg \Delta r$ is BD-satisfiable, the entailment fails. If $\phi^{\#} \land \neg \Delta r$ is BD-unsatisfiable, then it cannot consistently entail anything.

Now let $\phi$ be CPL-unsatisfiable. By Lemma 5.8, we have that $\phi^{\#} \land \neg \Delta r$ is BD-unsatisfiable. Thus,

$$ \phi^{\#}, \bigwedge_{p \in \text{Prop}(\chi)} (p \lor \neg p), \neg \Delta r \notin_{BD}^{\text{cons}} \neg \chi \lor \bigvee_{p \in \text{Prop}(\chi)} (p \land \neg p) $$

as required.

□

# 6 Complexity of Abduction in the Expansions of BD

This section considers the complexity of the principal decision problems related to BD abduction, namely, solution recognition, solution existence, and relevance and necessity of hypotheses. Table 2 summarises the obtained results for BD abduction, alongside results for classical abduction.
## 6.1 Solution Recognition

We can use Lemmas 5.14 and 5.15 to establish the complexity of recognising arbitrary and proper solutions. For both $\mathcal{L}_{\Delta}$-solutions w.r.t. $\mathcal{L}_{\Delta}$-theories and $\mathcal{L}_{\circ}$-solutions w.r.t. $\mathcal{L}_{BD}$- or $\mathcal{L}_{\Delta}$-theories, we find that (proper) solution recognition is DP-complete, which is the same complexity as in CPL. Intuitively, the DP complexity stems from the need to perform both entailment (coNP) and consistency (NP) checks. A lower complexity (coNP) is obtained for $\mathcal{L}_{\Delta}$-solutions w.r.t. $\mathcal{L}_{BD}$-theories, due to the fact that consistency is tractable in this setting.

**THEOREM 6.1.** It is coNP-complete to decide, given a BD abduction problem $\mathbb{P}$ and an $\mathcal{L}_{\Delta}$-term $\sigma$, whether $\sigma$ is a (proper) solution of $\mathbb{P}$.

**PROOF.** The coNP-completeness of recognising $\sigma \in \mathcal{S}(\mathbb{P})$ (recall Convention 2 for the solution types notation) follows immediately from Lemma 5.14 since $\sigma$ is a solution of $\langle \Gamma, \chi, H \rangle$ iff $\Gamma, \sigma \models_{BD}^{\text{cons}} \chi$. For proper solutions, we observe that recognising an arbitrary solution is reducible to the recognition of a proper solution as follows: if we let $p \notin \text{Prop}[\Gamma \cup \{\chi\} \cup H]$, then $\sigma$ is a solution of $\langle \Gamma, \chi, H \rangle$ iff $\sigma$ is a proper solution of $\langle \Gamma \cup \{p\}, p \wedge \chi, H \rangle$. Indeed, $\Gamma, \sigma \models_{BD} \chi$ holds iff $\Gamma, p, \sigma \models_{BD} \chi \wedge p$ holds, and likewise, $\Gamma, p, \sigma \models_{BD} \bot$ iff $\Gamma, \sigma \models_{BD} \bot$. Moreover, since $p$ does not occur in $\tau$, it is clear that $\sigma \models_{BD} \chi \wedge p$. This establishes coNP-hardness. For membership, we note that checking the properness condition ($\sigma \not\models_{BD} \chi$) is in $\mathbb{P}$ since $\sigma$ is an $\mathcal{L}_{\Delta}$-term (Theorem 5.11), so we remain in coNP. $\square$

**THEOREM 6.2.** It is DP-complete to decide, given a BD$_{\Delta}$ abduction problem $\mathbb{P} = \langle \Gamma, \chi, H \rangle$ and an $\mathcal{L}_{\Delta}$-term $\sigma$, whether $\sigma$ is a (proper) solution of $\mathbb{P}$.

**PROOF.** For arbitrary solutions, the result follows immediately from Lemma 5.15. To obtain the statement for proper solutions, we proceed as follows. Hardness can be obtained via a reduction from arbitrary solution recognition in the same way as in Theorem 6.1. For membership, given a term $\sigma$, we use an NP-oracle that guesses two valuations: $v_{\text{sat}}$ that witnesses $\Gamma, \sigma \not\models_{BD} \bot$ and $v_{\text{proper}}$ that witnesses $\sigma \not\models_{BD} \chi$. Simultaneously (as we do not need the results of these NP-checks), we conduct a coNP-check that $\Gamma, \sigma \models_{BD} \chi$. It follows by Definition 3.5 that $\sigma$ is a proper solution to $\mathbb{P}$ iff NP- and coNP-checks succeed. $\square$

**THEOREM 6.3.** It is DP-complete to decide, given a BD (or $BD_{\Delta}$) abduction problem $\mathbb{P}$ and an atomic $\mathcal{L}_{\circ}$-term $\sigma$, whether $\sigma$ is a (proper) solution of $\mathbb{P}$.

**PROOF.** The arguments are the same as in the proof of Theorem 6.2, but we use the complexity results for atomic $\mathcal{L}_{\circ}$-terms from Table 1 and Lemma 5.14. $\square$

We next show how to recognise $\models_{BD}$-minimal solutions. To deal with $\mathcal{L}_{\circ}$-solutions, we need the following straightforward statement.

**LEMMA 6.4.** For an atomic $\mathcal{L}_{\circ}$-term $\sigma$, define

$$ \sigma^{\prime V} = \{ \mathbf{TB}_p \mid \text{only } p \text{ is in } \sigma \} \cup \{ \mathbf{FB}_p \mid \text{only } \neg p \text{ is in } \sigma \} \cup \{ \mathbf{Tp} \mid p, \circ p \in \text{Lit}_{\circ}(\sigma) \} \cup \{ \mathbf{Fp} \mid \neg p, \circ p \in \text{Lit}_{\circ}(\sigma) \} \cup \{ \mathbf{BN}_p \mid \text{only } \bullet p \text{ is in } \sigma \} \cup \{ \mathbf{TF}_p \mid \text{only } \circ p \text{ is in } \sigma \} \cup \{ \mathbf{B}_p \mid \text{any two out of } \{ p, \neg p, \bullet p \} \text{ are in } \sigma \} $$

Then if we treat prefixes $\bar{X}$ and $\bar{Y}$ as sets, it holds that

$$ \sigma \models_{BD} \sigma' \quad \text{iff} \quad \forall p \in \text{Prop} : \text{ if } \bar{Y}p \in \sigma^{\prime V}, \text{ then } \exists \bar{X}(\bar{X}p \in \sigma^{\prime V} \& \bar{X} \subseteq \bar{Y}) $$

**PROOF.** Immediate consequence of Lemma 5.1. $\square$

**THEOREM 6.5.** It is DP-complete to decide, given a BD (or $BD_{\Delta}$) abduction problem $\mathbb{P}$ and a term $\sigma$, whether $\sigma$ is a $\models_{BD}$-minimal ($\mathcal{L}_{\circ}$- or $\mathcal{L}_{\Delta}$-) solution of $\mathbb{P}$.
PROOF. We start by showing membership in DP for the $\mathcal{L}_{\Delta}$ case, assuming that $\mathbb{P}$ is a BD$_{\Delta}$ abduction problem. Let $\sigma$ be an $\mathcal{L}_{\Delta}$-term. We can w.l.o.g. assume (recall Proposition 3.7) that all $\Delta$'s in $\sigma$ occur under $\neg$, i.e., $\sigma = \sigma^b$. It is clear from Lemma 4.4 that given two $\mathcal{L}_{\Delta}$-terms $\sigma^b$ and $\sigma'^b$, we have $\sigma^b \models_{\text{BD}} \sigma'^b$ iff $\text{Lit}_{\Delta}(\sigma^b) \supseteq \text{Lit}_{\Delta}(\sigma'^b)$. We can now proceed as follows. Given $\sigma$, we make a call to an NP oracle that guesses (linearly many) valuations $v_{\text{sat}}$, $v_{\text{proper}}$, and $v_l$ (for each literal $l$ of $\sigma$) and verifies that these valuations witness that (i) $\Gamma, \sigma \nvDash_{\text{BD}} \bot$, (ii) $\sigma \nvDash_{\text{BD}} \chi$, and (iii) $\Gamma, \sigma^{-l} \nvDash_{\text{BD}} \chi$ for every literal $l$ of $\sigma$, where $\sigma^{-l}$ being the result of deleting one $\mathcal{L}_{\Delta}$-literal from $\sigma$. At the same time (as we do not need the results of other guesses), we make a coNP check that $\Gamma, \sigma \models_{\text{BD}} \chi$. It follows from the definition of $\models_{\text{BD}}$-minimal solutions that $\sigma$ is a $\models_{\text{BD}}$-minimal solution iff the NP and coNP checks succeed.

Now let $\sigma$ be an atomic $\mathcal{L}_{\circ}$-term. We proceed in the same manner as with $\mathcal{L}_{\Delta}$-terms, but now we cannot just remove literals because of situations when one term entails another even though they do not have common atomic literals as in $p \wedge \neg p \models_{\text{BD}} \bullet p$. To circumvent this problem, we transform $\sigma$ into $\sigma'^{\vee}$ (defined in Lemma 6.4) and note that $\sigma \equiv \sigma' \text{ iff } \sigma'^{\vee} = \sigma'^{\vee}$. Now, given $\sigma = \bigwedge_{i=1}^{m} l_i$, we only need to check terms that can be obtained by removing a literal (there are $m$ of those) and terms corresponding to $\sigma'^{\vee}$ obtained from $\sigma^{\vee}$ by replacing one $\bar{X}p$ with some $\bar{Y}p$ such that $\bar{X} \subseteq \bar{Y}$ (there are at most $2m$ of those).

For DP-hardness, we reduce the recognition of classical prime implicants which is DP-complete due to (Marquis 2000, Proposition 115) to recognition of $\models_{\text{BD}}$-minimal $\mathcal{L}_{\text{BD}}$-solutions (thus, the bound will work for BD$_{\Delta}$ as well, and for $\mathcal{L}_{\Delta}$- and $\mathcal{L}_{\circ}$-solutions). Namely, let $\chi \in \mathcal{L}_{\text{BD}}$ and $\tau$ be a term. We assume w.l.o.g. that $\chi$ is classically satisfiable and show that $\tau$ is a prime implicant of $\chi$ iff $\tau$ is a $\models_{\text{BD}}$-minimal solution of

$$ \mathbb{P} = \left\{ \left\{ \bigwedge_{p \in \text{Prop}(\chi \wedge q)} (p \vee \neg p), q \right\}, (\chi \wedge q) \vee \bigvee_{p \in \text{Prop}(\chi)} (p \wedge \neg p), H \right\} $$

with $H = \{r | r \in \text{Prop}(\chi)\} \cup \{\neg r | r \in \text{Prop}(\chi)\}$ and $q \notin H$. Note that all improper solutions of $\mathbb{P}$ are classically unsatisfiable.

Now let $\tau$ be a classical prime implicant of $\chi$. Then we have that $\tau \models_{\text{CPL}}^{\text{cons}} \chi$ and there is no $\tau'$ such that $\tau \models_{\text{CPL}} \tau'$, $\tau' \nvDash_{\text{CPL}} \tau$, and $\tau' \nvDash_{\text{CPL}}^{\text{cons}} \chi$. By Proposition 2.6, we have that $\tau$ is indeed a solution of $\mathbb{P}$ (observe from Definition 2.2 that $\tau$ is consistent with any $\mathcal{L}_{\text{BD}}$-theory because it only contains $\neg$ and $\wedge$). It is a proper solution because it is classically satisfiable and does not contain $q$. It remains to show that $\tau$ is a $\models_{\text{BD}}$-minimal solution. For this, assume for contradiction that there is some weaker proper solution $\tau'$. But $\tau'$ must be classically satisfiable, whence, $\tau \models_{\text{CPL}} \tau'$ (because term entailment in BD and CPL coincide$^7$ for the case of classically satisfiable $\mathcal{L}_{\text{BD}}$-terms). Moreover, by Proposition 2.6, we would have that $\tau' \models_{\text{CPL}} \chi$ which would contradict the assumption of $\tau$ being a prime implicant.

The converse direction can be shown similarly. Let $\tau$ be a $\models_{\text{BD}}$-minimal solution of $\mathbb{P}$. Again, by Proposition 2.6, we have that $\tau \models_{\text{CPL}} \chi$ and that there is no other $\tau'$ such that $\tau' \models_{\text{CPL}} \chi$ and $\tau \models_{\text{BD}} \tau'$ for else we would have $\tau \models_{\text{BD}} \tau'$ and $\tau'$ be a proper solution of $\mathbb{P}$ (again, recall that all proper solutions of $\mathbb{P}$ are classically satisfiable). $\square$

In the case of theory-minimal solutions, we establish membership in $\Pi_2^p$. We expect that this case is indeed harder than $\models_{\text{BD}}$-minimality, intuitively because the presence of the theory means we cannot readily identify a polynomial number of candidate better solutions to check. We leave the search for a matching lower bound for future work and remark that, to the best of our knowledge, the complexity of the analogous problem in CPL is also unknown.

THEOREM 6.6. It is in $\Pi_2^p$ to decide, given a BD (or BD$_{\Delta}$) abduction problem $\mathbb{P}$ and $\sigma$ which is an $\mathcal{L}_{\Delta}$-term or atomic $\mathcal{L}_{\circ}$-term, whether $\sigma$ is a theory-minimal solution of $\mathbb{P}$.

<footnote>$^7$Observe that $\tau \models_{\text{BD}} \tau'$ iff $\text{Lit}(\tau) \supseteq \text{Lit}(\tau')$ iff $\tau \models_{\text{CPL}} \tau'$.</footnote>
PROOF. Let $\mathbb{P} = (\Gamma, \chi, H)$ be a BD$_\square$ abduction problem, and $\sigma$ be the $\mathcal{L}_\Delta$- or atomic $\mathcal{L}_\circ$-term we wish to test. We outline a $\Sigma_2^P$ procedure for the complementary problem of testing whether $\sigma$ is not a theory-minimal $\mathcal{L}_\Delta$-solution. We first guess either ‘not a proper solution’ or another term $\sigma'$ in the considered language. In the former case, due to the coNP- / DP-completeness of proper solution recognition (Theorems 6.1 and 6.3), we can make (one or two) calls to an NP oracle to verify that $\sigma$ is indeed not a proper solution (in which case we return yes). In the latter case, we can make a few calls to an NP oracle to verify that $\sigma'$ is a proper solution such that $\Gamma, \sigma \models_{BD} \sigma'$ and $\Gamma, \sigma' \not\models_{BD} \sigma$ (returning yes if the calls show this to be the case). It is easy to see that the procedure we have just described will return yes iff the input $\sigma$ is not a theory-minimal solution, which yields the desired membership in $\Pi_2^P$ for the original problems. □

## 6.2 Solution Existence

We now turn to the fundamental task of determining whether an abduction problem has a solution. To establish the complexity of deciding whether $\mathcal{S}(\mathbb{P}) = \emptyset$, we provide reductions from classical abduction problems.

THEOREM 6.7. It is $\Sigma_2^P$-complete to decide whether a BD (BD$_\square$) abduction problem has a (proper) $\mathcal{L}_\Delta$- or $\mathcal{L}_\circ$-solution.

PROOF. Membership in $\Sigma_2^P$ can be shown using a simple guess-and-check procedure, using Theorems 6.1 and 6.3. To show $\Sigma_2^P$-hardness for BD (hence BD$_\square$) abduction problems, we will give a reduction from the solution existence task for classical abduction problems $\mathbb{P}_{cl} = (\Gamma_{cl}, \chi_{cl}, H)$ of the following form:<fnref n="8" />

$$ 
\begin{align} 
\Gamma_{cl} &= \{\neg\phi \lor (p \land \tau), \neg p \lor \tau\} \cup \{\neg r \leftrightarrow r' \mid r \in \text{Prop}(\phi) \land \text{Prop}(p \land \tau)\} \nonumber \\ 
\chi_{cl} &= p \land \tau \tag{p $\notin$ \text{Prop}(\phi \land \tau)}, \quad \tau \text{ is a term} \nonumber \\ 
H &= \{r \mid r \in \text{Prop}(\phi) \land \text{Prop}(p \land \tau)\} \cup \{r' \mid \neg r \leftrightarrow r' \in \Gamma_{cl}\} \tag{6}
\end{align} 
$$

By (Eiter and Gottlob 1995, Theorem 4.2), determining the existence of classical solutions for abduction problems of this form is $\Sigma_2^P$-hard. We reduce $\mathbb{P}_{cl}$ to $\mathbb{P}^4 = (\Gamma^4, \chi^4, H^4)$, where:

$$ \Gamma^4 = \Gamma_{cl} \cup \{q \lor \neg q \mid q \in \text{Prop}[\Gamma_{cl}]\} \qquad \chi^4 = \chi_{cl} \lor \bigvee_{q \in \text{Prop}[\Gamma_{cl}]} (q \land \neg q) \qquad H^4 = H \quad (7) $$

We begin by noting that $\mathcal{S}(\mathbb{P}_{cl}) = \mathcal{S}^P(\mathbb{P}_{cl})$ since $H \cap \text{Prop}(p \land \tau) = \emptyset$. Now let $\sigma$ be a solution of $\mathbb{P}_{cl}$. By Proposition 2.6, we have that $\sigma$ is a solution of $\mathbb{P}^4$. And since $\sigma \in \mathcal{L}_{BD}$, it is both an $\mathcal{L}_\Delta$- and $\mathcal{L}_\circ$-solution. Moreover, as $\mathcal{S}(\mathbb{P}_{cl}) = \mathcal{S}^P(\mathbb{P}_{cl})$, $\sigma \models_{CPL} \chi_{cl}$. Applying again Proposition 2.6, we obtain $\sigma$, $\bigwedge_{q \in \text{Prop}[\Gamma_{cl}]} (q \lor \neg q) \not\models_{BD}$

$\chi_{cl} \lor \bigvee_{q \in \text{Prop}[\Gamma_{cl}]} (q \land \neg q)$, hence $\sigma \not\models_{BD} \chi_{cl} \lor \bigvee_{q \in \text{Prop}[\Gamma_{cl}]} (q \land \neg q)$. Thus, $\sigma \in \mathcal{S}^P(\mathbb{P}^4)$, as required.

For the converse, let $\sigma'$ be a solution of $\mathbb{P}^4$, i.e., $\Gamma^4, \sigma' \models_{BD}^{\text{cons}} \chi^4$. From Proposition 2.6 and the definition of $\Gamma^4$ and $\chi^4$, it is immediate that $\Gamma, \sigma' \models_{CPL}^{\text{cons}} \chi$, i.e., $\sigma' \in \mathcal{S}(\mathbb{P}_{cl})$. Finally, let $\sigma' \in \mathcal{S}^P(\mathbb{P}^4)$. As H contains only positive literals and no variables from $\text{Prop}(p \land \tau)$, it follows that $\sigma' \models_{CPL} p \land \tau$. Moreover, applying Proposition 2.6, we obtain that $\Gamma_{cl}, \sigma' \models_{CPL} \chi_{cl}$ and $\Gamma_{cl}, \sigma' \models_{CPL} \chi_{cl} \perp$. This shows that $\sigma'$ is a proper solution of $\mathbb{P}_{cl}$. □

## 6.3 Relevance and Necessity of Hypotheses

Two other natural reasoning tasks that arise in the context of abduction are the recognition of which hypotheses are relevant, in the sense that they belong to at least one (minimal) solution, and which are necessary (or indispensable), as they occur in every (minimal) solution. Both of these decision problems have been investigated in the case of CPL abduction, see (Eiter and Gottlob 1995).

<footnote n="8">⁸We write $\neg r \leftrightarrow r'$ as a shorthand for $(r \land \neg r') \lor (\neg r \land r')$.</footnote>
The next theorem shows that the complexity of relevance and necessity w.r.t. (proper) solutions and $\models_{BD}$-minimal solutions coincides with the complexity of the analogous problems for ($\subseteq$-minimal) solutions in CPL.

**THEOREM 6.8.** It is $\Sigma_2^p$-complete (resp. $\Pi_2^p$-complete) to decide, given a BD or $BD_\sqsubseteq$ abduction problem $\mathbb{P} = \langle \Gamma, \chi, \mathbb{H} \rangle$ and $h \in \mathbb{H}$, whether $h$ is relevant (resp. necessary) w.r.t. $S(\mathbb{P})$. The same holds for relevance and necessity w.r.t. $S^p(\mathbb{P})$ and $S^{BD}(\mathbb{P})$.

**PROOF.** Membership is straightforward since solution recognition is coNP-complete for proper $\mathcal{L}_\Delta$-solutions and BD problems and DP-complete for proper $\mathcal{L}_\circ$-solutions or $BD_\sqsubseteq$ problems and it suffices to guess a proper solution containing (or omitting) $h$ and verify it.

For the hardness results for arbitrary and proper solutions, we construct a reduction from the class of BD abduction problems presented in (7) and adapt the approach from (Eiter and Gottlob 1995). Namely, we let $\mathbb{P}^4 = \langle \Gamma^4, \chi^4, \mathbb{H}^4 \rangle$ be as in (7) and pick fresh variables $t, t'$, and $t''$. Now set $\Xi = \text{Prop}[\Gamma^4] \cup \{t, t', t''\}$ and define $\mathbb{P}^{\text{rd}} = \langle \Gamma^{\text{rd}}, \chi^{\text{rd}}, \mathbb{H}^{\text{rd}} \rangle$ as follows.

$$ 
\begin{align} 
\Gamma^{\text{rd}} &= \{\neg t \lor \psi \mid \psi \in \Gamma^4\} \cup \{s \lor \neg s \mid s \in \Xi\} \cup \{\neg t' \lor (p \land \tau), \neg t \lor \neg t', \neg (t \lor t') \lor t''\} \nonumber \\
\chi^{\text{rd}} &= (p \land t'' \land \tau) \lor \bigvee_{s \in \Xi} (s \land \neg s) \nonumber \\
\mathbb{H}^{\text{rd}} &= \mathbb{H}^4 \cup \{t, t'\} \tag{8}
\end{align} 
$$

Now let $S^p(\mathbb{P}^4)$ be the set of all proper solutions of $\mathbb{P}^4$ and recall that $S(\mathbb{P}^4) = S^p(\mathbb{P}^4)$. We show that

$$ S^p(\mathbb{P}^{\text{rd}}) = S(\mathbb{P}^{\text{rd}}) = \underbrace{\{\varrho \land t \mid \varrho \in S(\mathbb{P}^4)\}}_{\text{R}} \cup \underbrace{\{\varrho' \land t' \mid \exists \mathbb{H}' \subseteq \mathbb{H}^4 : \varrho' = \bigwedge_{l \in \mathbb{H}'} l\}}_{\text{N}} \tag{9} $$

Observe that all solutions to $\mathbb{P}^{\text{rd}}$ must be proper since $p \notin \mathbb{H}^{\text{rd}}$ and $\mathbb{H}^{\text{rd}}$ only contains positive propositional literals. Indeed, let $\sigma$ be an $\mathcal{L}_\Delta$-term over $\mathbb{H}^{\text{rd}}$. Then $\sigma$ cannot contain $s \land \neg s$ for any $s \in \Xi$ (because negated variables do not belong to $\mathbb{H}^{\text{rd}}$), nor does it contain $p$. Thus, setting $v(p) = \mathbb{F}$ and $v(q) = \mathbb{T}$ for $q \in \text{Prop}(\sigma)$, we obtain $\sigma \not\models_{BD} \chi^{\text{rd}}$.

Furthermore, it is clear from (8) and Proposition 2.6 that $\Gamma^{\text{rd}}, t' \models_{\mathbb{BD}}^{\text{cons}} \chi^{\text{rd}}$ and thus (as $\Gamma^{\text{rd}} \cup \{\chi^{\text{rd}}\} \subseteq \mathcal{L}_{\mathbb{BD}}$), $\Gamma^{\text{rd}}, t' \land \varrho' \models_{\mathbb{BD}}^{\text{cons}} \chi^{\text{rd}}$ for every $\mathcal{L}_{\mathbb{BD}}$-term $\varrho'$ over $\mathbb{H}^4$, as well. Thus, $\mathbb{N} \subseteq S(\mathbb{P}^{\text{rd}})$. Now let $\varrho \in S(\mathbb{P})$. Again, by Proposition 2.6, we get $\Gamma^{\text{rd}}, \varrho \land t \models_{\mathbb{BD}}^{\text{cons}} \chi^{\text{rd}}$, whence $\mathbb{R} \subseteq S(\mathbb{P})$.

Conversely, let $\sigma \in S(\mathbb{P}^{\text{rd}})$. If $t' \in \sigma$, then $\sigma \in \mathbb{N}$. Otherwise, we show that $\sigma = \varrho \land t$ for some $\varrho \in S(\mathbb{P}^4)$. We reason for the contradiction. Assume first that $t$ does not occur in $\sigma$. Then set $v$ to be a classical valuation such that $v(t) = v(t') = v(t'') = \mathbb{F}$. Clearly, $v$ witnesses $\Gamma^{\text{rd}}, \sigma \not\models_{\mathbb{BD}} \chi^{\text{rd}}$. Second, let $\sigma = \sigma' \land t$ with $\sigma'$ being a term over $\mathbb{H}^4$ and $\sigma' \notin S(\mathbb{P}^4)$. As $\Gamma^4 \cup \{\sigma'\} \subseteq \mathcal{L}_{\mathbb{BD}}$ and $\sigma' \notin S(\mathbb{P}^4)$, we know that there is some BD-valuation $v$ witnessing $\Gamma^4, \sigma' \not\models_{\mathbb{BD}} (p \land \tau) \lor \bigvee (s' \land \neg s')$. Note that there is necessarily a valuation falsifying the entailment because $s' \in \text{Prop}[\Gamma^4]$.

consistency is ensured by the def of $\Gamma^{\text{rd}}$ and the fact that $r$ occurs in $\sigma$. We extend $v$ as follows: $v(t) = v(t'') = \mathbb{T}$, $v(t') = \mathbb{F}$. Thus, we have that $v(\phi) \in \{\mathbb{T}, \mathbb{B}\}$ for all $\phi \in \Gamma^{\text{rd}}$. But as $v(p \land \tau) \notin \{\mathbb{T}, \mathbb{B}\}$, $v\left(\bigvee_{s' \in \text{Prop}[\Gamma^4]} (s' \land \neg s')\right) \notin \{\mathbb{T}, \mathbb{B}\}$, and the new variables are evaluated classically, $v$ witnesses $\Gamma^{\text{rd}}, \sigma \not\models_{\mathbb{BD}} \chi^{\text{rd}}$.

Now, from (9), it follows that $\mathbb{P}^4$ has (proper) solutions iff $r$ is relevant and $t'$ is not necessary w.r.t. $S(\mathbb{P}^{\text{rd}})$. Indeed, assume that $\varrho \in S(\mathbb{P}^4)$, then $\varrho \land t \in S(\mathbb{P}^{\text{rd}})$. As $t' \notin \text{Prop}(\varrho \land t)$, it is clear that $t$ is relevant and $t'$ is dispensable. w.r.t. $S(\mathbb{P})$. Conversely, let $S(\mathbb{P}^4) = \emptyset$. Then $\mathbb{R} = \emptyset$ and $\mathbb{N} \neq \emptyset$. Hence, $t$ is not relevant, but $t'$ is necessary.
To show hardness w.r.t. $S^{BD}(\mathbb{P})$, it suffices to observe that $t$ is relevant to $\mathbb{P}^{rd}$ iff it is relevant w.r.t. $\models_{BD}$-minimal solutions. Similarly, $t'$ is (not) necessary in $\mathbb{P}^{rd}$ iff it is (not) necessary w.r.t. $\models_{BD}$-minimal solutions. □

Finally, we present the following upper bounds for the recognition of relevant and necessary hypotheses w.r.t. theory-minimal solutions. The proof is an easy consequence of Theorem 6.6. To the best of our knowledge, no analogous problem has been considered for CPL abduction problems.

**THEOREM 6.9.** It is in $\Sigma_3^P$ (resp. $\Pi_3^P$) to decide, given a BD or $BD_\sqsubseteq$ abduction problem $\mathbb{P} = \langle \Gamma, \chi, H \rangle$ and $h \in H$, whether $h$ is relevant (resp. necessary) w.r.t. $S^{Th}(\mathbb{P})$.

## 7 Abduction in the Horn fragments of $BD_\sqsubseteq$

In classical propositional logic, it is known that restricting the language of theories and observations can lower the complexity of abductive reasoning and sometimes even yield tractable cases (cf. (Creignou and Zanuttini 2006) for a detailed discussion). Of particular interest are the Horn fragments of CPL as they have found multiple applications, in particular, in logic programming (Eiter, Gottlob, and Leone 1997). In $BD_\sqsubseteq$, we can similarly use implications to formalise causal connections and conditional statements (cf. Example 7.4, for instance). This motivates us to investigate in this section whether abductive reasoning in Horn fragments of $BD_\sqsubseteq$ is simpler than BD abduction with arbitrary theories.

We begin with the definition of the Horn and definite Horn fragments of classical logic and of $\mathcal{L}_\sqsubseteq$. We present them both in the implicative form.

**Definition 7.1 (Horn and definite Horn fragments of CPL).** The (definite) Horn fragment of CPL is defined using the following grammar:

$$ \text{ant} := p \mid \text{ant} \wedge \text{ant} \qquad (p \in \text{Prop}) $$

$$ C := \text{ant} \supset p \mid \text{ant} \supset \bot $$

$$ \phi := \text{ant} \mid C \mid \phi \wedge \phi $$

A formula $\phi$ produced by this grammar is called a *classical Horn formula*, and it is *definite* if it does not contain $\bot$.

**Definition 7.2 (Horn and definite Horn fragments of $\mathcal{L}_\sqsubseteq$).** The (definite) Horn fragment of $\mathcal{L}_\sqsubseteq$ is defined using the following grammar:

$$ \text{ant} := p \mid \neg p \mid \text{ant} \wedge \text{ant} \qquad (p \in \text{Prop}) $$

$$ C := \text{ant} \supset p \mid \text{ant} \supset \neg p \mid \text{ant} \supset \bot $$

$$ \phi := \text{ant} \mid C \mid \phi \wedge \phi $$

A formula $\phi$ produced by this grammar is called a *BD-Horn formula*, and it is *definite* if it does not contain $\bot$.

Observe that *definite BD-Horn formulas* can contain BD negation $\neg$. It is easy to see, however, that if $\phi$ is a *definite BD-Horn formula*, then $\phi^{cl}$ (recall Definition 4.2) is a classical *definite Horn formula*. Conversely, if $\phi$ is a classical (definite) Horn formula, then it is also a (definite) BD-Horn formula.

Let us now define BD-Horn abduction problems and their solutions. We adapt the definitions from (Creignou and Zanuttini 2006).

**Definition 7.3 (BD-Horn abduction problems).** A (definite) BD-Horn abduction problem is a triple $\mathbb{P} = \langle \Gamma, l, H \rangle$ with $\Gamma$ being a set of (definite) BD-Horn formulas, $l$ being a propositional literal, and $H$ a set of $\mathcal{L}_\Delta$-literals or atomic $\mathcal{L}_\circ$-literals such that $l \notin H$. The notions of *solution* and different kinds of solutions<fnref n="9" /> are as in Definition 3.5.

<footnote n="9">⁹Observe that by this definition all solutions are proper.</footnote>
Recall from Examples 3.10 and 3.11 that in the case of arbitrary theories, there are abduction problems that can be solved only in $BD_\circ$ and problems that can be solved only in $BD_\Delta$. It turns out that this is not the case when the theory is Horn. Indeed while some problems can be solved only in $BD_\circ$ (see next example), every problem with an $\mathcal{L}_\Delta$-solution also admits a solution in the form of a propositional term (and hence a $BD_\circ$-solution).

**Example 7.4.** Assume that if Paula committed the crime, she must have left fingerprints (*f*). The investigators, however, did not find Paula's fingerprints on the crime scene. Thus, Paula's defence wants to justify her innocence. We can formalise this situation as follows: $\mathbb{P} = \langle\{p \supset f, \neg f\}, \neg p\rangle$. Note that $p \supset f, \neg f \models_{CPL} \neg p$. On the other hand, this entailment fails in $BD_\square$. The defence, however, can argue that the search for Paula's fingerprints was conducted thoroughly (so, the information that there are none is reliable) and that Paula must be either guilty or innocent (i.e., there is no third option). Formally, this corresponds to the following explanation — ◦*p* ∧ ◦*f*. One can see that this is a theory-minimal solution for $\mathbb{P}$. Moreover, one can see that there is no $\mathcal{L}_\Delta$-solution of $\mathbb{P}$.

**THEOREM 7.5.** Let $\tau$ be an $\mathcal{L}_\Delta$-solution to a (definite) BD-Horn abduction problem $\mathbb{P} = (\Gamma, l, H)$. Then, $\mathbb{P}$ has a solution that does not contain $\Delta$.

**PROOF.** First note that if we have a solution $\sigma$ which contains only unnegated literals of the form $\Delta l$, it suffices to consider the term $\sigma^b$, which will also be a solution and does not contain $\Delta$. Let us thus consider a solution $\tau \wedge \neg\Delta l'$ of $\mathbb{P}$. It suffices to show that $\tau$ is also a solution of $\mathbb{P}$ (as by repeatedly removing the negated triangle literals, we will obtain a solution without $\Delta$). Assume for a contradiction that $\tau$ is not a solution of $\mathbb{P}$. We have three options: (a) $\Gamma, \tau \models_{BD} \perp$; (b) $\tau \models_{BD} l$; (c) $\Gamma, \tau \not\models_{BD} l$. If (a) or (b) is the case, it is clear that $\tau \wedge \neg\Delta l'$ is not a solution of $\mathbb{P}$ either. Thus, it must be the case that (c) holds: $\Gamma, \tau \not\models_{BD} l$. Moreover, $\Gamma, \tau, \neg\Delta l' \not\models_{BD} \perp$ since otherwise $\tau \wedge \neg\Delta l'$ is not a solution. By Lemma 4.4, we have that $\Gamma^{cl}, \tau^{cl}, (\neg\Delta l')^{cl} \not\models_{CPL} \perp$ and $\Gamma^{cl}, \tau^{cl} \models_{CPL} l^{cl}$. Moreover, one can see that $\Gamma^{cl} \cup \{\tau^{cl}\}$ is a classical Horn theory and $(\neg\Delta l')^{cl} = \sim l'^{cl}$ is a negative literal. As adding a negative literal to a Horn theory never derives a positive literal not contained in the theory, it follows that $\Gamma^{cl}, \tau^{cl}, (\neg\Delta l')^{cl} \not\models_{CPL} l^{cl}$. This contradicts our initial assumption that $\tau \wedge \neg\Delta l'$ is a solution. $\square$

Let us now consider the complexity of solution existence. We begin with the following straightforward statement concerning $\mathcal{L}_\Delta$-solutions.

**THEOREM 7.6.**

(1) It is NP-complete to decide, given a BD-Horn abduction problem $\mathbb{P} = (\Gamma, l, H)$, whether $\mathbb{P}$ has an $\mathcal{L}_\Delta$-solution.

(2) It can be decided in deterministic polynomial time, given a definite BD-Horn abduction problem $\mathbb{P} = (\Gamma, l, H)$, whether $\mathbb{P}$ has an $\mathcal{L}_\Delta$-solution.

**PROOF.** To see that Item 1 holds, we construct two reductions between classical and BD-Horn abduction with a positive observation. First, for membership, given a BD-Horn problem $\mathbb{P} = (\Gamma, l, H)$, we define $\mathbb{P}^{cl} = (\Gamma^{cl}, l^{cl}, H^{cl})$ with $\Gamma^{cl} = \{\phi^{cl} | \phi \in \Gamma\}$ and $H^{cl} = \{h^{cl} | h \in H\}$ (recall the notion of $\phi^{cl}$ from Definition 4.2). By Theorem 4.5, we have that $\tau$ is a solution of $\mathbb{P}$ iff $\tau^{cl}$ is a solution of $\mathbb{P}^{cl}$. As solutions to CPL-Horn abduction problems can be recognised in polynomial time (Eiter and Gottlob 1995, Proposition 5.2), it follows that the existence of $\mathcal{L}_\Delta$-solutions to BD-Horn problems is in NP. For hardness, given a classical Horn problem $\mathbb{P} = (\Gamma, p, H)$, we construct $\mathbb{P}^\Delta = (\Gamma^\Delta, p, H^\Delta)$ with $\Gamma^\Delta = \{\phi^\Delta | \phi \in \Gamma\}$, $H^\Delta = \{h^\Delta | h \in H\}$ (recall Definition 2.4 for the definition of $\phi^\Delta$). From Proposition 2.5, it is immediate that $\tau$ is a solution of $\mathbb{P}$ iff $\tau^\Delta$ is a solution of $\mathbb{P}^\Delta$. It then suffices to recall that solution existence for classical Horn problems is NP-complete (Selman and Levesque 1990, Theorem 2).

Item 2 can be shown similarly by reducing definite BD-Horn abduction to classical definite Horn abduction and recalling the tractability of solution existence for the classical definite Horn fragment when the observation is a positive literal (cf. (Bylander et al. 1991; Friedrich et al. 1990) and (Eiter and Gottlob 1995, Corollary 5.5) for details). Recall again that even though observations in definite BD-Horn problems can have the form $\neg p$ for some $p \in \text{Prop}$, they are still transformed into positive observations because $(\neg p)^{cl} = p^-$. $\square$
On the other hand, even if we restrict the language of background theories to the Horn (or even definite Horn) fragment, determining whether $\mathcal{L}_o$-solutions exist is still intractable. In fact, as one can see from the next statement, we can reduce classical solution existence for any problem to the existence of $\mathcal{L}_o$-solutions of BD-Horn problems.

**THEOREM 7.7.** It is $\Sigma_2^P$-complete to decide, given a BD-Horn abduction problem $\mathbb{P} = (\Gamma, l, \mathbf{H})$, whether $\mathbb{P}$ has a $\mathcal{L}_o$-solution.

**PROOF.** Membership follows immediately from Theorem 6.7. For hardness, we provide a reduction from solution existence for CPL abduction problems with CNF theories, which is known to be $\Sigma_2^P$-complete (Eiter and Gottlob 1995, Theorem 4.2), to solution existence for BD-Horn abduction problems. Let $\mathbb{P} = (\phi, \sigma, \mathbf{H})$ be a classical abduction problem with $\sigma = l$ and $\phi = \bigwedge_{i=1}^m \bigvee_{j=1}^n l_j^i$. Now set $\phi^\perp := \bigwedge_{i=1}^m \left( \bigwedge_{j=1}^n \overline{l_j^i} \supset \perp \right)$ and define $\mathbb{P}^o = (\phi^o, \sigma^o, \mathbf{H}^o)$ as follows (below, $p^{\dagger}$'s and $q$ are fresh variables and $\Xi = \text{Prop}(\phi) \cup \{q\}$).

$$ \begin{array}{l} \phi^o = \phi^\perp \wedge \bigwedge_{p \in \Xi} ((p \wedge \neg p) \supset \perp) \wedge \bigwedge_{p \in \text{Prop}(\phi)} ((p \supset p^\dagger) \wedge (\neg p \supset p^\dagger)) \wedge \left( \left( \left( l \wedge \bigwedge_{p \in \text{Prop}(\phi)} p^\dagger \right) \supset q \right) \supset \perp \right) \\ \sigma^o = q \\ \mathbf{H}^o = \mathbb{H} \cup \{\circ p \mid p \in \Xi\} \end{array} $$

Note that $\phi^o$ is a BD-Horn formula and $q \notin \mathbf{H}^o$. We claim that $\mathbb{P}$ has a solution iff $\mathbb{P}^o$ has a solution.

First let $\tau$ be a solution of $\mathbb{P}$. We show that $\tau^o = \tau \wedge \bigwedge_{p \in \Xi} \circ p$ is a solution of $\mathbb{P}^o$. Indeed, $\phi \wedge \tau$ must be CPL-satisfiable, so there is a classical valuation $v$ such that $v(\phi \wedge \tau) = \mathbf{T}$. By taking the classical valuation $v'$ that extends $v$ by setting $q$ and all the variables $p^\dagger$ to $\mathbf{T}$, we get $v'(\phi^o \wedge \tau^o) = \mathbf{T}$ as well, hence $\phi^o, \tau^o \not\models_{\mathbb{BD}} \perp$. Moreover, from $\phi, \tau \models_{\mathbb{CPL}} l$, we can infer $\phi^\perp, \tau^o \models_{\mathbb{BD}} l$. To see this, assume for contradiction that there is a BD-valuation $v$ witnessing $\phi^\perp, \tau^o \not\models_{\mathbb{BD}} l$. Then $v(\phi^\perp) \in \{\mathbf{T}, \mathbf{B}\}$, $v(\tau^o) \in \{\mathbf{T}, \mathbf{B}\}$, and $v(l) \in \{\mathbf{F}, \mathbf{N}\}$. Observe that $\tau^o = \tau \wedge \bigwedge_{p \in \Xi} \circ p$.

Thus, from $v(\tau^o) \in \{\mathbf{T}, \mathbf{B}\}$, it follows that $v(\circ p) \in \{\mathbf{T}, \mathbf{B}\}$ for every $p \in \text{Prop}[\{\phi, q\}]$. Thus, $v(p) \in \{\mathbf{T}, \mathbf{F}\}$ for every $p \in \text{Prop}[\{\phi, q\}]$. This means that $v$ is a classical valuation, i.e., $v(\phi^\perp) = v(\tau) = \mathbf{T}$ and $v(l) = \mathbf{F}$. As $\phi^\perp$ and $\phi$ are CPL-equivalent, it follows that $\phi, \tau \not\models_{\mathbb{CPL}} l$.

For the converse, let $\tau'$ be a solution of $\mathbb{P}^o$. We show that $\tau^{-o}$ obtained by dropping all literals of the form $\circ p$ from $\tau'$ is a solution of $\mathbb{P}$. In order to show that $\phi, \tau^{-o}$ is CPL-satisfiable, we take a valuation $v$ witnessing $\phi^o, \tau' \not\models_{\mathbb{BD}} \perp$. It follows that $v(\phi^o \wedge \tau') = \mathbf{T}$. Indeed, if $v(\phi^o \wedge \tau') = \mathbf{B}$, then $v(p) = \mathbf{B}$ for some $p \in \Xi$. But this is impossible because $\phi^o$ contains $(p \wedge \neg p) \supset \perp$ and $v((p \wedge \neg p) \supset \perp) = \mathbf{F}$ if $v(p) = \mathbf{B}$. Moreover, there is no $p \in \Xi$ such that $v(p) = \mathbf{N}$. If $\circ p, p, \text{or } \neg p$ occurs in $\tau'$, then $v(\tau') \in \{\mathbf{N}, \mathbf{F}\}$, i.e., $v$ does not witness $\phi^o, \tau' \not\models_{\mathbb{BD}} \perp$. Otherwise, we redefine $v(p^\dagger) = \mathbf{N}$ and $v(q) = \mathbf{N}$. But in this case, $v(\phi^o \wedge \tau') \in \{\mathbf{T}, \mathbf{B}\}$ but $v(q) = \mathbf{N}$, i.e., $v$ witnesses $\phi^o, \tau' \not\models_{\mathbb{BD}} q$, contrary to the assumption that $\tau'$ is a solution to $\mathbb{P}^o$. Now, if $v(\phi^o \wedge \tau') = \mathbf{T}$ and $v(p) \in \{\mathbf{T}, \mathbf{F}\}$ for every $p \in \Xi$, it follows that $v(\phi^o \wedge \tau^{-o}) = \mathbf{T}$ because all literals of $\tau^{-o}$ belong to $\tau'$. Moreover, $v(\phi^\perp) = \mathbf{T}$. Thus, as $\phi^\perp$ and $\phi$ are CPL-equivalent, $v$ is a classical valuation witnessing $\phi, \tau^{-o} \not\models_{\mathbb{CPL}} \perp$.

To see that $\phi, \tau^{-o} \models_{\mathbb{CPL}} l$, assume for contradiction that there is some classical valuation $v$ s.t. $v(\phi \wedge \tau^{-o}) = \mathbf{T}$ and $v(l) = \mathbf{F}$. Now, it is clear that $v(\phi^\perp) = \mathbf{T}$ and $v((p \wedge \neg p) \supset \perp) = \mathbf{T}$ for every $p \in \text{Prop}(\phi)$. We can now set $v(p^\dagger) = \mathbf{T}$ which gives us $v(p \supset p^\dagger) = \mathbf{T}$ and $v(\neg p \supset p^\dagger) = \mathbf{T}$ for all $p \in \text{Prop}(\phi)$. Furthermore, we set $v(q) = \mathbf{F}$ (observe that $q \notin \text{Prop}(\phi \wedge \tau^{-o})$, so it is not assigned a truth value by $v$). This gives us $v\left(\left( l \wedge \bigwedge_{p \in \text{Prop}(\phi)} p^\dagger \right) \supset q \right) = \mathbf{T}$. Thus, $v(\phi^o) = \mathbf{T}$. Moreover, as $v$ is a classical valuation, $v(\circ r) = \mathbf{T}$ for every $r \in \text{Prop}[\{\phi, \tau^{-o}, q\}]$. Thus, $v(\tau') = \mathbf{T}$. But since $\phi^o, \tau' \models_{\mathbb{BD}} q$, it must be that $v(q) \in \{\mathbf{T}, \mathbf{B}\}$. Contradiction. $\square$
The existence of $\mathcal{L}_o$-solutions for BD-Horn problems can in turn be reduced to the existence of $\mathcal{L}_o$-solutions for definite BD-Horn problems.

**THEOREM 7.8.** It is $\Sigma_2^\mathbb{P}$-complete to decide, given a definite BD-Horn abduction problem $\mathbb{P} = (\Gamma, l, \mathbb{H})$, whether $\mathbb{P}$ has an $\mathcal{L}_o$-solution.

**PROOF.** We provide a reduction from BD-Horn problems as in Theorem 7.7. Namely, let $\mathbb{P}^H = (\phi^\circ, q, H^\circ)$ and $r$ be a fresh variable and define $\mathbb{P}^{d^H} = (\phi^{d^H}, q, H^{d^H})$ as follows.

$$ \phi^{d^H} = \bigwedge_{i=1}^{m} \left( \bigwedge_{j=1}^{n} \overline{l_j^i} \supset r \right) \wedge \bigwedge_{p \in \text{Prop}[\{\phi, q\}]} ((p \wedge \neg p) \supset r) \wedge \bigwedge_{p \in \text{Prop}(\phi)} ((p \supset p^\dagger) \wedge (\neg p \supset p^\dagger)) \wedge \left( \left( \neg r \wedge l \wedge \bigwedge_{p \in \text{Prop}(\phi)} p^\dagger \right) \supset q \right) \\ H^{d^H} = H^\circ \cup \{\neg r, \circ r\} $$

We aim to show that $\mathbb{P}^H = (\phi^\circ, q, H^\circ)$ has an $\mathcal{L}_o$-solution iff $\mathbb{P}^{d^H} = (\phi^{d^H}, q, H^{d^H})$ has an $\mathcal{L}_o$-solution.

For the first direction, we let $\tau$ solve $\mathbb{P}^H$ and show that $\tau^{d^H} = \tau \wedge \neg r \wedge \circ r$ solves $\mathbb{P}^{d^H}$. It is clear that $\phi^{d^H} \wedge \tau^{d^H}$ is BD-satisfiable. Indeed, let $v$ be a BD valuation such that $v(\phi^\circ \wedge \tau) \in \{\mathbf{T}, \mathbf{B}\}$. Now if we set $v(r) = \mathbf{F}$, we will have $v(\phi^{d^H} \wedge \tau^{d^H}) \in \{\mathbf{T}, \mathbf{B}\}$. It is also clear that $\phi^{d^H} \wedge \tau^{d^H} \models_{\mathbb{BD}} q$. Indeed, if $v(\phi^{d^H} \wedge \tau^{d^H}) \in \{\mathbf{T}, \mathbf{B}\}$, then $v(r) = \mathbf{F}$, whence, $v(\phi^\circ) \in \{\mathbf{T}, \mathbf{B}\}$. But in this case, $v(q) \in \{\mathbf{T}, \mathbf{B}\}$ since $\phi^\circ \wedge \tau \models_{\mathbb{BD}} q$.

For the converse, let $\tau'$ solve $\mathbb{P}^{d^H}$. We show that $\tau' = \sigma \wedge \neg r \wedge \circ r$ for some $\mathcal{L}_o$-term $\sigma$. Assume for contradiction that $\neg r \notin \tau'$. Now let $v'(\phi^{d^H} \wedge \tau') \in \{\mathbf{T}, \mathbf{B}\}$. We set $v'(r) = \mathbf{T}$, $v(q) = \mathbf{F}$, and $v'(p^\dagger) = \mathbf{T}$ for every $p^\dagger$. As $\neg r \notin \tau$ and $q \notin \text{Prop}(\tau)$, it is clear that $v(\phi^{d^H} \wedge \tau') \in \{\mathbf{T}, \mathbf{B}\}$ but $v(q) = \mathbf{F}$, i.e., $v'$ witnesses $\phi^{d^H}$, $\tau' \not\models_{\mathbb{BD}} q$, contrary to the assumption that $\tau'$ solves $\mathbb{P}$. Thus, $\neg r \in \tau'$. Next, we suppose for a contradiction that $\circ r \notin \tau'$. Then there is a BD-valuation $v'$ such that $v'(r) = \mathbf{B}$ and $v'(\tau') \in \{\mathbf{T}, \mathbf{B}\}$. Observe that $v'(r) = \mathbf{B}$ entails that $v'\left(\bigwedge_{i=1}^{m} \left(\bigwedge_{j=1}^{n} \overline{l_j^i} \supset r\right)\right) \in \{\mathbf{T}, \mathbf{B}\}$ and $v'((p \wedge \neg p) \supset r) \in \{\mathbf{T}, \mathbf{B}\}$ for any valuation of variables in $\text{Prop}(\phi)$. Now we set $v'(l) = \mathbf{F}$, $v'(q) = \mathbf{F}$ (recall that $\text{Prop}[\{q, l\}] \cap \text{Prop}[\mathbb{H}^{d^H}] = \emptyset$, whence $\text{Prop}[\{q, l\}] \cap \text{Prop}(\tau') = \emptyset$), and $v'(p^\dagger) = \mathbf{T}$ for every $p^\dagger$. This gives us $v'(\phi^{d^H} \wedge \tau') \in \{\mathbf{T}, \mathbf{B}\}$ and $v'(q) = \mathbf{F}$, contrary to the assumption that $\tau'$ solves $\mathbb{P}^{d^H}$. It follows that if $\tau'$ is a solution to $\mathbb{P}^{d^H}$, then $\tau' = \sigma \wedge \neg r \wedge \circ r$ for some atomic $\mathcal{L}_o$-term $\sigma$.

Now, we can prove that $\sigma$ is a solution of $\mathbb{P}^H$. Since $\phi^{d^H} \wedge \tau'$ was BD-satisfiable, we have that $\phi^\circ \wedge \sigma$ is also BD-satisfiable. It is also clear that $\phi^\circ \wedge \sigma \models_{\mathbb{BD}} q$. Indeed, assume that $v$ witnesses $\phi^\circ \wedge \sigma \not\models_{\mathbb{BD}} q$. It is clear that if we define $v(r) = \mathbf{F}$, $v$ will witness $\phi^{d^H} \wedge \tau' \not\models_{\mathbb{BD}} q$ contrary to the assumption. The result now follows. $\square$

We end the section with a brief discussion of Theorems 7.6, 7.7 and 7.8. One can see that in contrast to the existence of $\mathcal{L}_\Delta$-solutions, the existence of $\mathcal{L}_o$-solutions for (definite) BD-Horn abduction problems is highly intractable. Essentially, this difference is because BD is in a sense ‘oblivious’ to negated literals, as both $p^{cl}$ and $(\neg p)^{cl}$ map to propositional variables $(p^+$ and $p^-$), and for this reason, clauses such as $(p \wedge \neg q) \supset r$ that are not Horn in CPL still ‘map’ to classical Horn clauses, and so belong to BD-Horn. However, if we allow o-literals, then we can force $\neg$ to behave classically using a term that states that ‘all variables have classical values’, thereby making it possible to simulate arbitrary (non-Horn) CPL theories.

# 8 Discussion and Future Work

We have studied abductive reasoning in the four-valued paraconsistent logic BD and its implicative expansion $BD_\square$, motivating and comparing $\mathcal{L}_\Delta$- and $\mathcal{L}_o$-solutions. By exhibiting reductions of abduction in $BD_\Delta$ and $BD_o$ to abduction in CPL, we have shown that existing procedures for generating abductive solutions in classical logic can be employed for paraconsistent abduction. Our complexity analysis (Table 2) provides an almost complete picture of the complexity of the main decision problems related to abduction. In particular, we established that the complexity of $\mathcal{L}_o$- and $\mathcal{L}_\Delta$-solution existence for BD and $BD_\square$ abduction problems with arbitrary theories is not
higher than in the classical case (Creignou and Zanuttini 2006; Eiter and Gottlob 1995; Pfandler et al. 2015; Pichler and Woltran 2010). On the other hand, while the complexity of $\mathcal{L}_{\Delta}$-solution existence for (definite) BD-Horn abduction problems coincides with that of the classical case, $\mathcal{L}_{\circ}$-solution existence even in the (definite) Horn case is $\Sigma_2^P$-hard.

A few questions remain open. First, we do not know the exact complexity of theory-minimal solution recognition and relevance. One way to approach this would be to establish the complexity of the closely related notion of theory prime implicants in CPL (Marquis 1995). There is also the question of how to embed BD abduction problems with $\mathcal{L}_{\circ}$-solutions into classical problems while preserving $|=_{BD}$-minimal solutions (recall that Theorem 4.9 only preserves theory-minimal solutions). Also, since some BD abduction problems can be solved by arbitrary $\mathcal{L}_{\circ}$-terms but not atomic ones, it would be interesting to explore the computational properties of $\mathcal{L}_{\circ}$-solutions based on non-atomic $\mathcal{L}_{\circ}$-terms.

A more general direction for future work is to consider abduction in other expansions of BD. Of particular interest are *functionally complete* expansions of BD, e.g., the bi-lattice language expansion or an expansion with a ‘quarter-turn’ connective from (Ruet 1996) (cf. (Omori and Sano 2015) for more details). An important technical question would be whether all $\mathcal{L}_{\Delta}$- and $\mathcal{L}_{\circ}$-solutions can be represented as terms in functionally complete languages. A further challenge is to come up with an intuitive natural-language interpretation of literals and terms in such languages.

Additionally, we plan to consider *modal* expansions of BD. Abduction in classical modal logic is well researched. In particular, abduction in classical epistemic and doxastic logics is studied by Levesque (1989) and (Sakama and Inoue 2016); tableaux procedures to solution generation in K, D, T, and S4 are applied by (Mayer and Pirri 1995). Different definitions of prime implicates closely related to abductive solutions are compared by Bienvenu (2009), where the author also provides complexity results and algorithms for prime implicate recognition and generation in multimodal $K_n$; Abduction in dynamic epistemic logic is presented by Nepomuceno-Fernández et al. (2017). Modal expansions of BD are also well known (cf. (Priest 2008) and (Drobyshevich 2020)). There are also public announcement (Rivieccio 2014) and dynamic (Sedlár 2016) BD logics. Thus, it is natural to consider abductive reasoning in *modal paraconsistent* frameworks and see whether classical decision procedures and complexity results can be transferred there.

Another direction is to consider abduction in other non-classical logics, particularly in fuzzy logics. The use of fuzzy logics enables us to formalise reasoning about truth degrees. For example, we may know that if the processor of a computer is overloaded, then the system temperature will increase. We observe that the temperature is 90% above the norm. The solution then would be a degree of the load on the processor that will explain the observation. Fuzzy abduction was first proposed by Yamada and Mukaidono (1995) and then studied in the context of fuzzy logic programming (cf. (Vojtás 1999) and (Chakraborty et al. 2013)). Recently (cf. (Bofill et al. 2019)), new results on the complexity of some fuzzy logics and their fragments were obtained. We plan to utilise these results and study fuzzy abduction in a general setting and consider different types of solutions and different language fragments. Namely, our main goal would be to find fragments of fuzzy logics wherein the complexity of abductive reasoning differs from their classical counterparts, as we have demonstrated in this paper with the recognition of $\mathcal{L}_{\Delta}$-solutions for arbitrary problems and the existence of $\mathcal{L}_{\circ}$-solutions for Horn problems.

## Acknowledgments

The first and third authors were supported by the ANR AI Chair INTENDED (ANR-19-CHIA-0014). The second author has been supported by JSPS KAKENHI Grant Numbers JP21H04905, JP25K03190 and JST CREST Grant Number JPMJCR22D3. The third author was also supported by an NII MOU grant. We would like to thank reviewers for their comments that helped enhance the quality of the paper.
## References

A. Aliseda. 2006. *Abductive Reasoning*. Synthese Library. Vol. 330. Springer. doi:10.1007/1-4020-3907-7.

O. Arieli and A. Avron. 1996. "Reasoning With Logical Bilattices." *Journal of Logic, Language and Information*, 5, 1. doi:10.1007/BF00215626.

O. Arieli and A. Avron. June 1998. "The Value of the Four Values." *Artificial Intelligence*, 102, 1, (June 1998), 97–141. doi:10.1016/S0004-3702(98)00032-0.

N. D. Belnap. 1977a. "A Useful Four-Valued Logic." In: *Modern Uses of Multiple-Valued Logic*. Springer Netherlands, Dordrecht, 5–37.

N. D. Belnap. 1977b. "How a Computer Should Think." In: *Contemporary Aspects of Philosophy*. Oriel Press.

C. Bhagavatula, R. Le Bras, C. Malaviya, K. Sakaguchi, A. Holtzman, H. Rashkin, D. Downey, W.-t. Yih, and Y. Choi. 2020. "Abductive Commonsense Reasoning." In: *8th International Conference on Learning Representations, ICLR 2020*. OpenReview.net.

M. Bienvenu. 2009. "Prime Implicates and Prime Implicants: From Propositional to Modal Logic." *Journal of Artificial Intelligence Research*, 36, 71–128. doi:10.1613/jair.2754.

M. Bienvenu, K. Inoue, and D. Kozhemiachenko. Nov. 2024. "Abductive Reasoning in a Paraconsistent Framework." In: *Proceedings of the Twenty-First International Conference on Principles of Knowledge Representation and Reasoning*. International Joint Conferences on Artificial Intelligence Organization, Hanoi, Vietnam, (Nov. 2024), 134–144. doi:10.24963/kr.2024/13.

M. Bofill, F. Manyà, A. Vidal, and M. Villaret. Apr. 2019. "New Complexity Results for Łukasiewicz Logic." *Soft Computing*, 23, 7, (Apr. 2019), 2187–2197. doi:10.1007/s00500-018-3365-9.

J. Bueno-Soler, W. Carnielli, M. E. Coniglio, and A. Rodrigues Filho. 2017. "Formal (In)consistency, Abduction and Modalities." In: *Springer Handbook of Model-Based Science*. Springer International Publishing, Cham, 315–335. doi:10.1007/978-3-319-30526-4_15.

T. Bylander, D. Allemang, M. C. Tanner, and J. R. Josephson. 1991. "The Computational Complexity of Abduction." *Artificial intelligence*, 49, 1–3, 25–60. doi:10.1016/0004-3702(91)90005-5.

W. Carnielli. Mar. 2006. "Surviving Abduction." *Logic Journal of the IGPL*, 14, 2, (Mar. 2006), 237–256. doi:10.1093/jigpal/jzk016.

A. Chakraborty, A. Konar, N. R. Pal, and L. C. Jain. Aug. 2013. "Extending the Contraposition Property of Propositional Logic for Fuzzy Abduction." *IEEE Transactions in Fuzzy Systems*, 21, 4, (Aug. 2013), 719–734. doi:10.1109/TFUZZ.2012.2230006.

S. Chlebowski, A. Gajda, and M. Urbański. Apr. 2022. "An Abductive Question-Answer System for the minimal logic of formal inconsistency mbC." *Studia Logica*, 110, 2, (Apr. 2022), 479–509. doi:10.1007/s11225-021-09963-0.

N. Creignou and B. Zanuttini. Jan. 2006. "A Complete Classification of the Complexity of Propositional Abduction." *SIAM Journal of Computing*, 36, 1, (Jan. 2006), 207–229. doi:10.1137/S0097539704446311.

W.-Z. Dai, Q. Xu, Y. Yu, and Z.-H. Zhou. 2019. "Bridging machine learning and logical reasoning by abductive learning." *Advances in Neural Information Processing Systems*, 32.

A. del Val. 2000. "The Complexity of Restricted Consequence Finding and Abduction." In: *Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence*. Ed. by H. Kautz and B. Porter. AAAI Press / The MIT Press, 337–342. doi:10.5555/647288.721260.

S. Drobyshevich. Dec. 2020. "A General Framework for FDE-Based Modal Logics." *Studia Logica*, 108, 6, (Dec. 2020), 1281–1306. doi:10.1007/s1225-020-09897-z.

J. Du, K. Wang, and Y.-D. Shen. Feb. 2015. "Towards Tractable and Practical ABox Abduction Over Inconsistent Description Logic Ontologies." *Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence*, 29, 1, (Feb. 2015). doi:10.1609/aaai.v29i1.9393.

J. M. Dunn. 1976. "Intuitive Semantics for First-Degree Entailments and 'Coupled Trees'." *Philosophical Studies*, 29, 3, 149–168.

T. Eiter and G. Gottlob. Jan. 1995. "The Complexity of Logic-Based Abduction." *Journal of the Association for Computing Machinery*, 42, 1, (Jan. 1995), 3–42. doi:10.1145/200836.200838.

T. Eiter, G. Gottlob, and N. Leone. Dec. 1997. "Abduction from logic programs: Semantics and complexity." *Theoretical Computer Science*, 189, 1–2, (Dec. 1997), 129–177. doi:10.1016/S0304-3975(96)00179-X.

B. El Ayeb, P. Marquis, and M. Rusinowitch. 1993. "Preferring diagnoses by abduction." *IEEE Transactions on Systems, Man, and Cybernetics*, 23, 3, 792–808. doi:10.1109/21.256550.

P. A. Flach and A. C. Kakas, (Eds.). Dec. 2000. *Abduction and Induction*. Applied Logic Series. Vol. 18. Springer, Dordrecht, Netherlands, (Dec. 2000). doi:10.1007/978-94-017-0606-3.

J. M. Font. May 1997. "Belnap's Four-Valued Logic and De Morgan Lattices." *Logic Journal of the IGPL*, 5, (May 1997), 1–29. doi:10.1093/jigpal/5.3.1-e.

G. Friedrich, G. Gottlob, and W. Nejdl. 1990. "Hypothesis Classification, Abductive Diagnosis and Therapy." In: *Expert Systems in Engineering Principles and Applications*. Lecture notes in artificial intelligence. Vol. 462. Ed. by G. Gottlob and W. Nejdl. Springer Berlin Heidelberg, Berlin, Heidelberg, 69–78. doi:10.1007/3-540-53104-1_32.

K. Inoue. 2002. "Automated Abduction." In: *Computational Logic: Logic Programming and Beyond*. Lecture Notes in Artificial Intelligence. Vol. 2408. Springer Berlin Heidelberg, Berlin, Heidelberg, 311–341. doi:10.1007/3-540-45632-5_13.

K. Inoue. Aug. 1992. "Linear Resolution for Consequence Finding." *Artificial Intelligence*, 56, 2-3, (Aug. 1992), 301–353. doi:10.1016/0004-3702(92)90030-2.
J. R. Josephson and S. G. Josephson, (Eds.). Oct. 2009. *Abductive inference*. Cambridge University Press, Cambridge, England, (Oct. 2009).

R. Koitz-Hristov and F. Wotawa. Nov. 2018. "Applying algorithm selection to abductive diagnostic reasoning." *Applied Intelligence*, 48, 11, (Nov. 2018), 3976-3994. doi:10.1007/s10489-018-1171-9.

H. J. Levesque. 1989. "A Knowledge-Level Account of Abduction." In: *Proceedings of the Eleventh International Joint Conference on Artificial Intelligence*. Vol. 2, 1061-1067. doi:10.5555/1623891.1623925.

L. Magnani. June 2011. *Abduction, reason and science*. (2001st ed.). Springer, New York, NY, (June 2011). doi:10.1007/978-1-4419-8562-0.

P. Marquis. 2000. "Consequence Finding Algorithms." In: *Algorithms for Uncertainty and Defeasible Reasoning*. Handbook of Defeasible Reasoning and Uncertainty Management Systems. Vol. 5. Springer, 41-145. doi:10.1007/978-94-017-1737-3_3.

P. Marquis. 1995. "Knowledge Compilation Using Theory Prime Implicates." In: *Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI-95)*. Vol. I, 837-845. doi:10.5555/1625855.1625964.

P. Marquis and S. Sadaoui. 1996. "A new algorithm for computing theory prime implicates compilations." In: *Proceedings of the Thirteenth National Conference on Artificial Intelligence — Volume 1 (AAAI'96)*. AAAI Press, Portland, Oregon, 504-509. doi:10.5555/1892875.1892950.

M. C. Mayer and F. Pirri. 1995. "Propositional Abduction in Modal Logic." *Logic Journal of the IGPL*, 3, 6, 907-919. doi:10.1093/jigpal/3.6.907.

A. Nepomuceno-Fernández, F. Soler-Toscano, and F. R. Velázquez-Quesada. 2017. "Abductive Reasoning in Dynamic Epistemic Logic." In: *Springer Handbook of model-based science*. Springer, 269-293. doi:10.1007/978-3-319-30526-4_13.

H. Omori and K. Sano. 2014. "Da Costa Meets Belnap and Nelson." In: *Recent Trends in Philosophical Logic*. Trends in Logic. Vol. 41. Springer International Publishing, Cham, 145-166. doi:10.1007/978-3-319-06080-4_11.

H. Omori and K. Sano. Oct. 2015. "Generalizing Functional Completeness in Belnap-Dunn Logic." *Studia Logica*, 103, 5, (Oct. 2015), 883-917. doi:10.1007/s11225-014-9597-5.

H. Omori and H. Wansing. Dec. 2017. "40 years of FDE: An Introductory Overview." *Studia Logica*, 105, 6, (Dec. 2017), 1021-1049. doi:10.1007/s11225-017-9748-6.

H. Omori and T. Waragai. 2011. "Some Observations on the Systems LFI1 and LFI1*." In: *22nd International Workshop on Database and Expert Systems Applications*, 320-324. doi:10.1109/DEXA.2011.77.

G. Paul. Apr. 1993. "Approaches to abductive reasoning: an overview." *Artificial Intelligence Review*, 7, 2, (Apr. 1993), 109-152. doi:10.1007/bf00849080.

A. Pfandler, R. Pichler, and S. Woltran. June 2015. "The Complexity of Handling Minimal Solutions in Logic-Based Abduction." *Journal of Logic and Computation*, 25, 3, (June 2015), 805-825. doi:10.1093/logcom/exu053.

R. Pichler and S. Woltran. 2010. "The Complexity of Handling Minimal Solutions in Logic-Based Abduction." In: *Proceedings of 19th European Conference on Artificial Intelligence (ECAI-2010)*. Frontiers in Artificial Intelligence and Applications. Vol. 215. IOS Press, 895-900. doi:10.3233/978-1-60750-606-5-895.

D. Poole. Feb. 1989. "Explanation and Prediction: An Architecture for Default and Abductive Reasoning." *Computational Intelligence*, 5, 2, (Feb. 1989), 97-110. doi:10.1111/j.1467-8640.1989.tb00319.x.

G. Priest. 2008. "Many-Valued Modal Logics: A Simple Approach." *The Review of Symbolic Logic*, 1, 2, 190-203. doi:10.1017/S1755020308080179.

U. Rivieccio. 2014. "Bilattice Public Announcement Logic." In: *Advances in Modal Logic (AiML-2014)*. Vol. 10. College Publications, 459-477.

A. Rodrigues, M. E. Coniglio, H. Antunes, J. Bueno-Soler, and W. Carnielli. 2023. "Paraconsistency, Evidence, and Abduction." In: *Handbook of Abductive Cognition*. Springer International Publishing, Cham, 313-350. doi:10.1007/978-3-030-68436-5_27-1.

P. Ruet. 1996. "Complete sets of connectives and complete sequent calculus for Belnap's Logic." In: *Logic Colloquium 96*. Ecole Normale Supérieure (Paris). Laboratoire d'Informatique.

C. Sakama and K. Inoue. Aug. 2016. "Abduction, Conversational Implicature and Misleading in Human Dialogues." *Logic Journal of the IGPL*, 24, 4, (Aug. 2016), 526-541. doi:10.1093/jigpal/jzw027.

C. Sakama and K. Inoue. June 1995. "The Effect of Partial Deduction in Abductive Reasoning." In: *Logic Programming: The 12th International Conference*. The MIT Press, (June 1995). ISBN: 9780262291439. doi:10.7551/mitpress/4298.003.0042.

K. Sano and H. Omori. 2014. "An Expansion of First-Order Belnap-Dunn logic." *Logic Journal of IGPL*, 22, 3, 458-481. doi:10.1093/jigpal/jzt044.

I. Sedlár. 2016. "Propositional Dynamic Logic With Belnapian Truth Values." In: *Advances in Modal Logic (AiML-2016)*. Vol. 11. College Publications, 503-519.

B. Selman and H. J. Levesque. 1990. "Abductive and Default Reasoning: A Computational Core." In: *Proceedings AAAI-90*, 343-348. doi:10.5555/1865499.1865552.

M. E. Stickel. 1990. "Rationale and Methods for Abductive Reasoning in Natural-Language Interpretation." In: *Natural Language and Logic* (Lecture Notes in Artificial Intelligence). Vol. 459. Springer, 233-252. doi:10.1007/3-540-53082-7_26.

A. del Val. 1999. "A New Method for Consequence Finding and Compilation in Restricted Languages." In: *AAAI-99 Proceedings*, 259-264. doi:10.5555/315149.315300.

P. Vojtás. 1999. "Fuzzy Logic Abduction." In: *Proceedings of the EUSFLAT-ESTYLF Joint Conference*. Ed. by G. Mayor and J. Suñer. Universitat de les Illes Balears, Palma de Mallorca, Spain, 319-322.

K. Yamada and M. Mukaidono. 1995. "Fuzzy Abduction Based on Łukasiewicz Infinite-Valued Logic and Its Approximate Solutions." In: *Proceedings of 1995 IEEE International Conference on Fuzzy Systems*. Vol. 1. IEEE, 343-350. doi:10.1109/FUZZY.1995.409702.