Revisiting Explicit Negation in Answer Set Programming

TL;DR

This paper explores the integration of explicit negation with nested expressions in Answer Set Programming, extending existing logical frameworks and analyzing their properties and relationships.

Contribution

It introduces an extension of Equilibrium Logic to incorporate explicit negation with nested expressions, providing a formal foundation and comparative analysis.

Findings

Extended the concept of reduct for combined explicit negation and nested expressions.

Proved that the extended syntax can be captured by an extension of Equilibrium Logic.

Compared the new approach with existing logic systems involving strong negation.

Abstract

A common feature in Answer Set Programming is the use of a second negation, stronger than default negation and sometimes called explicit, strong or classical negation. This explicit negation is normally used in front of atoms, rather than allowing its use as a regular operator. In this paper we consider the arbitrary combination of explicit negation with nested expressions, as those defined by Lifschitz, Tang and Turner. We extend the concept of reduct for this new syntax and then prove that it can be captured by an extension of Equilibrium Logic with this second negation. We study some properties of this variant and compare to the already known combination of Equilibrium Logic with Nelson's strong negation. Under consideration for acceptance in TPLP.

Equations

$$\sim {train}_1$$

$$\sim {train}_2$$

$$\sim {train}_3$$

$$\sim {train}_1\vee \sim {train}_2\vee \sim {train}_3$$

$$\sim ({train}_1\wedge {train}_2\wedge {train}_3)$$

$$\sim \neg p\to p$$

$$F::=\top \mid \perp \mid p\mid F\vee F\mid F\wedge F\mid \neg F\mid \sim F$$

$$\begin{array}[]{r@{\,}c@{\,}ll@{\hspace{40pt}}r@{\,}c@{\,}ll}T&\models&\top&\hfil\hskip 40.&T&\not=\!\!\!\!|&\top\\ T&\not\models&\bot&\hfil\hskip 40.&T&=\!\!\!\!|&\bot\\ T&\models&p&\mbox{if }p\in T\hfil\hskip 40.&T&=\!\!\!\!|&p&\mbox{if }\sim\!\!p\in T\\ T&\models&\varphi\wedge\psi&\mbox{if }T\models\varphi\mbox{ and }T\models\psi\hfil\hskip 40.&T&=\!\!\!\!|&\varphi\wedge\psi&\mbox{if }T=\!\!\!\!|\;\varphi\mbox{ or }T=\!\!\!\!|\;\psi\\ T&\models&\varphi\vee\psi&\mbox{if }T\models\varphi\mbox{ or }T\models\psi\hfil\hskip 40.&T&=\!\!\!\!|&\varphi\vee\psi&\mbox{if }T=\!\!\!\!|\;\varphi\mbox{ and }T=\!\!\!\!|\;\psi\\ T&\models&\sim\!\!\varphi&\mbox{if }T=\!\!\!\!|\;\varphi\hfil\hskip 40.&T&=\!\!\!\!|&\sim\!\!\varphi&\mbox{if }T\models\varphi\\ T&\models&\neg\varphi&\mbox{if }T\not\models\varphi\hfil\hskip 40.&T&=\!\!\!\!|&\neg\varphi&\mbox{if }T\models\varphi\end{array}$$

$$\begin{array}[]{rcll}p^{T}&\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}&p&\mbox{for any atom }p\in\mathit{At}\\ (F\wedge G)^{T}&\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}&F^{T}\wedge G^{T}\\ (F\vee G)^{T}&\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}&F^{T}\vee G^{T}\\ (\sim\!\!F)^{T}&\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}&\sim\!\!(F^{T})\\ (\neg F)^{T}&\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}&\left\{\begin{array}[]{rl}\bot&\mbox{if }T\models F\\ \top&\mbox{otherwise}\end{array}\right.\\ \end{array}$$

$$\neg (bird\wedge \sim flies)\to \sim (bird\wedge \sim flies)$$

$$\phi ::=p\mid \perp \mid \phi \wedge \phi \mid \phi \vee \phi \mid \phi \to \phi \mid \sim \phi$$

$$\neg \phi$$

$$\top$$

$$\phi \leftrightarrow \psi$$

$$\phi \iff \psi$$

$$\begin{array}[]{r@{\,}c@{\,}l@{\;}l@{\hspace{10pt}}r@{\,}c@{\,}l@{\;}l}\langle H,T\rangle&\models&\top&\hfil\hskip 10.&\langle H,T\rangle&\not=\!\!\!\!|&\top\\ \langle H,T\rangle&\not\models&\bot&\hfil\hskip 10.&\langle H,T\rangle&=\!\!\!\!|&\bot\\ \langle H,T\rangle&\models&p&\mbox{if }p\in H\hfil\hskip 10.&\langle H,T\rangle&=\!\!\!\!|&p&\mbox{if }\sim\!\!p\in H\\ \langle H,T\rangle&\models&\varphi\wedge\psi&\mbox{if }\langle H,T\rangle\models\varphi\mbox{ and }\langle H,T\rangle\models\psi\hfil\hskip 10.&\langle H,T\rangle&=\!\!\!\!|&\varphi\wedge\psi&\mbox{if }\langle H,T\rangle=\!\!\!\!|\;\varphi\mbox{ or }\langle H,T\rangle=\!\!\!\!|\;\psi\\ \langle H,T\rangle&\models&\varphi\vee\psi&\mbox{if }\langle H,T\rangle\models\varphi\mbox{ or }\langle H,T\rangle\models\psi\hfil\hskip 10.&\langle H,T\rangle&=\!\!\!\!|&\varphi\vee\psi&\mbox{if }\langle H,T\rangle=\!\!\!\!|\;\varphi\mbox{ and }\langle H,T\rangle=\!\!\!\!|\;\psi\\ \langle H,T\rangle&\models&\sim\!\!\varphi&\mbox{if }\langle H,T\rangle=\!\!\!\!|\;\varphi\hfil\hskip 10.&\langle H,T\rangle&=\!\!\!\!|&\sim\!\!\varphi&\mbox{if }\langle H,T\rangle\models\varphi\\ \langle H,T\rangle&\models&\varphi\!\to\!\psi&\mbox{if both}\hfil\hskip 10.&\langle H,T\rangle&=\!\!\!\!|&\varphi\!\to\!\psi&\mbox{if }\langle T,T\rangle\models\varphi\mbox{ and }\langle H,T\rangle=\!\!\!\!|\;\psi\\ &&&(i)\langle H,T\rangle\not\models\varphi\mbox{ or }\langle H,T\rangle\models\psi\hfil\hskip 10.\\ &&&(ii)\langle T,T\rangle\not\models\varphi\mbox{ or }\langle T,T\rangle\models\psi\hfil\hskip 10.&&&&\hfill\Box\end{array}$$

$$\begin{array}[]{cc}\varphi^{T}_{+}\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}\left\{\begin{array}[]{cl}\bot&\text{if }T\not\models\varphi\\ p&\text{if }\varphi=p\in\mathit{At},p\in T\\ \alpha^{T}_{+}\otimes\beta^{T}_{+}&\text{if }T\models\varphi,\varphi=\alpha\otimes\beta,\\ &\text{ for }\otimes\in\{\vee,\wedge\}\\ \neg(\alpha^{T}_{+})\vee\beta^{T}_{+}&\text{if }T\models\varphi,\varphi=\alpha\to\beta\\ \neg(\alpha^{T}_{+})&\text{if }T\models\varphi,\varphi=\neg\alpha,\\ \sim\!\!(\alpha^{T}_{-})&\text{if }T\models\varphi,\varphi=\sim\!\!\alpha\end{array}\right.&\varphi^{T}_{-}\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}\left\{\begin{array}[]{cl}\top&\text{if }T\not=\!\!\!\!|\;\varphi\\ p&\text{if }\varphi=p\in\mathit{At},\sim\!\!p\in T\\ \alpha^{T}_{-}\otimes\beta^{T}_{-}&\text{if }T=\!\!\!\!|\;\varphi,\varphi=\alpha\otimes\beta,\\ &\text{ for }\otimes\in\{\vee,\wedge\}\\ \beta^{T}_{-}&\text{if }T=\!\!\!\!|\;\varphi,\varphi=\alpha\to\beta\\ \bot&\text{if }T=\!\!\!\!|\;\varphi,\varphi=\neg\alpha\\ \sim\!\!(\alpha^{T}_{+})&\text{if }T=\!\!\!\!|\;\varphi,\varphi=\sim\!\!\alpha\end{array}\right.\end{array}$$

$$M(p)\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}\left\{\begin{array}[]{rl}2&\mbox{if }p\in H\\ -2&\mbox{if }\sim\!\!p\in H\\ 1&\mbox{if }p\in T\setminus H\\ -1&\mbox{if }\sim\!\!p\in T\setminus H\\ 0&\mbox{otherwise, i.e., }p\not\in T,\sim\!\!p\not\in T\end{array}\right.$$

$$\begin{array}[]{c@{\hspace{5pt}}c}\begin{array}[]{r|rrrrr}\wedge&-2&-1&0&1&2\\ \hline\cr-2&-2&-2&-2&-2&-2\\ -1&-2&-1&-1&-1&-1\\ 0&-2&-1&0&0&0\\ 1&-2&-1&0&1&1\\ 2&-2&-1&0&1&2\end{array}\hfil\hskip 5.0&\begin{array}[]{r|rrrrr}\vee&-2&-1&0&1&2\\ \hline\cr-2&-2&-1&0&1&2\\ -1&-1&-1&0&1&2\\ 0&0&0&0&1&2\\ 1&1&1&1&1&2\\ 2&2&2&2&2&2\end{array}\\ \hfil\hskip 5.0\\ \begin{array}[]{r|rrrrr}\to&-2&-1&0&1&2\\ \hline\cr-2&2&2&2&2&2\\ -1&2&2&2&2&2\\ 0&2&2&2&2&2\\ 1&-2&-1&0&2&2\\ 2&-2&-1&0&1&2\end{array}\hfil\hskip 5.0&\begin{array}[]{c@{\hspace{20pt}}c}\begin{array}[]{r|r}\varphi&\sim\!\!\varphi\\ \hline\cr-2&2\\ -1&1\\ 0&0\\ 1&-1\\ 2&-2\end{array}\hfil\hskip 20.&\begin{array}[]{r|r}\varphi&\neg\varphi\\ \hline\cr-2&2\\ -1&2\\ 0&2\\ 1&-2\\ 2&-2\end{array}\end{array}\\ \hfil\hskip 5.0\\ \begin{array}[]{r|rrrrr}\leftrightarrow&-2&-1&0&1&2\\ \hline\cr-2&2&2&2&-2&-2\\ -1&2&2&2&-1&-1\\ 0&2&2&2&0&0\\ 1&-2&-1&0&2&1\\ 2&-2&-1&0&1&2\end{array}\hfil\hskip 5.0&\begin{array}[]{r|rrrrr}\Leftrightarrow&-2&-1&0&1&2\\ \hline\cr-2&2&1&0&-2&-2\\ -1&1&2&0&-1&-2\\ 0&0&0&2&0&0\\ 1&-2&-1&0&2&1\\ 2&-2&-2&0&1&2\end{array}\end{array}$$

$$\sim \phi \to \neg \phi$$

$$\sim ((\phi \to \sim \phi )\to \sim (\phi \to \sim \phi ))$$

$$\sim (p\wedge \neg p)$$

$$\sim \top$$

$$\sim \perp$$

$$\sim (\phi \wedge \psi )$$

$$\sim (\phi \vee \psi )$$

$$\sim \sim \phi$$

$$\sim \neg \phi$$

$$\begin{array}[]{rcll}\sim\!\!(p\wedge\neg p)&\Leftrightarrow&\sim\!\!p\vee\sim\!\!\neg p&\mbox{ by }\eqref{f:nnf3}\\ &\Leftrightarrow&\sim\!\!p\vee\neg\neg p&\mbox{ by }\eqref{f:nnf6}\end{array}$$

$$\phi \wedge (\psi \vee \gamma )\iff (\phi \wedge \psi )\vee (\phi \wedge \gamma )$$

$$\phi \wedge \perp \iff \perp$$

$$\phi \wedge \top \iff \phi$$

$$\neg (\phi \wedge \psi )\iff \neg \phi \vee \neg \psi$$

$$\neg \top \iff \perp$$

$$\neg \neg \neg \phi$$

$$\phi \to \psi \wedge \gamma$$

$$\phi \vee \psi \to \gamma$$

$$\phi \wedge \neg \neg \psi \to \gamma$$

Full text

1 Introduction

Although the introduction of stable models [Gelfond and Lifschitz (1988)] in logic programming was motivated by the search of a suitable semantics for default negation, their early application to knowledge representation revealed the need of a second negation to represent explicit falsity. This second negation was already proposed in [Gelfond and Lifschitz (1991)] under the name of classical negation, an operator only applicable on atoms that, when present in the syntax, led to a change in the name of stable models to become answer sets. Classical negation soon became common in applications for commonsense reasoning and action theories [Gelfond and Lifschitz (1993)] and was also extrapolated to the Well-Founded Semantics [Pereira and Alferes (1992)] under the name of explicit negation. Later on, it was incorporated to the paradigm of Answer Set Programming [Niemelä (1999), Marek and Truszczyński (1999)] (ASP), being nowadays present in the input language of most ASP solvers.

To understand the difference for knowledge representation between default negation (in this paper, written as $\neg$) and explicit negation (represented as $\sim\!\!$ ), a typical example is to distinguish the rule $\neg\mathit{train}\to\mathit{cross}$, that captures the criterion “you can cross if you have no information on a train coming,” from the (safier) encoding $\sim\!\!\mathit{train}\to\mathit{cross}$ that means “you can cross if you have evidence that no train is coming.” In ASP, this explicit negation can only be used in front of atoms111In fact, the construct “$\sim\!\!\mathit{train}$” is normally treated in ASP as a new atom $\mathit{train}^{\prime}$ and an implicit constraint $\mathit{train}\wedge\mathit{train}^{\prime}\to\bot$ is used to guarantee that both atoms cannot be true simultaneously. so it is not seen as a real connective. In an attempt of providing more flexibility to logic program connectives, \citeNLTT99 introduced programs with nested expressions where conjunction, disjunction and default negation could be arbitrarily nested both in the heads and bodies of rules, but classical negation was still restricted to an application on atoms. To see an example, suppose that a given moment, three trains should be crossing, and we have an alarm that fires if one of them is known to be missing. Using nested expressions, we can rewrite the program:

[TABLE]

as a single rule with a disjunction in the body:

[TABLE]

but we cannot further apply De Morgan to rewrite the rule above as:

[TABLE]

It is easy to imagine that providing a semantics for this kind of expressions would be interesting if we plan to jump from the propositional case to programs with variables and aggregates (where, for instance, the number of trains is some arbitrary value $n\geq 0$).

An important breakthrough that meant a purely logical treatment, was the characterisation of stable models in terms of Equilibrium Logic proposed by \citeNPearce96. This non-monotonic formalism is defined in terms of a models selection criterion on top of the (monotonic) intermediate logic of Here-and-There (HT) [Heyting (1930)] and captures default negation $\neg\varphi$ as a derived operator in terms of implication $\varphi\to\bot$, as usual in intuitionistic logic. The definition of Equilibrium Logic also included a second, constructive negation ‘$\sim\!\!$’ corresponding to Nelson’s strong negation [Nelson (1949)] for intermediate logics. In the case of HT, this extension yields a five-valued logic called ${\cal N}_{5}$ where, although ‘$\sim\!\!$’ can now be nested as the rest of connectives, there exists a reduction for shifting it in front of atoms, obtaining a negative normal form (NNF). Once in NNF, the obtained equilibrium models actually coincide with answer sets for the syntactic fragments of nested expressions [Lifschitz et al. (1999)] or for regular programs [Gelfond and Lifschitz (1993)]. For this reason, most papers on Equilibrium Logic for ASP assumed a reduction to NNF from the very beginning, and little attention was paid to the behaviour of formulas in the scope of strong negation under a logic programming perspective. There are, however, cases in which this behaviour is not aligned with the reduct-based understanding of nested expressions in ASP. Take, for instance, the formula:

[TABLE]

Its NNF reduction removes the combination of negations $\sim\!\!\neg$ and produces the tautological rule $p\to p$ whose unique equilibrium model is $\emptyset$, i.e., neither $p$ nor $\sim\!\!p$ hold. However, if we start instead from the formula $\sim\!\!\neg\neg\neg p\to p$, the NNF reduction removes again the first pair of negations producing the rule $\neg\neg p\to p$ with a second answer set $\{p\}$. This illustrates that we cannot replace $\neg p$ by $\neg\neg\neg p$ in the scope of strong negation, even though they would produce the same effect in any reduct of the style of [Lifschitz et al. (1999)] for nested expressions.

In this paper, we consider a different characterisation of ‘$\sim\!\!$’  in HT and Equilibrium Logic. We call this variant explicit negation to differentiate it from Nelson’s strong negation. To test its adequacy, we start generalising the definition of nested expression by introducing an arbitrary nesting of ‘$\sim\!\!$’, adapting the definitions of reduct and answer set from [Lifschitz et al. (1999)] to that context. After that, we prove that equilibrium models (with explicit negation) capture the answer sets for these extended nested expressions and, in fact, preserve the strong equivalences from [Lifschitz et al. (1999)] even for arbitrary formulas (including implication). We also prove several properties of HT with explicit negation and provide a reduction to NNF that produces a different effect from ${\cal N}_{5}$ when applied on implications or default negation.

The rest of the paper is organised as follows. In the next section, we introduce the extended definition of answer sets for programs with nested expressions, where explicit negation can be arbitrarily combined both in the rule bodies and the rule heads. In Section 3, we present Equilibrium Logic with explicit negation and in particular, its new monotonic basis, ${\cal X}_{5}$, since the selection of equilibrium models is the same one as in [Pearce (1997)]. Section 4 provides a five-valued characterisation of ${\cal X}_{5}$ and studies different types of equivalence relations, including variants of strong equivalence. In Section 5, we briefly explain the main differences between explicit (${\cal X}_{5}$) and strong (${\cal N}_{5}$) negations. Finally, Section 6 concludes the paper.

2 Nested expressions with explicit negation

We begin describing the syntax of nested expressions, starting from a set of atoms $\mathit{At}$. A nested expression $F$ is defined with the following grammar:

[TABLE]

where $p$ is any atom $p\in\mathit{At}$. The two negations $\neg$ and $\sim\!\!$  are respectively called default and explicit negation (the latter is also called classical in the ASP literature). An explicit literal is either an atom $p$ or its explicit negation $\sim\!\!p$. A default literal is either an explicit literal $A$ or its default negation $\neg A$. Thus, given atom $p$, we can form the default literals $p,\sim\!\!p,\neg p$ and $\neg\!\!\sim\!\!p$. As we can see, the main difference with respect to [Lifschitz et al. (1999)] is that, in that case, the explicit negation222To be precise, [Lifschitz et al. (1999)] used a different notation and names for operators: $\wedge$, $\vee$ and $\neg$ were respectively denoted as comma, semicolon and ‘not’ in [Lifschitz et al. (1999)], whereas explicit negation $\sim\!\!$ was denoted as $\neg$ and called classical negation. operator $\sim\!\!$  was only used for explicit literals, whereas in this definition, it can be arbitrarily nested. For instance, $\sim\!\!(p\vee\neg q)$ is a nested expression under this new definition, but it is not under [Lifschitz et al. (1999)]. A rule is an implication of the form $F\to G$ where $F$ and $G$ are nested expressions respectively called the *body * and the head of the rule. A rule of the form $\top\to G$ is sometimes abbreviated as $G$ and is further called a fact if $G$ is an explicit literal. A logic program is a set of rules. We say that a nested expression, a rule or a program is explicit if it does not contain default negation.

A program rule $F\to G$ is said to be regular if the body $F=B_{1}\wedge\dots\wedge B_{n}$ is a conjunction of default literals and the head $G=H_{1}\vee\dots\vee H_{m}$ is a disjunction of default literals. In a regular rule, we allow an empty body $n=0$ and write $F=\top$ or an empty head $m=0$ and $G=\bot$ but not both. A program is regular if all its rules are regular.

An interpretation is a set of explicit literals that is consistent, that is, it does not contain both $p$ and $\sim\!\!p$ for any atom $p$. We define when an interpretation $T$ satisfies (resp. falsifies) a nested expression $F$, written $T\models F$ (resp. $T=\!\!\!\!|\;F$) providing the following recursive conditions:

[TABLE]

As an example, given $\mathit{At}=\{p,q\}$ and $T=\{\sim\!\!p\}$ we have $T\models\sim\!\!p\vee q$ because $T\models\,\sim\!\!p$ (i.e. $T=\!\!\!\!|\;p$) although neither $T\models q$ nor $T=\!\!\!\!|\;q$, that is, $q$ is undefined. The latter can be expressed as $T\models\neg q\wedge\neg\!\sim\!\!q$ (i.e., $q$ is neither true nor false). As another example, $T=\!\!\!\!|\;p\wedge q$ because $T=\!\!\!\!|\;p$ even though, as we said, $q$ is undefined. We say that $\varphi$ is valid if we have $T\models\varphi$ for every interpretation $T$. The logic induced by these valid expressions precisely corresponds to classical logic with strong negation as studied by \citeNvakarelov1977notes. Note that, as usual in classical logic, $\varphi\to\psi$ is definable as $\neg\varphi\vee\psi$ in this context.

Let $\Pi$ be an explicit program. A consistent set of literals $T$ is a model of $\Pi$ if, for every rule $F\to G$ in $\Pi$, $T\models G$ whenever $T\models F$.

Definition 1** (reduct)**

The reduct of a nested expression $F$ with respect to an interpretation $T$ is denoted as $F^{T}$ and defined recursively as follows:

[TABLE]

*The reduct of a program $\Pi$ with respect to $T$ corresponds to the explicit program:

$\Pi^{T}\mathbin{\stackrel{{\scriptstyle\mathrm{def}}}{{=}}}\{\ (F^{T}\to G^{T})\mid(F\to G)\in\Pi\ \}$. $\Box$*

Proposition 1

For any consistent set of literals $T$ and any nested formula $F$:

• •

$T\models F$* iff $T\models F^{T}$;*

• •

$T=\!\!\!\!|\;F$* iff $T=\!\!\!\!|\;F^{T}$. *$\Box$

Definition 2** (answer set)**

A consistent set of literals $T$ is an answer set of a program $\Pi$ if it is a $\subseteq$-minimal model of the reduct $\Pi^{T}$. $\Box$

Notice that the definitions of reduct and answer set for the case of regular programs directly coincide with the standard definitions in ASP without nested expressions [Gelfond and Lifschitz (1991)]. They also coincide with [Lifschitz et al. (1999)], defined on the case of programs with nested expressions where ‘$\sim\!\!$’  is only in front of atoms.

Example 1

Take the program consisting of the single rule (1). For $\mathit{At}=\{p\}$, we have three possible interpretations $T_{1}=\{p\}$, $T_{2}=\{\sim\!\!p\}$ and $T_{3}=\emptyset$. This yields two possible reducts $\Pi^{T_{1}}=\{\sim\!\!\bot\to p\}$ and $\Pi^{T_{2}}=\Pi^{T_{3}}=\{\sim\!\!\top\to p\}$. It is easy to see that their corresponding minimal models are $T_{1}$ and $T_{3}$ which constitute the two answer sets of $\Pi$. $\Box$

Example 2

Take the program consisting of the single rule:

[TABLE]

capturing the idea that “being a bird that does not fly” should be false by default. If we choose any interpretation $T$ such that $T\models\mathit{bird}\wedge\sim\!\!\mathit{flies}$ then the reduct will have a single rule with $\bot$ in the body and the minimal model will be $\emptyset$ which does not satisfy $\mathit{bird}\wedge\sim\!\!\mathit{flies}$. If $T\not\models\mathit{bird}\wedge\sim\!\!\mathit{flies}$ instead, the reduct becomes $\top\to\ \sim\!\!(\mathit{bird}\wedge\sim\!\!\mathit{flies})$ and the minimal models of this program are $\{\sim\!\!\mathit{bird}\}$ and $\{\mathit{flies}\}$ that, as they are both compatible with the assumption for $T$, they become the two answer sets of (2).

Suppose we extend now (2) with the fact $bird$. Doing so, it is easy to see that the only answer set becomes $\{\mathit{flies}\}$. Analogously, if we take (2) plus the fact $\sim\!\!\mathit{flies}$ the only answer set becomes $\{\sim\!\!\mathit{bird}\}$. Finally, if we add the facts $\mathit{bird}$ and $\sim\!\!\mathit{flies}$ to (2), the default is deactivated and we get the unique answer set $\{\mathit{bird},\sim\!\!\mathit{flies}\}$. $\Box$

3 Equilibrium logic with explicit negation

We start defining the monotonic logic of Here-and-There with explicit negation, ${\cal X}_{5}$. Let $\mathit{At}$ be a set of atoms. A formula $\varphi$ is an expression built with the grammar:

[TABLE]

for any atom $p\in\mathit{At}$. We also use the abbreviations:

[TABLE]

[TABLE]

Given a pair of formulas $\varphi$ and $\alpha$, we write $\varphi[\alpha/p]$ to denote the uniform substitution of all occurrences of atom $p$ in $\varphi$ by $\alpha$. As usual, a theory is a set of formulas. We sometimes understand finite theories (or subtheories) as the conjunction of their formulas. Notice that programs with nested expressions are also theories under this definition.

An ${\cal X}_{5}$-interpretation is a pair $\langle H,T\rangle$ of consistent sets of explicit literals (respectively standing for “here” and “there”) satisfying $H\subseteq T$. We say that the interpretation is total when $H=T$.

Definition 3** (${\cal X}_{5}$ Satisfaction/falsification)**

We say that $\langle H,T\rangle$ satisfies (resp. falsifies) a formula $\varphi$, written $\langle H,T\rangle\models\varphi$ (resp. $\langle H,T\rangle=\!\!\!\!|\;\varphi$), when the following recursive conditions hold:

[TABLE]

A formula $\varphi$ is a tautology (or is valid), written $\models\varphi$, if it is satisfied by every possible interpretation. We say that an ${\cal X}_{5}$-interpretation $\langle H,T\rangle$ is a model of a theory $\Gamma$, written $\langle H,T\rangle\models\Gamma$, if $\langle H,T\rangle\models\varphi$ for all $\varphi\in\Gamma$. The next observation about Definition 3 connects satisfaction ‘$\models$’ with standard HT.

Observation 1

The satisfaction relation ‘$\models$’ (left column in Def. 3) of any formula corresponds to regular HT satisfaction up to the first occurrence of ‘$\sim$’, where the falsification ‘$=\!\!\!\!|\;$’ comes into play. $\Box$

As a result, any tautology from HT can be shifted to ${\cal X}_{5}$, even if its atoms are uniformly replaced by subformulas containing explicit negation.

Theorem 1

If formula $\varphi$ is HT valid (and so, it does not contain $\sim\!\!$ ) then $\varphi[\alpha/p]$ is also ${\cal X}_{5}$ valid, for any formula $\alpha$ and any atom $p$. $\Box$

If we choose any $p$ not occurring in $\varphi$, then $\varphi[\alpha/p]=\varphi$ and the theorem above is just saying that ${\cal X}_{5}$ is a conservative extension of HT. But it can also be exploited further by replacing, in the HT tautology, any atom by an arbitrary formula containing negation. For instance, if explicit negation only occurs in front of atoms, we essentially get HT with explicit literals playing the role of atoms (disregarding inconsistent models). However, when we combine explicit negation in an arbitrary way, some usual properties of HT need to be checked in the new context.

Lemma 1

Let $T$ be a consistent set of literals and $F$ a nested expression. Then:

• •

$\langle T,T\rangle\models F$* iff $T\models F$;*

• •

$\langle T,T\rangle=\!\!\!\!|\;F$* iff $T=\!\!\!\!|\;F$. *$\Box$

Theorem 2** (Persistence)**

For any ${\cal X}_{5}$-interpretation $\langle H,T\rangle$ and any formula $\varphi$ then both:

• (i)

$\langle H,T\rangle\models\varphi$* implies $\langle T,T\rangle\models\varphi$;*

• (ii)

$\langle H,T\rangle=\!\!\!\!|\;\varphi$* implies $\langle T,T\rangle=\!\!\!\!|\;\varphi$. *$\Box$

Proposition 2

For any ${\cal X}_{5}$-interpretation $\langle H,T\rangle$, any formula $\varphi$:

• •

$\langle H,T\rangle\models\neg\varphi$* iff $\langle T,T\rangle\not\models\varphi$;*

• •

$\langle H,T\rangle=\!\!\!\!|\;\neg\varphi$* iff $\langle T,T\rangle\models\varphi$. *$\Box$

The following results establish a connection between ${\cal X}_{5}$ and the reduct of a nested expression or a program.

Lemma 2

Let $\langle H,T\rangle$ be an ${\cal X}_{5}$-interpretation and $F$ a nested expression. Then:

• •

$\langle H,T\rangle\models F$* iff $H\models F^{T}$;*

• •

$\langle H,T\rangle=\!\!\!\!|\;F$* iff $H=\!\!\!\!|\;F^{T}$. *$\Box$

Corollary 1

For any consistent set of literals $T$ and any program $\Pi$: $\langle T,T\rangle\models\Pi$ iff $T\models\Pi$. $\Box$

Proposition 3

For any ${\cal X}_{5}$-intepretation $\langle H,T\rangle$ and any program $\Pi$:

$\langle H,T\rangle\models\Pi$* iff $H$ is a model of $\Pi^{T}$ and $T$ is a model of $\Pi$.*

$\Box$

Definition 4** (Equilibrium model)**

A total ${\cal X}_{5}$-interpretation $\langle T,T\rangle$ is an equilibrium model of a theory $\Gamma$ if $\langle T,T\rangle$ is a model of $\Gamma$ and there is no other model $\langle H,T\rangle$ of $\Gamma$ with $H\subset T$. $\Box$

Equilibrium logic (with explicit negation) is the non-monotonic logic induced by equilibrium models. The following theorem guarantees that equilibrium models and answer sets coincide for the syntax of programs with nested expressions.

Theorem 3

An interpretation $T$ is an answer set of a program $\Pi$ iff $\langle T,T\rangle$ is an equilibrium model of $\Pi$. $\Box$

To conclude this section, we provide an alternative reduct definition for arbitrary formulas (and not just nested expressions) obtained as a generalisation of Ferraris’ reduct [Ferraris (2005)]. This generalisation introduces a main feature333We also provide a translation for implications $\alpha\to\beta$ but this is not strictly necessary: for computing the reduct, they can be previously replaced by $\neg\alpha\vee\beta$. with respect to [Ferraris (2005)]: it actually uses two dual transformations, $\varphi^{T}_{+}$ and $\varphi^{T}_{-}$, to obtain a symmetric behaviour depending on the number of explicit negations in the scope.

Definition 5

Given a formula $\varphi$ and an interpretation $T$ (a consistent set of explicit literals) we define the following pair of mutually recursive transformations:

[TABLE]

The reduct $\Gamma^{T}_{+}$ of a theory $\Gamma$ is just defined as the set $\{\varphi^{T}_{+}\mid\varphi\in\Gamma\}$. $\Box$

For instance, given $\varphi=\eqref{f:bird}$ and $T=\{\sim\!\!\mathit{bird}\}$, the reader can check that the application of the definition above eventually produces the formula $\varphi^{T}_{+}=\neg\neg\bot\vee\sim\!\!(\mathit{bird}\wedge\top)$ which is equivalent to $\sim\!\!\mathit{bird}$. If we take $T=\{\mathit{flies}\}$ instead, the result is $\varphi^{T}_{+}=\neg\neg\bot\vee\sim\!\!(\top\wedge\sim\!\!\mathit{flies})$ that is equivalent to $\mathit{flies}$. As a third example, if we take $T=\{\mathit{bird}\}$ then we directly get $\varphi^{T}_{+}=\bot$.

Theorem 4

For any formula $\varphi$ and any pair of interpretations $H\subseteq T$:

1. (i)  $H\models\varphi^{T}_{+}$ iff $\langle H,T\rangle\models\varphi$;
2. *(ii) $H=\!\!\!\!|\;\varphi^{T}_{-}$ iff $\langle H,T\rangle=\!\!\!\!|\;\varphi$. *$\Box$

From Lemma 2 and Theorem 4 we immediately conclude:

Corollary 2

For any nested expression $F$ and any pair of interpretations $H\subseteq T$:

1. (i)

$H\models F^{T}$* iff $T\models F$ and $H\models F^{T}_{+}$;* 2. (ii)

$H=\!\!\!\!|\;F^{T}$* iff $T=\!\!\!\!|\;F$ and $H=\!\!\!\!|\;F^{T}_{-}$. *$\Box$

Corollary 3

$\langle T,T\rangle$* is an equilibrium model of $\Gamma$ iff $T$ is a minimal model of $\Gamma^{T}_{+}$. $\Box$*

Back to the example formula $\varphi=$(2), taking $T=\{\sim\!\!\mathit{bird}\}$ we saw that $\varphi^{T}_{+}$ is equivalent to $\sim\!\!\mathit{bird}$ whose minimal model is obviously $T$. Therefore, $\langle T,T\rangle$ is an equilibrium model.

4 Multivalued characterisation and equivalence relations

An alternative way of characterising ${\cal X}_{5}$ is as a five-valued logic defined as follows. Given any ${\cal X}_{5}$-interpretation $M=\langle H,T\rangle$ we define its corresponding 5-valued mapping $M:\mathit{At}\to\{-2,-1,0,1,2\}$ so that, for any atom $p\in\mathit{At}$:

[TABLE]

We can read these five values as follows: $2$ = proved to be true; $-2$ = proved to be false; $1$ = true by default; $-1$ = false by default; and [math] = undefined. Notice that values $1$ and $-1$ are used for explicit literals in $T\setminus H$. As a consequence:

Proposition 4

An ${\cal X}_{5}$-interpretation $M=\langle H,T\rangle$ is total (i.e. $H=T$) iff $M(p)\in\{-2,0,2\}$ for all $p\in\mathit{At}$. $\Box$

Definition 6** (Valuation of formulas)**

This 5-valuation can be extended to arbitrary formulas in the following way: {IEEEeqnarray}lCl+x* M(⊥) & =def -2

M(⊤) =def 2

M(φ*∧*ψ) =def min(M(φ),M(ψ))

M(φ*∨*ψ) =def max(M(φ),M(ψ))

M(φ*→*ψ) =def { 2if M(φ) ≤max(M(ψ),0)M(ψ)otherwise

M(*∼​​φ) =def -M(φ) $\Box$

The designated value is $2$, that is, we will understand that a formula is satisfied when $M(\varphi)=2$. Moreover, a complete correspondence with the satisfaction/falsification of formulas given in the previous section is fixed by the following theorem:

Theorem 5

For any ${\cal X}_{5}$-interpretation $M=\langle H,T\rangle$ and any formula $\varphi$:

• •

$\langle H,T\rangle\models\varphi$* iff $M(\varphi)=2$;*

• •

$\langle T,T\rangle\models\varphi$* iff $M(\varphi)>0$;*

• •

$\langle H,T\rangle=\!\!\!\!|\;\varphi$* iff $M(\varphi)=-2$;*

• •

$\langle T,T\rangle=\!\!\!\!|\;\varphi$* iff $M(\varphi)<0$. *$\Box$

The equilibrium condition given in Definition 4 can be rephrased in 5-valued terms as follows. Given two ${\cal X}_{5}$-interpretations $M=\langle H,T\rangle$ and $M^{\prime}=\langle H^{\prime},T^{\prime}\rangle$ we say that $M$ is smaller than $M^{\prime}$, written $M\leq M^{\prime}$, when $T=T^{\prime}$ and $H\subseteq H^{\prime}$.

Proposition 5

Let $M$ and $M^{\prime}$ be a pair of ${\cal X}_{5}$-interpretations. Then $M\leq M^{\prime}$ iff, for any atom $p\in\mathit{At}$, the following three conditions hold:

$M(p)=0$* iff $M^{\prime}(p)=0$;* 2. 2.

If $M(p)>0$, then $M(p)\leq M^{\prime}(p)$; 3. 3.

*If $M(p)<0$, then $M^{\prime}(p)\leq M(p)$. *$\Box$

Theorem 6

A total interpretation $M=\langle T,T\rangle$ is an equilibrium model of a theory $\Gamma$ iff $M(\varphi)=2$ for all $\varphi\in\Gamma$ and there is no $M^{\prime}<M$ such that $M^{\prime}(\varphi)=2$ for all $\varphi\in\Gamma$.

Proof 4.7**.**

It follows from Theorem 5 and the definition of $\leq$ relation.

The truth tables derived from Definition 6 are depicted in Figure 1, including the tables for derived operators ‘$\neg$’, ‘$\leftrightarrow$’ and ‘$\Leftrightarrow$’. Note that the table for $\neg\varphi=(\varphi\to\bot)$ is just the first column of the table for ‘$\to$’ since the evaluation of ‘$\bot$’ is fixed to $-2$.

It is easy to check, for instance, that the following implication is valid:

[TABLE]

expressing that explicit negation is stronger than default negation444This property is called the coherence principle in [Pereira and Alferes (1992)].. Moreover, default negation is definable in terms of implication and explicit negation (without resorting to $\bot$) since, with some effort, it can be checked that the table for $\neg\varphi$ can be equally obtained through the expression:

[TABLE]

An important remark regarding equivalence is that to express that this (or any) pair of formulas are equivalent, double implication does not suffice. This is because, as we can see in the tables, $M(\varphi\leftrightarrow\psi)=2$ does not imply that $M(\varphi)=M(\psi)$. To get such a correspondence, we must resort instead to the stronger ‘$\Leftrightarrow$’ for which $M(\varphi\Leftrightarrow\psi)=2$ holds if and only if $M(\varphi)=M(\psi)$. This lack of the ‘$\leftrightarrow$’ equivalence (we call it weak equivalence) has an important consequence: it does not define a congruence relation since $\models\alpha\leftrightarrow\beta$ no longer implies that we can freely replace subformula $\alpha$ by $\beta$ in any arbitrary context: it may be the case that $\not\models\sim\!\!\alpha\leftrightarrow\sim\!\!\beta$. For instance, we can easily check that $\models p\wedge\neg p\leftrightarrow\bot$ because $\min(M(p),M(\neg p))\leq 0$ and $M(\bot)=-2$, so $M(p\wedge\neg p\leftrightarrow\bot)=2$ for any $M$. However, we cannot replace $p\wedge\neg p$ by $\bot$ in any context. Take the program $\Pi$ consisting of the unique rule

[TABLE]

with empty body. Interpretation $T=\{\sim\!\!p\}$ is an answer set because $\Pi^{T}=\{\sim\!\!(p\wedge\top)\}$ has $\{\sim\!\!p\}$ as minimal model (in fact, it is the unique answer set) but if we replace $p\wedge\neg p$ by $\bot$ in $\Pi$ we get the trivial program $\{\sim\!\!\bot\}$ whose unique answer set is $\emptyset$. Although weak equivalence does not guarantee arbitrary replacements, it can be used to replace formulas in a theory, as stated below:

Proposition 4.8**.**

Let $\alpha$, $\beta$ be a pair of formulas such that $\models\alpha\leftrightarrow\beta$. Then, $M\models\Gamma\cup\{\alpha\}$ iff $M\models\Gamma\cup\{\beta\}$ for any theory $\Gamma$ and ${\cal X}_{5}$-interpretation $M$.∎

As we mentioned before, for obtaining a congruence relation we can use validity of ‘$\Leftrightarrow$’ instead, which guarantees the following substitution theorem.

Theorem 4.9** (Substitution).**

Let $\alpha$, $\beta$ be a pair of formulas satisfying $\models\alpha\Leftrightarrow\beta$. Then, for any formula $\varphi$, we also obtain $\models\varphi[\alpha/p]\Leftrightarrow\varphi[\beta/p]$. ∎

Still, there are some cases in which $\leftrightarrow$ can be used for substitution, provided that the replaced formulas are not in the scope of explicit negation.

Theorem 4.10**.**

Let $\varphi$ be a formula where atom $p$ only occurs outside the scope of explicit negation, and let $\alpha,\beta$ be two formulas satisfying $\models\alpha\leftrightarrow\beta$. Then, $\models\varphi[\alpha/p]\leftrightarrow\varphi[\beta/p]$.∎

An important property of ASP related to HT equivalence is strong equivalence. We say that two programs (resp. theories) $\Gamma$ and $\Gamma^{\prime}$ are strongly equivalent iff $\Gamma\cup\Delta$ and $\Gamma^{\prime}\cup\Delta$ have the same answer sets (resp. equilibrium models), for any additional program (resp. theory) $\Delta$. When we talk about strong equivalence of formulas $\alpha$ and $\beta$ we assume they correspond to the singleton theories $\{\alpha\}$ and $\{\beta\}$. As shown in [Lifschitz et al. (2001)] (for the case without explicit negation), two programs or theories are strongly equivalent if and only if they are HT equivalent. Since the ‘$\leftrightarrow$’ relation in HT is congruent, there is no difference between strong equivalence (replacing formulas in a theory) and substitution (replacing subformulas in a formula). However, as explained in [Ortiz and Osorio (2007)], once congruence is lost, we can further refine strong equivalence in the following way.

Definition 4.11** (Strong equivalence on substitution).**

We say that two formulas $\alpha$ and $\beta$ are strongly equivalent on substitutions if $\Delta\cup\{\varphi[\alpha/p]\}$ and $\Delta\cup\{\varphi[\beta/p]\}$ have the same equilibrium models, for any formula $\varphi$ and theory $\Delta$.

The proof of the next lemma can be obtained following similar steps to the proof of the main theorem in [Lifschitz et al. (2001)] replacing atoms in that case by explicit literals in ours.

Lemma 4.12**.**

Let $\alpha$ and $\beta$ be two formulas and be an interpretation such that $\langle H,T\rangle\models\alpha$ but $\langle H,T\rangle\not\models\beta$. Then, there is a finite theory $\Delta$ such that $\langle T,T\rangle$ is an equilibrium model of one of $\Delta\cup\{\beta\}$, $\Delta\cup\{\alpha\}$ but not of both.∎

Theorem 4.13**.**

Formulas $\alpha$ and $\beta$ are strongly equivalent iff $\models\alpha\leftrightarrow\beta$.∎

Theorem 4.14**.**

Formulas $\alpha$ and $\beta$ are strongly equivalent on substitutions iff $\models\alpha\Leftrightarrow\beta$.∎

The following set of valid equivalences allow us reducing any nested expression with explicit negation to an explicit negation normal form (NNF) where $\sim\!\!$  is only applied on atoms.

[TABLE]

For instance, we can reduce the nested expression (4) to NNF as follows:

[TABLE]

Programs in NNF correspond to the original syntax in [Lifschitz et al. (1999)]. That paper provided several transformations that allowed reducing any program in NNF to a regular program. These transformations included commutativity and associativity of conjunction and disjunction (which are obviously satisfied in ${\cal X}_{5}$) plus the equivalences in the following proposition.

Proposition 4.15**.**

The following formulas are ${\cal X}_{5}$ tautologies:

[TABLE]

[TABLE]

and correspond to the transformations in [Lifschitz et al. (1999)].∎

For instance, as we saw, (4) was equivalent to $\sim\!\!p\vee\neg\neg p$ but this can be further transformed into the regular rule $\neg p\to\sim\!\!p$ commonly used to assign falsity of $p$ by default.

Example 4.16** (Example 2 continued).**

Rule (2) can be transformed as follows:

[TABLE]

and the last step is a conjunction of two regular rules as in standard ASP solvers.∎

Reduction to NNF is also possible on arbitrary formulas. For that purpose, we can combine (5)-(10) with the following valid (weak) equivalence:

[TABLE]

However, the reduction must be done with some care, because this last equivalence cannot be shifted to $\Leftrightarrow$. Indeed, the left and right expressions have different valuations when $M(\varphi)=M(\psi)=1$, obtaining $M(\sim\!\!(\varphi\to\psi))=-2\neq-1=M(\neg\neg\varphi\wedge\sim\!\!\psi)$. Fortunately, Theorem 4.10 allows us applying (21) from the outermost occurrence of $\sim$ and then recursively combining with (5)-(10) until $\sim$ is only applied to atoms.

Theorem 4.17**.**

For any formula $\varphi$ there exists a formula $\psi$ in NNF such that $\models\varphi\leftrightarrow\psi$.∎

For instance, we can reduce the following formula into NNF as follows:

[TABLE]

However, we cannot apply (21) making a replacement in the scope of explicit negation. A clear counterexample is the formula $\sim\!\!\ \sim\!\!(p\to q)$ that, due to (9), is strongly equivalent to $p\to q$, but applying (21) inside would incorrectly lead to the nested expression $\sim\!\!(\neg\neg p\wedge\sim\!\!q)$ that can be transformed into the strongly equivalent expression $\neg p\vee q$, different from $p\to q$ in ASP.

5 Related work

As explained in the introduction, this work is obviously related to the characterisation of ‘$\sim$’ as Nelson’s strong negation [Nelson (1949)] for intermediate logics. In particular, the addition of strong negation to HT produces the five-valued logic ${\cal N}_{5}$ already present in the original definition of Equilibrium Logic [Pearce (1997)]. In fact, the interpretations and the truth values we have chosen for ${\cal X}_{5}$ coincide with those for ${\cal N}_{5}$, and their evaluation of (non-derived) connectives $\top,\wedge,\vee$ and $\to$ from Figure 1 also coincide in both logics, except for one difference in the table of implication: the value for $M(\varphi)=1$ and $M(\psi)=-2$ changes from $-2$ to $-1$ in ${\cal N}_{5}$. This change and its result on derived operators is shown in Figure 2 where the different values are framed in rectangles.

As a result, ${\cal N}_{5}$ ceases to satisfy (10) and (21) whose role in the reduction to NNF is respectively replaced by the ${\cal N}_{5}$-valid weak equivalences:

[TABLE]

The difference between (21) and (23) also reveals the effect on falsification of implication in both logics. While $\langle H,T\rangle=\!\!\!\!|\;\varphi\to\psi$ requires $\langle T,T\rangle\models\varphi$ in ${\cal X}_{5}$, this is replaced by condition $\langle H,T\rangle\models\varphi$ in ${\cal N}_{5}$. Curiously, although these two logics provide a different behaviour for $\sim\!\!$  as strong versus explicit negation, they actually have the same evaluation for that connective, while their real technical difference lies on falsity of implication.

The reason why ${\cal N}_{5}$ does not capture the extended reduct for nested expressions proposed in this paper is that (16) is not valid in that logic. This is because, when $M(\varphi)=1$, we get $M(\neg\varphi)=-1\neq-2=M(\neg\neg\neg\varphi)$. It is still possible to define ${\cal N}_{5}$ operators in ${\cal X}_{5}$ as follows:

[TABLE]

using here the ${\cal X}_{5}$ interpretation for implication. Analogously, we can also define the ${\cal X}_{5}$ operators in ${\cal N}_{5}$ in the following way:

[TABLE]

assuming that we interpret implication and $\neg$ under ${\cal N}_{5}$ instead.

An interesting connection between both variants is that the addition of the excluded middle axiom schemata $\varphi\vee\neg\varphi$ imposes the restriction of total models $\langle T,T\rangle$ both in ${\cal X}_{5}$ and in ${\cal N}_{5}$. This means that all atoms and formulas are evaluated in the set $\{-2,0,2\}$, for which the truth tables coincide in these two logics and actually collapse to classical logic with strong negation [Vakarelov (1977)] introduced in Section 2. This coincidence is important since equilibrium models (and so, answer sets) are total models.

To conclude the section on related work, another possibility for interpreting a second negation ‘$\sim\!\!$’ inside intuitionistic logic was provided by [Fariñas del Cerro and Herzig (1996)] using a classical negation interpretation. Although the idea seems closer to Gelfond and Lifschitz’ original terminology for a second negation, it actually provides undesired effects from an ASP point of view. Classical negation in HT means keeping only the satisfaction relation ‘$\models$’ in Definition 3 (falsification ‘$=\!\!\!\!|\;$’ is not needed) but replacing the condition for ‘$\sim\!\!$’ so that $\langle H,T\rangle\models\sim\!\!\varphi$ if $\langle H,T\rangle\not\models\varphi$. One important effect of this change is that HT with classical negation ceases to satisfy the persistence property (Theorem 2). But perhaps a more important problem from the ASP perspective is that $\neg p$ implies $\sim\!\!p$ for any atom $p$. Thus, the rule $\neg p\to\sim\!\!p$ becomes a tautology in this context, whereas it is normally used in ASP to conclude that $p$ is explicitly false by default.

6 Conclusions

We have introduced a variant of constructive negation in Equilibrium Logic (and its monotonic basis, HT) we called explicit negation. This variant shares some similarities with the previous formalisation based on Nelson’s strong negation, but changes the interpretation for falsity of implication. We have also introduced a reduct-based definition of answer sets for programs with nested expressions extended with explicit negation, proving the correspondence with equilibrium models.

For future work, we will study a possible axiomatisation. To this aim, it is interesting to observe that the formulas (7)-(9) (in their weak equivalence versions) plus (22) and (23) actually correspond to Vorob’ev axiomatisation [Vorob’ev (1952a), Vorob’ev (1952b)] of strong negation in intuitionistic logic. As we saw, the role of (22) and (23) in ${\cal N}_{5}$ is replaced in ${\cal X}_{5}$ by (9) and (21), so an interesting question is whether this replacement may become a complete axiomatisation for explicit negation in ${\cal X}_{5}$ or intuitionistic logic in the general case. We also plan to explore the effect of explicit negation on extensions of equilibrium logic, revisiting the use of strong negation in paraconsistent [Odintsov and Pearce (2005)] and partial [Cabalar et al. (2006)] equilibrium logic, or considering its combination with partial functions [Cabalar (2011), Cabalar et al. (2014)], and temporal [Aguado et al. (2013)] or epistemic [Fariñas del Cerro et al. (2015), Cabalar et al. (2019)] reasoning.