# Tree-Like Justification Systems are Consistent††thanks: This work was
partially supported by Fonds Wetenschappelijk Onderzoek – Vlaanderen (project
G0B2221N).

Simon Marynissen KU Leuven, Leuven, BelgiumVrije Universiteit Brussel,
Brussel, Belgium<EMAIL_ADDRESS>Vrije Universiteit Brussel,
Brussel, Belgium Bart Bogaerts Vrije Universiteit Brussel, Brussel, Belgium
<EMAIL_ADDRESS>
###### Abstract

Justification theory is an abstract unifying formalism that captures semantics
of various non-monotonic logics. One intriguing problem that has received
significant attention is the _consistency problem_ : under which conditions
are justifications for a fact and justifications for its negation suitably
related. Two variants of justification theory exist: one in which
justifications are trees and one in which they are graphs. In this work we
resolve the consistency problem once and for all for the tree-like setting by
showing that all reasonable tree-like justification systems are consistent.

##  1 Introduction

Justification theory [4] is a unifying theory to capture semantics of non-
monotonic logics. Largely thanks to its abstract nature, it is a powerful
framework with many use cases. First, it provides a mechanism to _define new
logics_ based on well-known principles in a uniform way, as well as to
_transfer results_ between domains. Second, it brings order in the zoo of
logics and semantics, by enabling a _systematic comparison_ between multiple
semantics for a single logic and between different logics, for instance by
answering the question whether a certain semantics of a given logic coincides
with a semantics of another logic. Third, building on the notion of _nested
justification systems_ 111Nested justification systems were originally defined
by Denecker et al.[4], but have remained largely unexplored since then. In a
companion paper to this paper [14], we provide a systematic study of nested
systems and their properties, it facilitates _modular definitions of knowledge
representation languages and semantics_.

Justification theory builds on the semantic notion of a _justification_ ,
which can intuitively be understood as an explanation (in the form of a tree
or a directed graph) as to why a certain fact is true or false. For this
reason, logics of which the semantics is captured by justification theory
automatically come with a mechanism of _explanation_ , which is of increasing
importance for societal and legal reasons. On top of that, justifications have
repeatedly proven to be useful algorithmically. They have been used in the
unfounded set algorithm of Gebser et al.[6], for improving lazy grounding
algorithms [2], as well as to speed-up parity game solvers [10].

The roots of justification theory can be traced back to the doctoral thesis of
Denecker [3], where it was developed as a framework for studying semantics of
logic programs. Later, Denecker et al.[4] developed a more general theory,
aiming to also capture other knowledge representation formalisms, such as
abstract argumentation [5], and nested least and greatest fixpoint definitions
[9]. A notable difference between the original work of Denecker [3] and the
theory of Denecker et al.[4] is that in the former work, a justification is a
tree where the nodes are labeled with literals, while in the latter a
justification is a (directed) graph. The relationship between these two
formalisms was studied among others by Marynissen et al.[12]. For clarity, we
will refer to _tree-like_ and _graph-like_ justifications when the distinction
is important.

In justification theory, whether or not a justification is “good” is
determined by a _branch evaluation_. A branch evaluation is a function that
associates to each path through a justification (i.e., to each branch of the
justification) a value. However, a priori, it is not clear that each branch
evaluation induces a well-defined semantics. For this to be the case,
intuitively the justifications of a fact $x$ and those of its negation
$\mathord{\sim}x$ should be suitably related. Indeed, we cannot accept that
there is both an explanation that $x$ is true and an explanation that
$\mathord{\sim}x$ is true. In general, to get a well-defined semantics we will
need that the best possible justification for $x$ and the best possible
justification for $\mathord{\sim}x$ are complementary (either one of them is
true and the other false, or both are unknown). The problem of determining
whether or not a branch evaluation induces a well-defined semantics is known
as the _consistency problem_ and has been studied in several papers.

  * •

Denecker [3, Theorem 4.3.1] studied the consistency problem for _tree-like_
justifications for three specific branch evaluations (corresponding to
completion semantics, stable semantics and well-founded semantics in logic
programming).

  * •

Marynissen et al.[15] were the first to exhibit a branch evaluation that (for
graph-like justifications) is _not_ consistent. Moreover, they showed that for
_graph-like_ justifications, four branch evaluations (in addition to the three
mentioned above, also the Kripke-Kleene branch evaluation) are guaranteed to
be consistent.

  * •

Marynissen et al.[12] investigated the relationship between justification
theory and games over graphs [8]. They used this relationship to identify some
key properties that, when satisfied by a branch evaluation, guarantee that
that branch evaluation is consistent for graph-like _and_ tree-like
justifications, but only in the context of a _finite_ fact space.

Despite all these efforts, there is no clear understanding yet of what it is
that makes a branch evaluation consistent. Moreover, proofs of consistency of
individual branch evaluations often span several pages. In this paper, we
resolve this question once and for all for tree-like justifications. Our main
theorem states that: _for tree-like justifications, every reasonable branch
evaluation is consistent_. The proof is surprisingly simple (compared to
earlier proofs for individual branch evaluations) and is completely included
in the main text. The results presented in this paper are part of the PhD
thesis of the first author [11].

The rest of this paper is structured as follows. We recall some basic
definitions of justification theory (focusing solely on tree-like
justifications) in Section 2 and state the consistency problem in Section 3.
In Section 4 we present the core theoretic results (in somewhat more
generality) that are subsequently used to prove our main result (namely that
every reasonable branch evaluation is consistent) in Section 5. We conclude in
Section 6.

##  2 Preliminaries

We present the core definitions of justification theory, based on the
formalization of Marynissen et al.[12, 13].

In the rest of this paper, let $\mathbb{F}$ be a set, referred to as a _fact
space_ , such that
$\mathcal{L}=\left\\{\mathbf{t},\mathbf{f},\mathbf{u}\right\\}\subseteq\mathbb{F}$,
where $\mathbf{t}$, $\mathbf{f}$ and $\mathbf{u}$ have the respective meaning
_true_ , _false_ , and _unknown_. The elements of $\mathbb{F}$ are called
_facts_. The set $\mathcal{L}$ behaves as the three-valued logic with truth
order $\leq_{t}$ given by $\mathbf{f}\leq_{t}\mathbf{u}\leq_{t}\mathbf{t}$. We
assume that $\mathbb{F}$ is equipped with an involution
$\mathord{\sim}:\mathbb{F}\rightarrow\mathbb{F}$ (i.e., a bijection that is
its own inverse) such that $\mathord{\sim}\mathbf{t}=\mathbf{f}$,
$\mathord{\sim}\mathbf{u}=\mathbf{u}$, and $\mathord{\sim}x\neq x$ for all
$x\neq\mathbf{u}$. For any fact $x$, $\mathord{\sim}x$ is called the
_complement_ of $x$. An example of a fact space is the set of literals over a
propositional vocabulary $\Sigma$ extended with $\mathcal{L}$ where
$\mathord{\sim}$ maps a literal to its negation. For any set $A$ we define
$\mathord{\sim}A$ to be the set of elements of the form $\mathord{\sim}a$ for
$a\in A$. We distinguish two types of facts: _defined_ and _open_ facts. The
former are accompanied by a set of rules that determine their truth value. The
truth value of the latter is not governed by the rule system but comes from an
external source or is fixed (as is the case for logical facts).

######  Definition 2.1.

A _justification frame_ $\mathbb{JF}$ is a tuple
$\left\langle\mathbb{F},\mathbb{F}_{d},R\right\rangle$ such that

  * •

$\mathbb{F}_{d}$ is a subset of $\mathbb{F}$ closed under $\mathord{\sim}$,
i.e. $\mathord{\sim}\mathbb{F}_{d}=\mathbb{F}_{d}$; facts in $\mathbb{F}_{d}$
are called _defined_ ;

  * •

no logical fact is defined: $\mathcal{L}\cap\mathbb{F}_{d}=\emptyset$;

  * •

$R\subseteq\mathbb{F}_{d}\times 2^{\mathbb{F}}$;

  * •

for each $x\in\mathbb{F}_{d}$, $(x,\emptyset)\notin R$ and there is an element
$(x,A)\in R$ for $\emptyset\neq A\subseteq\mathbb{F}$.

The set of _open_ facts is denoted as
$\mathbb{F}_{o}:=\mathbb{F}\setminus\mathbb{F}_{d}$. An element $(x,A)\in R$
is called a _rule_ with _head_ $x$ and _body_ (or _case_) $A$. The set of
cases of $x$ in $\mathbb{JF}$ is denoted as $\mathbb{JF}(x)$. Rules $(x,A)\in
R$ are often denoted as $x\leftarrow A$ and if
$A=\left\\{y_{\\_}1,\ldots,y_{\\_}n\right\\}$, we often write $x\leftarrow
y_{\\_}1,\ldots,y_{\\_}n$.

Logic programming rules can easily be transformed into rules in a
justification frame. However, in logic programming, only rules for positive
facts are given; never for negative facts.222In some extensions of logic
programming “classical negation” is allowed in the head of rules. In that
setting, an expression $\lnot p$ is a shorthand for an arbitrary atom that can
never be true together with $p$. This is significantly different from our
setting where $\mathord{\sim}p$ simply means that $p$ is false, and hence a
rule with $\mathord{\sim}p$ in the head states a condition under which $p$ is
false. To further illustrate this difference: if there are no rules for
$\mathord{\sim}p$, this means in our setting that $\mathord{\sim}p$ cannot be
true (hence $p$ cannot be false). In the aforementioned extensions of logic
programming, a lack of rules for $\lnot p$ entails nothing about $p$.  Hence,
in order to apply justification theory to logic programming, a mechanism for
deriving rules for negative literals is needed as well. Similarly, in the
setting of argumentation we can naturally derive rules for negative facts
(given attack relations), but rules for positive facts are less obvious. For
this, a technique called _complementation_ was invented [4]; it is a generic
mechanism that allows turning a set of rules for $x$ into a set of rules for
$\mathord{\sim}x$.

Complementation makes use of so-called selection functions for $x$. A
_selection function_ for $x$ is a mapping
$s\colon\mathbb{JF}(x)\rightarrow\mathbb{F}$ such that $s(A)\in A$ for all
rules of the form $x\leftarrow A$. Intuitively, a selection function chooses
an element from the body of each rule of $x$. For a selection function $s$,
the set $\\{s(A)\mid A\in\mathbb{JF}(x)\\}$ is denoted by
$\operatorname{Im}(s)$. Selection functions can be used to construct rules for
$\mathord{\sim}x$ from rules for $x$: intuitively, a fact $\mathord{\sim}x$
can be derived if every rule for $x$ fails. Formally, if $R$ is a set of
rules, the complement $\operatorname{C}(R)$ is the set of elements of the form
$\mathord{\sim}x\leftarrow\mathord{\sim}\operatorname{Im}(s)$ with $x$ defined
in $R$ and $s$ a selection function for $x$ in $R$. The _complementation_ of a
set of rules $R$ is $\operatorname{CC}(R):=R\cup\operatorname{C}(R)$.

In general, we will be interested in justification frames where the rules for
$x$ and the rules for $\mathord{\sim}x$ are suitably related. It does not
necessarily have to be the case that our frame is obtained by complementation,
but still we want to ensure that the rules are compatible. This has been
studied intensively by Marynissen et al.[15], who have given several
equivalent characterizations of when a justification frame is complementary.
Here, we give only one such characterization:

######  Definition 2.2.

Let $\mathbb{JF}=\left\langle\mathbb{F},\mathbb{F}_{d},R\right\rangle$ be a
justification frame. We call $\mathbb{JF}$ _complementary_ if for every
$x\in\mathbb{F}_{d}$ the following hold:

  1. 1.

for every selection function $s$ for $x$ in $R$, there exists an
$A\in\mathbb{JF}(\mathord{\sim}x)$ with
$A\subseteq\mathord{\sim}\operatorname{Im}(s)$;

  2. 2.

for every $A\in\mathbb{JF}(x)$, there exists a selection function $s$ for
$\mathord{\sim}x$ in $R$ with $\mathord{\sim}\operatorname{Im}(s)\subseteq A$.

The first item states that if we find a way to block every possible rule for
$x$ (by taking the complement of all the elements selected by a selection
function $s$ for $x$), then there should be a rule that derives
$\mathord{\sim}x$, i.e., there should be some rule $\mathord{\sim}x\leftarrow
A$ with $A$ containing only facts in $\mathord{\sim}\operatorname{Im}(s)$. The
second item states the other direction, namely that whenever we can derive $x$
(by means of a rule $x\leftarrow A$), it cannot be possible to
$\mathord{\sim}x$, i.e., at least one fact in each rule for $\mathord{\sim}x$
should be blocked. This is expressed again by means of a selection function:
there should exist a selection function that selects only facts that are the
complement of a fact in $A$. For more intuition regarding complementarity, we
refer the reader to Marynissen et al.[15, 12].

######  Example 2.3.

The justification frame

$\displaystyle p$ $\displaystyle\leftarrow q,\mathord{\sim}r$
$\displaystyle\mathord{\sim}p$ $\displaystyle\leftarrow\mathord{\sim}q$

is not complementary. Intuitively, the first rule states that $p$ holds
whenever $q$ is true and $r$ is false; this is the only case in which $p$ can
be derived. Since this is the only rule for $p$, we expect $p$ to be false
(i.e., $\mathord{\sim}p$ to be true) whenever $q$ is false or $r$ is true; the
first case is present, but the second case for $\mathord{\sim}p$ is missing.
After adding the rule

$\mathord{\sim}p\leftarrow r$ (1)

the frame becomes complementary. If we add a further rule

$\mathord{\sim}p\leftarrow r,q,$ (2)

the frame is still complementary; intuitively, (2) is a redundant rule, in the
sense that it is weaker than (1).

######  Definition 2.4.

A _directed labeled graph_ is a quadruple $(N,L,E,\ell)$ where $N$ is a set of
nodes, $L$ is a set of labels, $E\subseteq N\times N$ is the set of edges, and
$\ell\colon N\rightarrow L$ is a function called the labeling. An _internal_
node is a node with outgoing edges and a _leaf_ node is one without outgoing
edges.

######  Definition 2.5.

Let $\mathbb{JF}=\left\langle\mathbb{F},\mathbb{F}_{d},R\right\rangle$ be a
justification frame. A _(tree-like) justification_ $J$ in $\mathbb{JF}$ is a
directed labeled graph $(N,\mathbb{F}_{d},E,\ell)$ such that

  * •

the underlying undirected graph is a forest, i.e., is acyclic;

  * •

for every internal node $n\in N$ it holds that
$\ell(n)\leftarrow\\{\ell(m)\mid(n,m)\in E\\}\in R$.

######  Definition 2.6.

A justification is _locally complete_ if it has no leaves with label in
$\mathbb{F}_{d}$. We call $x\in\mathbb{F}_{d}$ a _root_ of a justification $J$
if there is a node $n$ labeled $x$ such that every node is reachable from $n$
in $J$.

We write $\mathfrak{J}(x)$ for the set of locally complete justifications
rooted in a node labeled $x$.

######  Definition 2.7.

Let $\mathbb{JF}$ be a justification frame. A $\mathbb{JF}$-_branch_ is either
an infinite sequence in $\mathbb{F}_{d}$ or a finite sequence in
$\mathbb{F}_{d}$ followed by an element in $\mathbb{F}_{o}$. For a
justification $J$ in $\mathbb{JF}$, a $J$-_branch_ starting in
$x\in\mathbb{F}_{d}$ is a path in $J$ starting in $x$ that is either infinite
or ends in a leaf of $J$. We write $B_{\\_}J(x)$ to denote the set of
$J$-branches starting in $x$.

Not all $J$-branches are $\mathbb{JF}$-branches since they can end in nodes
with a defined fact as label. However, if $J$ is locally complete, any
$J$-branch is also a $\mathbb{JF}$-branch.

We denote a branch $\mathbf{b}$ as $\mathbf{b}:x_{\\_}0\rightarrow
x_{\\_}1\rightarrow\cdots$ and define $\mathord{\sim}\mathbf{b}$ as
$\mathord{\sim}x_{\\_}0\rightarrow\mathord{\sim}x_{\\_}1\rightarrow\cdots$.

######  Definition 2.8.

A _branch evaluation_ $\mathcal{B}$ is a mapping that maps any
$\mathbb{JF}$-branch to an element in $\mathbb{F}$ for all justification
frames $\mathbb{JF}$. A branch evaluation $\mathcal{B}$ _respects negation_ if
$\mathcal{B}(\mathord{\sim}\mathbf{b})=\mathord{\sim}\mathcal{B}(\mathbf{b})$
for any branch $\mathbf{b}$. A justification frame $\mathbb{JF}$ together with
a branch evaluation $\mathcal{B}$ forms a _justification system_
$\mathbb{JS}$, which is presented as a quadruple
$\left\langle\mathbb{F},\mathbb{F}_{d},R,\mathcal{B}\right\rangle$.

We now define some branch evaluations that induce semantics corresponding to
the equally named semantics of logic programs.

######  Definition 2.9.

The _supported_ (completion) branch evaluation $\mathcal{B}_{\mathrm{sp}}$
maps $x_{\\_}0\rightarrow x_{\\_}1\rightarrow\cdots$ to $x_{\\_}1$ and
branches that consist only of a singe open fact $x_{\\_}0$ to $x_{\\_}0$. The
_Kripke-Kleene_ branch evaluation $\mathcal{B}_{\mathrm{KK}}$ maps finite
branches to their last element and infinite branches to $\mathbf{u}$.

Other branch evaluations have been defined as well, for instance stable and
well-founded branch evaluations, which correspond to the equally-named
semantics of logic programming [7, 16]. We refer the reader to the original
work introducing justification theory [4] for their definitions.

######  Definition 2.10.

A _(three-valued) interpretation_ of $\mathbb{F}$ is a function
$I:\mathbb{F}\rightarrow\mathcal{L}$ such that
$I(\mathord{\sim}x)=\mathord{\sim}I(x)$ and $I(\ell)=\ell$ for all
$\ell\in\mathcal{L}$.

######  Definition 2.11.

Let
$\mathbb{JS}=\left\langle\mathbb{F},\mathbb{F}_{d},R,\mathcal{B}\right\rangle$
be a justification system, $I$ an interpretation of $\mathbb{F}$, and $J$ a
locally complete justification in $\mathbb{JS}$. Let $x\in\mathbb{F}_{d}$ be a
label of a node in $J$. The _value_ of $x\in\mathbb{F}_{d}$ by $J$ under $I$
is defined as $\operatorname{val}(J,x,I)=\min_{\\_}{\mathbf{b}\in
B_{\\_}J(x)}I(\mathcal{B}(\mathbf{b}))$, where $\min$ is the minimum with
respect to $\leq_{t}$.

The _supported value_ of $x\in\mathbb{F}$ in $\mathbb{JS}$ under $I$ is
defined as

$\displaystyle\operatorname{SV}_{\\_}{\mathbb{JS}}(x,I)$
$\displaystyle=\max_{\\_}{J\in\mathfrak{J}(x)}\operatorname{val}(J,x,I)\text{
for $x\in\mathbb{F}_{d}$ }$
$\displaystyle\operatorname{SV}_{\\_}{\mathbb{JS}}(x,I)$
$\displaystyle=I(x)\text{ for $x\in\mathbb{F}_{o}$}.$

In other words, the value of a fact in a justification is the value of the
worst branch starting in that fact, and the supported value of a fact in an
interpretation is the value of that fact in its best justification. Models are
then defined as those interpretation in which the supported value of each fact
equals their actual value. Every branch evaluation induces a different class
of “models”. For instance, models under the supported branch evaluation
correspond to supported models in logic programming.

When $\mathbb{JS}$ is clear from the context, we will drop the subscript and
just write $\operatorname{SV}(x,I)$ for
$\operatorname{SV}_{\\_}{\mathbb{JS}}(x,I)$.

######  Definition 2.12.

Let
$\mathbb{JS}=\left\langle\mathbb{F},\mathbb{F}_{d},R,\mathcal{B}\right\rangle$
be a justification system. An $\mathbb{F}$-interpretation $I$ is a
$\mathbb{JS}$-model if for all $x\in\mathbb{F}_{d}$,
$\operatorname{SV}(x,I)=I(x)$. If $\mathbb{JS}$ consists of $\mathbb{JF}$ and
$\mathcal{B}$, then a $\mathbb{JS}$-model will also be called a
$\mathcal{B}$-model of $\mathbb{JF}$.

##  3 The Consistency Problem

We defined _models_ of a justification system by a kind of a fixpoint
equation: for $I$ to be a model, it must be a fixpoint of the operator
$S_{\mathbb{JS}}$ that maps $I$ to the interpretation $S_{\mathbb{JS}}(I)$,
which is the function

$\mathbb{F}\to\mathcal{L}:x\mapsto\operatorname{SV}(x,I).$

However, one intriguing problem is that domain and range of the support
operator are not equal: the range of the support operator is the set of
functions from $\mathbb{F}$ to $\mathcal{L}$, while the domain is the set of
$\mathbb{F}$-interpretations, which are functions from $\mathbb{F}$ to
$\mathcal{L}$ with some additional properties such as
$I(\mathord{\sim}x)=\mathord{\sim}I(x)$ for all $x\in\mathbb{F}$. We might
then wonder under which conditions, these properties will be guaranteed for
$S_{\mathbb{JS}}(I)$.

On top of that, there is a more fundamental reason why this property is
important. Explanations are of growing importance in various subdomains of
artificial intelligence. In our setting, a justification with value
$\mathbf{t}$ for $x$ serves as an explanation of why $x$ is true. But what if
$x$ is false? Which semantic structure can explain that? From the definition
of supported value, it can be seen that $x$ is false if _there are no
justifications_ with a better value (than $\mathbf{f}$) for $x$. But, the
absence of such justifications is difficult to argue. The question that then
remains is: how to show that there are no better justifications for $x$. The
most obvious solution is considering a justification of $\mathord{\sim}x$.
Indeed, intuitively, an explanation why the negation of $x$ is true should
explain why $x$ is false. However, this method implicitly assumes that
$\operatorname{SV}(\mathord{\sim}x,I)=\mathord{\sim}\operatorname{SV}(x,I)$,
thus motivating the following definition.

######  Definition 3.1.

A justification system $\mathbb{JS}$ is _consistent_ if
$\operatorname{SV}(\mathord{\sim}x,I)=\mathord{\sim}\operatorname{SV}(x,I)$
for every $x\in\mathbb{F}_{d}$ and every $\mathbb{F}$-interpretation $I$.

We are now ready to state the consistency problem, which is the central
research question of this article.

When is a justification system consistent? In particular, what properties do
branch evaluations and justification frames need to have to ensure that the
justification system is consistent?

Consistency is a reasonable assumption that, unfortunately, is not always
satisfied. An obvious way to not satisfy it is by having unrelated rules for
$x$ and $\mathord{\sim}x$.

$\left\\{\begin{array}[]{l}x\leftarrow\mathbf{t}\\\
\mathord{\sim}x\leftarrow\mathbf{t}\end{array}\right\\}$

Of course, in this example we cannot expect that the justifications for $x$
and $\mathord{\sim}x$ are related because their rules are contradictory. While
justification theory in principle works with such rule sets, most of the
theory has focused on complementary justification frames, where the rules for
$x$ and $\mathord{\sim}x$ are suitably related. Another way in which
consistency can be violated is if $\mathcal{B}$ does not respect negation.
Again, in its most general form, justification theory allows such strange
branch evaluations (e.g., one that maps every branch to $\mathbf{t}$, in which
every justification is always true), however there are no applications of such
branch evaluations.

In fact, the main result of our paper is that for _tree-like_ justifications,
the two aforementioned syntactic properties are enough to guarantee
consistency:

######  Theorem 3.2 (Main theorem).

Let
$\mathbb{JS}=\left\langle\mathbb{F},\mathbb{F}_{d},R,\mathcal{B}\right\rangle$
be a justification system. If $\mathbb{JS}$ is complementary and $\mathcal{B}$
respects negation, then $\mathbb{JS}$ is (tree-like) consistent.

We do want to stress the fact that this only holds for tree-like justification
systems: Marynissen et al.[15] gave an example of a branch evaluation that
respects negation, on a complementary justification frame, that is _not_
consistent for graph-like justifications (which we do not consider in this
paper).

##  4 Constructing a Justification

In this section, we will provide the core theoretic results that are needed to
prove our main theorem. In short, what we aim to show here is that if there
are no “good” justifications for $x$, then we can construct a “good”
justification for $\mathord{\sim}x$. We will prove this in some more
generality, making use of a new concept: a _branch selection_ : a set of
branches starting in a certain fact $x$ that contains at least one branch from
every justification of $x$. The main result of this section (Theorem 4.5) then
states that for every branch selection $\mathbb{B}$ for $x$, we can construct
a justification for $\mathord{\sim}x$ that only has branches in
$\mathord{\sim}\mathbb{B}$.

Throughout this section, we fix a justification system
$\mathbb{JS}=\left\langle\mathbb{F},\mathbb{F}_{d},R,\mathcal{B}\right\rangle$
with $\mathbb{JF}=\left\langle\mathbb{F},\mathbb{F}_{d},R\right\rangle$.

######  Definition 4.1.

A _branch selection_ for $x$ in $\mathbb{JF}$ is a set $\mathbb{B}$ of
branches starting in $x$ such that for each locally complete justification $J$
rooted in $x$, $\mathbb{B}$ contains at least one $J$-branch.

In what follows, if $x\leftarrow A$ is a rule, and for each $y\in A$,
$J_{\\_}y$ is a justification333In case $y$ is an open fact, there is only one
such justification, namely a justification with a single node and without
edges. rooted in $y$, we will write $x\stackrel{{\scriptstyle
A}}{{\rightarrow}}(J_{\\_}y)_{\\_}{y\in A}$ for the justification in which $A$
are the children of $x$ and such that the subtree rooted in $y\in A$ equals
$J_{\\_}y$.

######  Lemma 4.2.

Let $\mathbb{B}$ be a branch selection for $x$, and let $x\leftarrow A$ be a
rule in $\mathbb{JF}$. There exists a $y^{*}\in A$ such that for every
justification $J_{\\_}{y^{*}}\in\mathfrak{J}(y^{*})$ rooted in $y^{*}$,
$\mathbb{B}$ contains at least one branch of the form $x\to
y^{*}\to\mathbf{b}$ with $y^{*}\to\mathbf{b}$ a branch starting from the root
of $J_{\\_}{y^{*}}$.444In case $y^{*}$ is an open fact, this thus means that
$\mathbf{b}$ is the empty branch and $y^{*}\to\mathbf{b}$ is a branch with
only a single element $y^{*}$.

###### Proof.

Assume by contradiction that such a $y^{*}$ does not exist. This would mean
that for each $y\in A$, there exists a $J_{\\_}y\in\mathfrak{J}(y)$ such that
$\mathbb{B}$ does _not_ contain any branches of the form $x\to y\to\mathbf{b}$
with $y\to\mathbf{b}$ a branch in $J_{\\_}y$. However, if we have such a
justification for each $y\in A$, consider the justification
$x\stackrel{{\scriptstyle A}}{{\rightarrow}}(J_{\\_}y)_{\\_}{y\in A}$. Since
this is a locally complete justification of $x$, $\mathbb{B}$ must contain at
least one of its branches, which yields a contradiction. ∎

######  Corollary 4.3.

Let $\mathbb{B}$ be a branch selection for $x$, and let $x\leftarrow A$ be a
rule in $\mathbb{JF}$. There exists a $y^{*}\in A$ such that
$\mathbb{B}_{\\_}{y^{*}}:=\\{y^{*}\to\mathbf{b}\mid x\to
y^{*}\to\mathbf{b}\in\mathbb{B}\\}$ is a branch selection for $y^{*}$.

###### Proof.

The only thing we need to show is that $\mathbb{B}_{\\_}{y^{*}}$ contains at
least one branch from each justification rooted in $y^{*}$. This follows
directly from Lemma 4.2. ∎

######  Corollary 4.4.

Assume $\mathbb{JS}$ is a complementary justification system. If $\mathbb{B}$
is a branch selection for $x$ in $\mathbb{JF}$, then there exists a rule
$\mathord{\sim}x\leftarrow B_{\\_}{\mathord{\sim}x}$ for $\mathord{\sim}x$
such that for each $y\in\mathord{\sim}B_{\\_}{\mathord{\sim}x}$, we have that
$\mathbb{B}_{\\_}{y}:=\\{y\to\mathbf{b}\mid x\to
y\to\mathbf{b}\in\mathbb{B}\\}$ is a branch selection for $y$.

###### Proof.

Corollary 4.3 determines a selection function for $x$ in $\mathbb{JF}$, by
choosing from each $x\leftarrow A$ a $y^{*}\in A$. Then by complementarity of
$\mathbb{JS}$, there is a rule $\mathord{\sim}x\leftarrow
B_{\\_}{\mathord{\sim}x}$ such that every element of
$B_{\\_}{\mathord{\sim}x}$ is one of the selected $y^{*}$. ∎

######  Theorem 4.5.

If $\mathbb{JS}$ is a complementary justification system and $\mathbb{B}$ is a
branch selection for $x$ in $\mathbb{JF}$, then there exists a justification
$J^{\prime}$ rooted in $\mathord{\sim}x$ such that for each branch
$\mathbf{b}^{\prime}$ of $J^{\prime}$ starting in the root,
$\mathord{\sim}\mathbf{b}^{\prime}\in\mathbb{B}$.

###### Proof.

We will first construct a labeled tree $T$ rooted in $\mathord{\sim}x$ with
the properties that

  1. 1.

the label of each internal node is a defined fact;

  2. 2.

the label of each leaf is an open fact;

  3. 3.

for each path in $T$ starting in the root, the corresponing branch (obtained
by taking the labels of each node) is the negation of a branch in
$\mathbb{B}$.

However, our tree $T$ will not necessarily be a justification: the set of
children’s labels of an internal node will not necessarily be the body of a
rule for the label of that node. In the second part of the proof, we will then
prove that a subtree of $T$ indeed forms a justification.

Our tree $T$ is constructed as follows.

  * •

The nodes of $T$ are all finite prefixes of the branches in
$\mathord{\sim}\mathbb{B}$. That is, the nodes of $T$ are all sequences
$\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\mathord{\sim}x_{\\_}2\to\dots\to\mathord{\sim}x_{\\_}n$
such that there is a branch in $\mathbb{B}$ that starts with $x\to
x_{\\_}1\to\dots\to x_{\\_}n$. Each such node is labeled
$\mathord{\sim}x_{\\_}n$.

  * •

For each prefix
$\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\mathord{\sim}x_{\\_}2\to\dots\to\mathord{\sim}x_{\\_}{n-1}\to\mathord{\sim}x_{\\_}n$,
there is an edge from
$\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\mathord{\sim}x_{\\_}2\to\cdots\to\mathord{\sim}x_{\\_}{n-1}$
to
$\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\mathord{\sim}x_{\\_}2\to\dots\to\mathord{\sim}x_{\\_}n$.

By construction, there is a one-to-one correspondence between paths starting
in the root of $T$ and branches in $\mathbb{B}$. Since all branches in
$\mathbb{B}$ are part of a locally complete justification, it is clear that
indeed, the labels of internal nodes of this tree are defined facts and the
labels of leaves are open facts.

We will now show that we can choose a subtree $J^{\prime}$ of $T$ that is a
locally complete justification. For each node
$\eta=\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\cdots\to\mathord{\sim}x_{\\_}n$,
we define $\mathbb{B}_{\\_}\eta$ as the set of branches $\mathbf{b}$ starting
in $x_{\\_}n$ such that $x\to x_{\\_}1\to\dots\to x_{\\_}{n-1}\to\mathbf{b}$
is a branch in $\mathbb{B}$. For some nodes, $\mathbb{B}_{\\_}\eta$ is a
branch selection function for $x_{\\_}n$, but this is not guaranteed to be the
case for every node. For _those nodes_ $\eta$ (with label $\mathord{\sim}z$)
for which $\eta$ _is_ a branch selection for $z$, Corollary 4.4 guarantees
there is a rule $\mathord{\sim}z\leftarrow B_{\\_}{\mathord{\sim}z}$ such that
for each $\mathord{\sim}y\in B_{\\_}{\mathord{\sim}z}$, $\\{y\to\mathbf{b}\mid
z\to y\to\mathbf{b}\in\mathbb{B}_{\\_}\eta\\}$ is also a branch selection
function for $y$. For each such $\eta$, we choose such a rule and for the rest
of this proof denote $B_{\\_}{\mathord{\sim}z}$ as
$\mathit{chosenBody}(\eta)$. Given this choice, we construct the justification
$J$ inductively as follows:

  * •

The root $\mathord{\sim}x$ is a node in $J$.

  * •

For each node
$\eta=\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\mathord{\sim}x_{\\_}n$ in
$J$, and for each $\mathord{\sim}y\in\mathit{chosenBody}(\eta)$, the node
$\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\cdots\to\mathord{\sim}x_{\\_}n\to\mathord{\sim}y$
of $T$ is a node of $J$.

Of course, in order for this construction to work, we need to show that for
each node in $J$, $\mathit{chosenBody}(\eta)$ is well-defined, i.e., that for
each node $\eta$ in $J$ with label $\mathord{\sim}z$, $\mathbb{B}_{\\_}\eta$
is a branch selection function for $z$. We prove this inductively as well

  * •

This claim clearly holds for the root node since the corresponding branch
selection function simply equals $\mathbb{B}$.

  * •

If
$\eta=\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\cdots\to\mathord{\sim}x_{\\_}n$
is a node for which $\mathbb{B}_{\\_}\eta$ is a branch selection function for
$x_{\\_}n\in\mathbb{F}_{d}$ and $\mathord{\sim}y\in\mathit{chosenBody}(\eta)$,
let $\eta^{\prime}$ denote the node
$\mathord{\sim}x\to\mathord{\sim}x_{\\_}1\to\cdots\to\mathord{\sim}x_{\\_}n\to\mathord{\sim}y$.
We should show that $\mathbb{B}_{\\_}{\eta^{\prime}}$ is a branch selection
for $y$. Now this follows easily from the fact that

$\displaystyle\mathbb{B}_{\\_}{\eta^{\prime}}$
$\displaystyle=\\{y\to\mathbf{b}\mid x\to x_{\\_}1\to\cdots\to x_{\\_}n\to
y\to\mathbf{b}\in\mathbb{B}\\}$ $\displaystyle=\\{y\to\mathbf{b}\mid
x_{\\_}n\to y\to\mathbf{b}\in\mathbb{B}_{\\_}\eta\\}$

and this last set is guaranteed to be a branch selection (by Corollary 4.4).

This way of constructing $J$ indeed results in a locally complete
justification: for each internal node $\eta$ labeled $\mathord{\sim}z$ of $T$
that is part of $J$, a rule $\mathord{\sim}z\leftarrow B$ is selected and the
children of $\eta$ have labels in $B$, which thus concludes our proof. ∎

##  5 Tree-Like Justification Systems are Consistent

We now turn our attention to proving the main theorem of this paper (Theorem
3.2). As before, we fix a justification system
$\mathbb{JS}=\left\langle\mathbb{F},\mathbb{F}_{d},R,\mathcal{B}\right\rangle$
with $\mathbb{JF}=\left\langle\mathbb{F},\mathbb{F}_{d},R\right\rangle$.

One direction of the main theorem is fairly easy to prove: if we are given a
good justification for a certain fact, there cannot be a good justification
for its complement. This direction relies on the fact that for complementary
frames, the cases of $x$ and those of $\mathord{\sim}x$, and the justification
of $x$ and $\mathord{\sim}x$ are intrinsically related as formalized in the
following two lemmas (inspired by similar results for graph-like
justifications [15]).

######  Lemma 5.1.

If $\mathbb{JF}$ is complementary, then for all rules $x\leftarrow A$ and
$\mathord{\sim}x\leftarrow B$ in $R$, we have
$A\cap\mathord{\sim}B\neq\emptyset$.

###### Proof.

Take $A\in\mathbb{JF}(x)$ and $B\in\mathbb{JF}(\mathord{\sim}x)$. By
complementarity, there exists a selection function $s$ for $\mathord{\sim}x$
such that $\mathord{\sim}\operatorname{Im}(s)\subseteq A$. Therefore,
$\mathord{\sim}s(B)\in A$. On the other hand, $s(B)\in B$; hence
$\mathord{\sim}s(B)\in A\cap\mathord{\sim}B$. ∎

######  Lemma 5.2.

Let $\mathbb{JF}=\left\langle\mathbb{F},\mathbb{F}_{d},R\right\rangle$ be a
complementary justification frame and $x\in\mathbb{F}_{d}$. If $J$ and $K$ are
justifications in $\mathfrak{J}(x)$ and $\mathfrak{J}(\mathord{\sim}x)$
respectively, then there exists a $J$-branch $\mathbf{b}$ starting in $x$ such
that $\mathord{\sim}\mathbf{b}$ is a $K$-branch starting in $\mathord{\sim}x$.

###### Proof.

We incrementally define $J$-paths $\mathbf{b}_{\\_}i$ and $K$-paths
$\mathbf{b}_{\\_}i^{*}$ of length $i$ such that
$\mathbf{b}_{\\_}i=\mathord{\sim}\mathbf{b}_{\\_}i^{*}$. Define
$\mathbf{b}_{\\_}1$ and $\mathbf{b}_{\\_}1^{*}$ as the node $x$ and
$\mathord{\sim}x$ respectively. Now assume that we obtained
$\mathbf{b}_{\\_}i$ and $\mathbf{b}_{\\_}i^{*}$. Let $y$ be the end node of
$\mathbf{b}_{\\_}i$. If $y$ is not defined, so is $\mathord{\sim}y$ and then
$\mathbf{b}_{\\_}i$ is the desired $J$-branch. So assume $y$ is defined. We
want to find a fact $z$ such that $z$ is a child of $y$ in $J$ and
$\mathord{\sim}z$ is a child of $\mathord{\sim}y$ in $K$. By using the rules
for $y\leftarrow A$ in $J$ and $\mathord{\sim}y\leftarrow B$ in $K$ we can use
Lemma 5.1 to obtain that $A\cap\mathord{\sim}B\neq\emptyset$ because
$\mathbb{JF}$ is complementary. Choose a $z$ in $A\cap\mathord{\sim}B$. Then
we construct $\mathbf{b}_{\\_}{i+1}=\mathbf{b}_{\\_}i\rightarrow z$ and
$\mathbf{b}_{\\_}{i+1}^{*}=\mathbf{b}_{\\_}i^{*}\rightarrow\mathord{\sim}z$.
Our required branch is then the limit of $\mathbf{b}_{\\_}i$ for $i$ going to
infinity. ∎

From this lemma, one direction of consistency directly follows; this result
was also already shown by Marynissen et al.[12, Proposition 5.13], but we
include a direct proof to make the current paper self-contained.

######  Proposition 5.3.

If $\mathbb{JS}$ is complementary and $\mathcal{B}$ respects negation, then

$\operatorname{SV}(x,I)\leq_{t}\mathord{\sim}\operatorname{SV}(\mathord{\sim}x,I)$

for any $x\in\mathbb{F}_{d}$ and any $\mathbb{F}$-interpretation $I$.

###### Proof.

Take $x$ with $\operatorname{SV}(x,I)=\ell$ for some $\ell\in\mathcal{L}$.
This means there is a justification $J$ such that
$\operatorname{val}_{\\_}{\mathbb{JS}}(J,x,I)=\ell$. Take a justification $K$
for $\mathord{\sim}x$. Therefore, by Lemma 5.2, there is a $J$-branch
$\mathbf{b}$ starting in $x$ such that $\mathord{\sim}\mathbf{b}$ is a
$K$-branch starting in $\mathord{\sim}x$. We consider three cases:

  * •

If $\ell=\mathbf{t}$, then $I(\mathcal{B}(\mathbf{b}))=\mathbf{t}$; hence $K$
has a branch that is evaluated to $\mathbf{f}$. Therefore,
$\operatorname{val}_{\\_}{\mathbb{JS}}(K,\mathord{\sim}x,I)=\mathbf{f}$. Since
$K$ was taken arbitrarily, we have that
$\operatorname{SV}(\mathord{\sim}x,I)=\mathbf{f}$.

  * •

If $\ell=\mathbf{u}$, we need to prove that
$\mathbf{u}\geq_{t}\operatorname{SV}(\mathord{\sim}x,I)$. Similarly, every
justification $K$ for $\mathord{\sim}x$ has a branch
$\mathord{\sim}\mathbf{b}$ starting in $\mathord{\sim}x$ such that
$\mathbf{b}$ is a $J$-branch and
$I(\mathcal{B}(\mathbf{b}))\geq_{t}\mathbf{u}$. This shows that
$I(\mathcal{B}(\mathord{\sim}\mathbf{b}))\leq_{t}\mathbf{u}$. Therefore,
$\operatorname{SV}(\mathord{\sim}x,I)\leq_{t}\mathbf{u}$.

  * •

For $\ell=\mathbf{f}$, the statement is trivial.∎

The other direction of the consistency is completely novel and follows
directly from the theory developed in Section 4.

######  Proposition 5.4.

If $\mathbb{JS}$ is complementary and $\mathcal{B}$ respects negation, then

$\operatorname{SV}(x,I)\geq_{t}\mathord{\sim}\operatorname{SV}(\mathord{\sim}x,I)$

for any $x\in\mathbb{F}_{d}$ and any $\mathbb{F}$-interpretation $I$.

###### Proof.

Consider the branch selection

$\mathbb{B}_{\\_}{\mathord{\sim}x}=\left\\{\mathord{\sim}x\to\mathbf{b}\mid\mathcal{B}(\mathord{\sim}x\to\mathbf{b})\leq_{t}\operatorname{SV}(\mathord{\sim}x,I)\right\\}.$

This set is a branch selection for $\mathord{\sim}x$, because each
justification rooted in $\mathord{\sim}x$ must have at least one branch with a
value at most $\operatorname{SV}(\mathord{\sim}x,I)$. Theorem 4.5 then
guarantees that a justification $J$ rooted in a node labelled $x$ exists such
that every branch $\mathbf{b}$ in $J$ starting in the root is an element of
$\mathord{\sim}\mathbb{B}_{\\_}{\mathord{\sim}x}$; hence
$\mathcal{B}(\mathord{\sim}\mathbf{b})\leq_{t}\operatorname{SV}(\mathord{\sim}x,I)$.
Since $\mathcal{B}$ respects negation, we have
$\mathcal{B}(\mathbf{b})\geq_{t}\mathord{\sim}\operatorname{SV}(\mathord{\sim}x,I)$
for every $\mathbf{b}$ in $J$ starting in the root and thus that
$\operatorname{val}(J,x,I)\geq_{t}\mathord{\sim}\operatorname{SV}(\mathord{\sim}x,I)$.
From this, it immediately follows that
$\operatorname{SV}(x,I)\geq_{t}\mathord{\sim}\operatorname{SV}(\mathord{\sim}x,I)$.
∎

######  Theorem 5.5 (Main theorem, restated).

Let
$\mathbb{JS}=\left\langle\mathbb{F},\mathbb{F}_{d},R,\mathcal{B}\right\rangle$
be a justification system. If $\mathbb{JS}$ is complementary and $\mathcal{B}$
respects negation, then $\mathbb{JS}$ is tree-like consistent.

###### Proof.

Follows by combining Proposition 5.3 with Proposition 5.4. ∎

##  6 Conclusion

Consistency is an important property that relates the absence of an
explanation of a fact to the existence of an explanation for its complement.
Our results do not have an impact on branch evaluations that have been used
before, since for all of them, consistency has separately been proven.
However, we believe it will simplify future applications of (tree-like)
justification theory, by removing the burden of this proof obligation.
Moreover, the general formulation of our results in Section 4, in fact entails
that the so-called _flattening_ of a justification system [11] is
complementary. This notion of flattening is important in the context of
_nested_ justification systems [4, 14].

While we have now once and for all resolved the consistency question for tree-
like justifications, for graph-like justifications, this problem is still
open. However, in the PhD thesis of the first author [11, Corollary 2.4.7], we
show that a justification system is graph-like consistent if and only if it is
tree-like consistent and every tree-like justification can be transformed into
a graph-like justification555In graph-like justifications, each fact occurs as
the label of at most one node. The difficulty in this transformation is
dealing with tree-like justifications that make multiple choices for a given
fact. (a property that is there called _graph-reducibility_). The results we
presented in this work now entail that, under very mild assumptions, graph-
like consistency is equivalent to graph-reducibility, and hence indirectly,
also contributes to the understanding of graph-like justification systems.

## References

  * [1]
  * [2] Bart Bogaerts & Antonius Weinzierl (2018): _Exploiting Justifications for Lazy Grounding of Answer Set Programs_.  In Jérôme Lang, editor: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., ijcai.org, pp. 1737–1745, 10.24963/ijcai.2018/240.
  * [3] Marc Denecker (1993): _Knowledge representation and reasoning in incomplete logic programming_.  Ph.D. thesis, K.U.Leuven, Leuven, Belgium.
  * [4] Marc Denecker, Gerhard Brewka & Hannes Strass (2015): _A Formal Theory of Justifications_.  In Francesco Calimeri, Giovambattista Ianni & Mirosław Truszczyński, editors: Logic Programming and Nonmonotonic Reasoning - 13th International Conference, LPNMR 2015, Lexington, KY, USA, September 27-30, 2015. Proceedings, Lecture Notes in Computer Science 9345, Springer, pp. 250–264, 10.1007/978-3-319-23264-5_22.
  * [5] Phan Minh Dung (1995): _On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games_.  Artif. Intell. 77(2), pp. 321 – 357, 10.1016/0004-3702(94)00041-X.
  * [6] Martin Gebser, Roland Kaminski, Benjamin Kaufmann & Torsten Schaub (2009): _On the Implementation of Weight Constraint Rules in Conflict-Driven ASP Solvers_.  In Patricia M. Hill & David Scott Warren, editors: ICLP, LNCS 5649, Springer, pp. 250–264, 10.1007/978-3-642-02846-5.
  * [7] Michael Gelfond & Vladimir Lifschitz (1988): _The Stable Model Semantics for Logic Programming_.  In Robert A. Kowalski & Kenneth A. Bowen, editors: ICLP/SLP, MIT Press, pp. 1070–1080.  Available at http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.6050.
  * [8] Hugo Gimbert & Wieslaw Zielonka (2005): _Games Where You Can Play Optimally Without Any Memory_.  In Martín Abadi & Luca de Alfaro, editors: CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, Lecture Notes in Computer Science 3653, Springer, pp. 428–442, 10.1007/11539452_33.
  * [9] Ping Hou, Broes De Cat & Marc Denecker (2010): _FO(FD): Extending classical logic with rule-based fixpoint definitions_.  TPLP 10(4-6), pp. 581–596, 10.1017/S1471068410000293.
  * [10] Ruben Lapauw, Maurice Bruynooghe & Marc Denecker (2020): _Improving Parity Game Solvers with Justifications_.  In Dirk Beyer & Damien Zufferey, editors: Verification, Model Checking, and Abstract Interpretation \- 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings, Lecture Notes in Computer Science 11990, Springer, pp. 449–470, 10.1007/978-3-030-39322-9_21.
  * [11] Simon Marynissen (2022): _Advances in Justification Theory_.  Ph.D. thesis, Department of Computer Science, KU Leuven.  Available at https://lirias.kuleuven.be/3646147.  Denecker, Marc and Bart Bogaerts (supervisors).
  * [12] Simon Marynissen, Bart Bogaerts & Marc Denecker (2020): _Exploiting Game Theory for Analysing Justifications_.  Theory Pract. Log. Program. 20(6), pp. 880–894, 10.1017/S1471068420000186.
  * [13] Simon Marynissen, Bart Bogaerts & Marc Denecker (2021): _On the Relation Between Approximation Fixpoint Theory and Justification Theory_.  In Zhi-Hua Zhou, editor: Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, ijcai.org, pp. 1973–1980, 10.24963/ijcai.2021/272.
  * [14] Simon Marynissen, Bart Bogaerts, Marc Denecker & Jesse Heyninck (2022): _On Nested Justification Systems_.  Theory Pract. Log. Program. 22\.  To appear (Accepted for ICLP 2022 special issue in TPLP).
  * [15] Simon Marynissen, Niko Passchyn, Bart Bogaerts & Marc Denecker (2018): _Consistency in Justification Theory_.  In: Proceedings of 17th International Workshop on Non-Monotonic Reasoning (NMR 2018), Tempe, Arizona, USA, Oct. 27-29, 2018, AAAI Press 2018, pp. 41–52.  Available at http://www4.uma.pt/nmr2018/NMR2018Proceedings.pdf.
  * [16] Allen Van Gelder, Kenneth A. Ross & John S. Schlipf (1991): _The Well-Founded Semantics for General Logic Programs_.  J. ACM 38(3), pp. 620–650, 10.1145/116825.116838.


# Quantum Hall Goos–Hänchen effect in graphene

D. Jahani<EMAIL_ADDRESS>O. Akhavan, A. Alidoust Ghatar

###### Abstract

_Strong Goos–Hänchen (GH) effect at a prism-graphene interface in the quantum
Hall effect (QHE) condition is reported. Based on the full quantum description
of the temperature-dependent surface conductivity of graphene present in the
unconventional quantum Hall regime, magnetically strong tunable QHE GH shifts
emerge. Our approach is based on deriving the generalized Fresnel coefficients
with antisymmetric conductivity tensor for the Kerr phase of the incident
linearly polarized light. Moreover, it is demonstrated that at low
temperatures, GH shifts map plateaus as the intensity of the magnetic field
grows. This quantum modulation of the GH effect in graphene by an applied
magnetostatic bias may open doors to new opportunities for optical devices and
QHE sensing applications in 2D materials._

_Department of Physics, Sharif University of Technology, P.O. Box 11155-9161,
Tehran, Iran_

_Keywords_ : _Graphene; Goos-Hänchen effect; Quantum Hall effect; Terahertz
regime._

##  1 Introduction

_A lateral shift occurs between an incident light beam and its predicted
geometrical optical path for the reflected light at an interface when it
undergoes the total internal reflection condition. This so-called Goos–Hänchen
(GH) effect has been analyzed both theoretically and experimentally[1, 2, 3].
This phenomenon has attracted immense attention due to the development of
micro/nano-optics evolution at subwavelength scales [4]. However, being just
of the order of the wavelength of the incident light wave hinders its
application area. Thus, the enhancement and control of GH effect have recently
received rapidly increasing attention in various fields such as biomedicine,
sensors, modulators and acoustics, quantum mechanics, and plasma physics [5,
6, 7, 8, 9, 10, 11]. Up to now many ways such as layered structures, absorbing
media, photonic crystals with and without a defect layer, metamaterials and
prism coupling to 2D materials have been used to increase and control this
effect [12, 13, 14, 15, 16, 17]. Moreover, GH effect in graphene, a single
two-dimensional plane of carbon atoms in a honeycomb structure, has attracted
great attention and, therefore, has already been the subject of some
researches due to its extraordinary optical properties [18, 19, 20]. For
instance, many graphene-based structures including the Tamm states, photonic
crystal (PC), and Prism-coupling have been introduced to raise GH effect in
the terahertz region which is of most interest in sensing applications [21,
22, 23, 24, 25, 26, 27]. _

_Now, the full description of the optical conductivity of graphene in QHE
regime with optical excitation within the Landau levels (LLs) could be
determined by the Kubo conductivity model. This QHE for optical transitions in
single-layer graphene in the presence of a magnetostatic bias contributes as
longitudinal and Hall components in its conductivity tensor which yields a
Kerr effect rotation providing GH shifts of different polarization to the
incident linearly polarized light upon the reflection. Thus, this temperature-
dependent magneto-optical conductivity may produce GH effect which is large
enough to be suitable for practical THz applications._

_Also, the magneto-optical GH effect has been investigated in a prism-graphene
coupling system with a magneto-optical Kerr effect(MOKE) for the incident
polarized beam in Ref.[28]. The authors in this paper, based on the classic
model for the optical conductivity study the magneto-tunable enhanced GH
shifts of graphene in the polar Kerr effect (PMOKE) configuration for which
the magnetic field is perpendicularly applied on its surface. However, the
enhancement of GH effect in graphene in their report is limited to the Drude
model considering just the intra-band transitions. Now, in general, to study
QHE GH effect in a carbonic single-layer structure like graphene it is
essential to go beyond the semiclassical model and consider the full quantum
description of its surface conductivity. In this work, we prove the existence
of giant QHE GH shifts in a simple prism-graphene coupling device in QHE
regime. Light-matter interaction in graphene under the unconventional QHE
situation could bring giant GH shifts for different polarized light upon the
total reflection. Hence, these giant QHE phase jumps in the reflected light
for the introduced coupling structure could lead to dramatic improvement of
THz GH effect in graphene. _

_The outline of the paper is divided into the following sections: The
theoretical model and derivation of generalized Fresnel coefficients in QHE
regime are introduced in Section 2. We consider graphene in the quantum QHE
regime with optical transitions from LLs in Kubo conductivity model. In
Section 3 the numerical results and discussions are presented. The conclusion
remarks are also addressed in Section 4. _

##  2 Model and formula

_In this work, we present the full quantum description of GH effect in a
prism-graphene coupling system in QHE condition under the incident of $s$\-
and $p$-polarized light with the frequency $\omega$ as shown schematically in
Fig. 1. The dispersion of a linearly polarized beam passing through two
dielectric media separated by monolayer graphene could be obtained by
developing the components of the electric and magnetic vector of the incident,
transmitted, and reflected beam as [29]:_

$\displaystyle\left\\{\begin{array}[]{cc}E_{i}=(-a_{p}\cos\theta_{i},a_{s},a_{p}\sin\theta_{i})e^{i\tau_{i}}\\\
H_{i}Z_{0}=(-a_{s}n_{1}\cos\theta_{i},-a_{p}n_{1},a_{s}n_{1}\sin\theta_{i})e^{i\tau_{i}}\end{array}\right.$
(3)
$\displaystyle\left\\{\begin{array}[]{cc}E_{r}=(-r_{p}\cos\theta_{r},r_{s},r_{p}\sin\theta_{r})e^{i\tau_{r}}\\\
H_{r}Z_{0}=(-r_{s}n_{1}\cos\theta_{r},-r_{p}n_{1}e^{i\tau_{r}},r_{s}n_{1}\sin\theta_{r})e^{i\tau_{r}}\end{array}\right.$
(6)
$\displaystyle\left\\{\begin{array}[]{cc}E_{t}=(-t_{p}\cos\theta_{t},t_{s}e^{i\tau_{t}},t_{p}\sin\theta_{t})e^{i\tau_{t}}\\\
H_{t}Z_{0}=(-t_{s}n_{2}\cos\theta_{t},-t_{p}n_{2}e^{i\tau_{t}},t_{s}n_{2}\sin\theta_{t})e^{i\tau_{t}}\end{array}\right.$
(9)

_with $a$, $r$, and $t$ indicating the complex amplitudes of the incidence,
reflected, and transmitted light and $\tau_{m}=\omega
t-\textbf{k}_{m}.\textbf{{r}}$ ($m=i,r,t$). Then, the electric and magnetic
field components of the incident light at the interface, $z=0$, could be
related by following equations:_

$\displaystyle\left\\{\begin{array}[]{cc}E_{x}^{t}=E_{x}^{i}+E_{x}^{r}\ \ \ \
\ \ \ \ \ \ E_{y}^{t}=E_{y}^{i}+E_{y}^{r},\\\
H_{x}^{t}=H_{x}^{i}+H_{x}^{r}+J_{y},\ \ \ \ \ \ \ \ \ \
H_{y}^{t}=H_{y}^{i}+H_{y}^{r}-J_{x}\end{array}\right.$ (12)

_for which $J=\bar{\sigma}.E^{t}$ and $\bar{\sigma}$ are the surface current
density and the optical conductivity of graphene, respectively. To proceed, in
QHE condition, the surface conductivity of graphene develops a tensor which
could be written in the following matrix form:_

$\displaystyle\sigma=\begin{pmatrix}\sigma_{L}&\sigma_{H}\\\
-\sigma_{H}&\sigma_{L}\end{pmatrix}$ (13)

_As we use the quantum model for describing the optical transitions of LLs in
a prism-graphene coupling system, the frequency-dependent longitudinal (
$\sigma_{L}$) and Hall parts ($\sigma_{H}$) of its optical conductivity tensor
are [30]:_

$\begin{split}\sigma_{0}(\omega)=&\frac{e^{2}v_{F}^{2}|eB|\left(\hbar\omega+2i\Gamma\right)}{\pi
i}\times\\\
&\sum_{n=0}^{\infty}\left\\{\frac{\left[f_{d}(M_{n})-f_{d}(M_{n+1})\right]+\left[f_{d}(-M_{n+1})-f_{d}(-M_{n})\right]}{\left(M_{n+1}-M_{n}\right)^{3}-\left(\hbar\omega+2i\Gamma\right)^{2}\left(M_{n+1}-M_{n}\right)}\right\\}\\\
&+\left\\{\frac{\left[f_{d}(-M_{n})-f_{d}(M_{n+1})\right]+\left[f_{d}(-M_{n+1})-f_{d}(M_{n})\right]}{\left(M_{n+1}+M_{n}\right)^{3}-\left(\hbar\omega+2i\Gamma\right)^{2}\left(M_{n+1}+M_{n}\right)}\right\\}\end{split}$
(14)

_and:_

$\begin{split}&\sigma_{H}(\omega)=\frac{-e^{2}v_{F}^{2}eB}{\pi}\\\
&\sum_{n=0}^{\infty}\left\\{\left[f_{d}(M_{n})-f_{d}(M_{n+1})\right]-\left[f_{d}(-M_{n+1})-f_{d}(-M_{n})\right]\right\\}\times\\\
&\left\\{\frac{1}{\left(M_{n+1}-M_{n}\right)^{2}-\left(\hbar\omega+2i\Gamma\right)^{2}}+\frac{1}{\left(M_{n+1}+M_{n}\right)^{2}-\left(\hbar\omega+2i\Gamma\right)^{2}}\right\\}\end{split}$
(15)

_where $E_{n}=\pm M_{n}=\sqrt{2n|eB|\hbar v_{F}^{2}}$ determines LLs and the
scattering rate $\Gamma$ is assumed to be independent of the frequency of the
light. The distribution function is
$f_{d}(M_{n})=1/(1+exp[(M_{n}-\mu)/K_{B}T])$ with $e$, $\hbar$, $K_{B}$ and
$T$ representing the electron charge, reduced Planck constant, Boltzmann
constant and the temperature, respectively. In general, the existence of the
nonzero Hall term in the surface conductivity of graphene indicates that the
initial polarization of the incident light will not be preserved anymore for
the reflected and transmitted light. Thus, a p-polarized (s-polarized) light
could brings transmitted or reflected s-and p-polarized beam which could be
shown by subscripts $sp$ ($ss$) and $pp$ ($ps$). _

_Now, we are able to provide QHE description of the emergent GH effect from
reflected $ss$-, $sp$-, $ps$\- and $pp$-polarized light based on the Fresnel
equations for an incident linearly p- or s-polarized beam with the scattering
angle, $\theta_{1}$ and the photon energy $E_{ph}$ in the THz region. From
equations (1)-(5) one can show that the reflection coefficients of $ss$-,
$sp$-, $ps$\- and $pp$-polarized beam are:_

$\displaystyle\left\\{\begin{array}[]{cc}r_{ss}=-(1-\frac{2n_{1}f_{1}\cos\theta_{1}}{f_{1}f_{2}+z_{0}^{2}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}})a_{s},\\\
r_{sp}=-(\frac{2n_{1}z_{0}\sigma_{H}\cos\theta_{1}\cos\theta_{2}}{f_{1}f_{2}+z_{0}^{2}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}})a_{p},\\\
r_{pp}=(1-\frac{2n_{1}f_{2}\cos\theta_{2}}{f_{1}f_{2}+z_{0}^{2}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}})a_{p},\\\
r_{ps}=-(\frac{2n_{1}z_{0}\sigma_{H}\cos\theta_{1}\cos\theta_{2}}{f_{1}f_{2}+z_{0}^{2}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}})a_{s}\end{array}\right.$
(20)

_where $f_{1}$ and $f_{2}$ are defined as
$f_{1}=n_{1}\cos\theta_{2}+n_{2}\cos\theta_{1}+z_{0}\sigma_{L}\cos\theta_{1}\cos\theta_{2}$
and $f_{2}=n_{1}\cos\theta_{1}+n_{2}\cos\theta_{2}+z_{0}\sigma_{L}$. Here,
$z_{0}\approx 377\Omega$ is the vacuum impedance. Note that, $a_{s}$ and
$a_{p}$ are the amplitude of the electric vector of the incident field in the
perpendicular and parallel planes, respectively and the magnetic field is
applied along the $z$ direction (see Fig. 1). It is clear that for
$a_{s}=a_{p}=1$ one gets $r_{sp}=r_{ps}$ and in the case of normal incidence
$G_{1}=G_{2}$. Then, according to the stationary phase method, the amount of
GH shifts could be obtained from:_

$\displaystyle\Delta_{r_{ij}}=-\frac{\lambda}{2\pi}\frac{d\phi_{r_{ij}}}{d\theta}$
(21)

_where $\lambda=\frac{2\pi c}{\omega}$ is the wavelength of the incident beam
and $\phi_{r_{ij}}$ ($r_{ij}$), with $i$ and $j$ indicating p and s, is the
phases of the reflection coefficient ( reflection coefficient). At this point,
it should be emphasized that our model is based on putting a layer of graphene
on the prism in order to measure the GH shifts for the internal reflection
condition in QHE regime. It is due the ease of the detection of the beams
bringing the GH shift with high intensity and assuring that GH effect is not
affected by any dip in the reflection before total reflection. Interestingly
for lowest LL we have both electron and hole and therefore half-integer .
Equation (9) could be written in the following form:_

$\displaystyle\Delta_{r_{ij}}=-\frac{\lambda}{2\pi}\frac{1}{|r_{ij}|^{2}}\left(Re(r_{ij})\frac{dIm(r_{ij})}{d\theta}-Im(r_{ij})\frac{dRe(r_{ij})}{d\theta}\right)$
(22)

_Note that, it is obvious that one can have $R=|r_{ij}|^{2}$ equal to unity
when a beam of light hits an interface with indices of refraction
$n_{1}>n_{2}$ under an angle $\theta_{i}=\theta_{c}=\arcsin n_{2}/n_{1}$ at
which geometrical optics predicts the total reflection. In the calculation of
QHE GH shift, we treat the different components of the rotated polarized
reflected light separately and calculate their contributions to each of QHE GH
shifts. _

##  3 Results and discussion

_To satisfy the total internal reflection condition, we consider a prism with
the refractive index $n=1.5$ coupled to a graphene layer with the surface
optical conductivity tensor including nonzero Hall and longitudinal terms. In
fact, from equation 34 we see that what brings $sp$-polarized ($ps$-polarized)
light in the reflection spectra of the introduced structure is the existence
of a nonzero Hall term in the conductivity which is dependent on the energy of
the incident light, magnetic bias, chemical potential and the temperature. In
our calculations the temperature is considered to be set as very low
temperature $T=1\ K$ and also the room temperature $T=300\ K$ which is of most
interest in the real-world THz application of optical devices. Also, note that
in the classical model for GH effect in graphene we are not able to study the
shifts at very low temperatures for which the unconventional QHE is observed
[31]. _

_Fig. 2 (a-c) shows the dependence of the reflected beams versus the magnetic
field and the chemical potential with different polarizations for the prism-
graphene coupling device upon a specific incident angle for both incoming
$s$\- and $p$-polarized wave in the QHE situation. As it is clear, the total
internal reflection for $R_{ss}$ and $R_{pp}$ occurs at the scattering angle
$\theta=41.8104^{o}$. Interestingly, in this case, the reflection spectrum for
$R_{ps}=R_{sp}$ could be neglected. Furthermore, as is seen in Fig. 2 (d), at
$\theta=41.8104^{o}$, one could observe giant QHE GH shift of $ss$-polarized
wave for relatively high magnetic fields and the low temperature ($T=1\ K$)
which is larger than the GH peak of $sp$/$ps$-polarized reflected light.
Interestingly, Fig. 2 (e) shows a forbidden region for the presence of QHE GH
shifts in lower area for the magnetic field intensity and high values of the
chemical potential at $T=1\ K$. THe QHE GH spectrum for $pp$-polarized beam is
shown in Fig. 2 (e) which reveals different results in comparison to the other
polarized beam. _

_At very low temperature, $T=1\ K$, and for different photon energies Fig. 3
(a) reveals QHE GH shifts for $B=3.3\ T$ and $\mu=0.4\ eV$. It is observed
that by growing the photon energy QHE GH shifts are decreased for
$ss$-polarized light. This weak GH effect observed for stronger photon
energies might be explained as that for stronger energies the surface
conductivity of graphene shows smaller modulations in quantum regime. Note
that the maximum value of the GH shift for this spectrum occurs at $E_{ph}=1\
meV$ and $\theta=41.8104^{o}$. Fig. 3 (b) illustrates both positive and
negative QHE GH for $sp$ ($ps$) polarization of the reflected beam. We see
that the largest positive GH shift similar to $ss$-polarized reflected beam
appears at the same scattering angle $\theta=41.8104^{o}$. In addition, both
positive and negative GH shifts could be neglected when the photon energy
increases. However, in Fig. 3 (c), it is clear that the maximum amount of GH
effect for $pp$-polarized beam appears at $\theta=41.8104^{o}$. Interestingly,
the maximum value in this case shows to be almost independent of the photon
energy. It is because at very low temperatures emergent QHE GH shifts of
different frequencies show to be more localized in the frequency space._

_In Fig. 4 we take our attention toward the effect of increasing the magnetic
field on the GH effect for $\mu=0.4\ eV$ and $E_{ph}=1.5\ meV$. It is observed
from Fig. 4 (a) that the peak of the $GH$ shift spectrum for $ss$-polarized
light in the presence of an applied magnetic field appears at
$\theta=41.8102^{o}$. However, it is seen that the GH peak of
$sp$/$ps$-polarized light is much larger than the maximum of $ss$ polarized
beam occuring at $\theta=41.8104^{0}$. It is clear that the spectrum in this
case similar to the results of Fig. 4 (b), shows both positive and negative
QHE GH shifts. In Fig. 4 (c) the maximum amount of QHE shifts for
$pp$-polarized light waves are independent of the field intensity. _

_Note that, we neglect the effect of surface plasmon resonances (SPRs) which
could occur in the total reflection condition for the introduced coupling
structure. The reason is that SPRs decrease the amount of the reflected light
in this condition as an observed dip in the reflection spectrum. Therefore,
this dip in the reflection may result in observing larger GH shifts as it is
clear from equation (10). However, the presence of an SPR indicates a dip in
the reflection spectrum of the device weakening the reflected beam which could
cause problem in the experimental detection of GH shifts. Therefore, there
will be a trad-off between the enhancement of the GH shifts by exciting SPRs
and the intensity of the reflected light. Therefore, all the shift peaks are
induced by the total reflection of the incident linearly polarized beam at a
specific scattering angle._

_Fig. 5 shows the dependence of the QHE GH effect observed from $ss$-,
$sp/ps$\- and $pp$-polarized reflected beams on the intensity of the magnetic
field for the incident angle $\theta=48.8104^{o}$. The variation of the GH
effect spectrum is depicted in the field interval ranging from $1$ to $10\
(T)$ for different photon energy $E_{ph}$ (Fig. 5 (a-c)), chemical potential
($\mu$ Fig. 5 (d-f)) and temperature $T$ (Fig. 5 (g-i)). It is observed that
for $\mu=0.4\ eV$, $T=1\ K$ and $E_{ph}=1.5\ meV$ the GH effect emerges as
steps for stronger magnetic fields. This step-like feature of GH effect is due
to the observation of QHE for the conductance of graphene at applied strong
magnetic fields and low temperatures. Also, it is seen that the modulation of
GH shifts begin at a certain value for applied magnetic field which is
observed in the GH effect which is due to Pauli blocking. Interestingly, as it
is seen, at higher magnetic fields GH effect appears to be independent of the
frequency at specific scattering angle. Moreover, by increasing the value of
the chemical potential, as shown in Fig. 5 (d-f), QHE in prism-graphene
structure reveals stronger GH effect for different polarized beams. Here, we
see that strong QHE GH shift at low temperature, $T=1\ K$, can be observed for
higher potential in the case of applying stronger magnetic fields. However,
for lower field values as it is seen from the figure one observes that
increasing the chemical potential reveals weaker GH effect in graphene. We
emphasize that this behaviour is not observed in the classical model
considered to study GH effect in graphene. Additionally, as the temperature is
considered to be $T=300\ K$, the step-like behavior tends to be disappeared.
This expected behaviour of GH effect at higher temperatures which is shown in
Fig. 5 (g-i), reflects the distribution of Dirac electrons of graphene in LLs
levels. In fact, incrasing the temperature disturb the well separated LLs of
graphene. Superisingly, the amount of GH effect at the room temperature
remains almost the same relative to its low temperature values for $ss$,
$sp/ps$ and decreases for $pp$-polarized reflected light. This might be of
most interest in real-world sensing applications of GH effect-based optical
devices which are considered to operate at the room temperature. _

_Now, we examine the QHE lateral shifts for $ss$-, $sp/ps$\- and
$pp$-polarized beams in the photon energy interval ranging from $E_{ph}=1\
meV$ to $E_{ph}=10\ meV$ as shown in Fig. 6 for the fixed scattering angle
$\theta=48.8104^{o}$. In Fig. 6 (a-c), we have shown that by increasing the
photon energy, the value of QHE GH shift is decreased gradually. In Fig. 6
(d-f) the behaviour of QHE GH shifts are depicted for different chemical
potentials which show that one could gain the giant GH shift (1500) in lower
frequencies. In Fig. 6 (g-i), GH shifts are presented for two different
temperatures and fixed chemical potential. It is seen that the results at the
low and room temperature show the same GH effect for different polarized
reflected lights. _

_As we see relative to the results reported in the case of considering GH
effect for classical model of prism-graphene coupling which gives at most
shifts equal to $100$, one could obtain giant GH shifts near $1500$ for the
structure under QHE situation. Moreover, it is revealed that incident
$s$-polarized light shows much larger GH effect in quantum Hall model for the
introduced structure. The story behind this giant QHE GH effect is that the
optical conductivity of graphene under the influence of a normal magnetic bias
marks much larger values than its classical counterpart. Moreover, the
detection of individual quanta by GH effect in graphene requires quantum
methods to be employed in studying the sensing properties of this 2D carbonic
material. Such sensitivity is beyond the reach of any detection method which
employs a classical model. Therefore, tunable GH shifts in QHE regime could be
used for detection of low magnetic field intensity and also for THz
applications in graphene-based sensing devices._

_time._

##  4 Conclusion

_In this work, we prove the existence of an adjustable model for achieving
giant GH shifts from different polarized reflect light in a prism-graphene
coupling device under the QHE regime. We show that giant tunable GH shifts in
graphene could be induced upon the total reflection of the incident polarized
light waves at a specific scattering angle. The QHE GH shifts are studied by
deriving generalized Fresnel coefficients for the incident linearly polarized
light including an antisymmetric conductivity tensor realized by applying a
constant magnetic field on graphene’s surface. Significantly, GH shifts
undergo step-like changes at the low temperature and strong magnetic fields
which diminish at higher temperatures. Here, we notice that QHE in graphene
could be also observed at the room temperature[32]. As graphene is an one-
atom-thick 2D carbonic material quantum Hall GH effect could suggest very
sensitive tool in THz sensing applications. This is far beyond the reach of
any detection methods for which the classical models for studying GH effect in
graphene are introduced. In the end, we note that introduced Fresnel
reflection coefficients of the graphene-prism coupling structure in the
presence of an applied magnetostatic field is different from those suggested
in [33, 34]. Therefore, our numerical results for QHE GH effect are different
from results have been reported for GH shifts. _

##  5 Appendix: Fresnel reflection coefficients

_Here, we present a detailed calculation of the reflected spectrum for the
introduced structure and show that it could recover equation from the
following expression introduced in[33, 34]._

$\displaystyle
r_{ss}=-\frac{\alpha_{-}^{T}\alpha_{+}^{L}+\beta}{\alpha_{+}^{T}\alpha_{+}^{L}+\beta},\
\
r_{pp}=\frac{\alpha_{+}^{T}\alpha_{-}^{L}+\beta}{\alpha_{+}^{T}\alpha_{+}^{L}+\beta},\
\
r_{sp}=r_{ps}=-2\sqrt{\frac{\mu_{0}}{\epsilon_{0}}}\frac{k_{1z}k_{2z}\sigma_{H}}{\alpha_{+}^{T}\alpha_{+}^{L}+\beta}$
(23)

_where_

$\displaystyle\alpha_{\pm}^{L}=(k_{1z}\epsilon_{2}\pm
k_{2z}\epsilon_{1}+k_{1z}k_{2z}\frac{\sigma_{L}}{\epsilon_{0}\omega}),\ \
\alpha_{\pm}^{T}=(k_{2z}\pm k_{1z}+\mu_{0}\omega\sigma_{T}),\ \
\beta=\frac{\mu_{0}}{\epsilon_{0}}k_{1z}k_{2z}\sigma_{H}^{2}$ (24)

_Now by the use of relation $K_{iz}=\frac{\omega}{c}n_{i}\cos(\theta_{i})$ we
can write:_

$\displaystyle\alpha_{\pm}^{L}=\frac{\omega}{c}n_{1}n_{2}[n_{2}\cos\theta_{1}\pm
n_{1}\cos\theta_{2}+\frac{1}{c\epsilon_{0}}\sigma_{L}\cos\theta_{1}\cos\theta_{2}],\
\ \alpha_{\pm}^{T}=\frac{\omega}{c}[n_{2}\cos\theta_{2}\pm
n_{1}\cos\theta_{1}+\mu_{0}c\sigma_{T}],\ \ $ (25)

_and_

$\displaystyle\beta=\frac{\omega^{2}}{c^{2}}n_{1}n_{2}\frac{\mu_{0}}{\epsilon_{0}}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}$
(26)

_At this point one might recognize that:_

$\displaystyle\alpha_{-}^{L}=\alpha_{+}^{L}-2\frac{\omega}{c}n_{1}n_{2}n_{1}\cos\theta_{2},\
\ \ \ \alpha_{-}^{T}=\alpha_{+}^{T}-2\frac{\omega}{c}n_{1}\cos\theta_{1}$ (27)

_Then with the help of following relations for the impendance of free space
$z_{0}$:_

$\displaystyle
Z_{0}=\sqrt{\frac{\mu_{0}}{\epsilon_{0}}}=\mu_{0}c=\frac{1}{c\epsilon_{0}}$
(28)

_one could proceed one step forward and write:_

$\displaystyle\alpha_{+}^{L}=\frac{\omega}{c}n_{1}n_{2}f_{1},\ \ \
\alpha_{+}^{T}=\frac{\omega}{c}f_{2},\ \
\beta=\frac{\omega^{2}}{c^{2}}n_{1}n_{2}z_{0}^{2}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}$
(29)

_with the definitions:_

$\displaystyle
f_{1}=[n_{2}\cos\theta_{1}+n_{1}\cos\theta_{2}+z_{0}\sigma_{L}\cos\theta_{1}\cos\theta_{2}],\
\ f_{2}=[n_{2}\cos\theta_{2}+n_{1}\cos\theta_{1}+z_{0}\sigma_{T}]$ (30)

_In the end, by substituting equations (15) and (17) in (11) Fresnel
reflection coefficients of the graphene-prism coupling system in the presence
of a constant magnetic field applied on its surface is given by:_

$\displaystyle\left\\{\begin{array}[]{cc}r_{ss}=-(1-\frac{2n_{1}f_{1}\cos\theta_{1}}{f_{1}f_{2}+z_{0}^{2}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}}),\\\
r_{sp}=r_{ps}=-(\frac{2n_{1}z_{0}\sigma_{H}\cos\theta_{1}\cos\theta_{2}}{f_{1}f_{2}+z_{0}^{2}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}}),\\\
r_{pp}=(1-\frac{2n_{1}f_{2}\cos\theta_{2}}{f_{1}f_{2}+z_{0}^{2}\sigma_{H}^{2}\cos\theta_{1}\cos\theta_{2}})\end{array}\right.$
(34)

_which are almost the same as we have derived independently from the relations
(1)-(5). However, to be exactly recovered one instead requires to use the
following relations:_

$\displaystyle
r_{ss}=-\frac{\alpha_{-}^{L}\alpha_{+}^{L}+\beta}{\alpha_{+}^{L}\alpha_{+}^{L}+\beta},\
\
r_{pp}=\frac{\alpha_{+}^{L}\alpha_{-}^{L}+\beta}{\alpha_{+}^{L}\alpha_{+}^{L}+\beta},\
\
r_{sp}=r_{ps}=-2\sqrt{\frac{\mu_{0}}{\epsilon_{0}}}\frac{k_{1z}k_{2z}\sigma_{H}}{\alpha_{+}^{L}\alpha_{+}^{L}+\beta}$
(35)

_with_

$\displaystyle
f_{1}=[n_{2}\cos\theta_{1}+n_{1}\cos\theta_{2}+z_{0}\sigma_{L}\cos\theta_{1}\cos\theta_{2}],\
\ f_{2}=[n_{2}\cos\theta_{2}+n_{1}\cos\theta_{1}+z_{0}\sigma_{L}]$ (36)

##  6 Data availability

Data sharing does not apply to this article as no new data were created or
analyzed in this study.

##  7 Acknowledgment

A. Alidoust Ghatar is an invited researcher by D. Jahani

## References

  * [1] J. Picht, Ann. Phys. (Paris) 3, 433 (1929).
  * [2] F. Goos, and H. Hänchen, (1947). Ein neuer und fundamentaler Versuch zur Totalreflexion. Annalen der Physik, 436(7‐8), 333-346.
  * [3] F. Goos, and H. Lindberg-Hänchen, (1949). Neumessung des strahlversetzungseffektes bei totalreflexion. Annalen der Physik, 440(3), 251-252.
  * [4] H. K. V. Lotsch, Optik 32, 116 (1970); 32, 189 (1970); 32, 299 (1971); 32, 553 (1971).
  * [5] S. Hayashi, D. V. Nesterenko, and Z. Sekkat, (2015). Fano resonance and plasmon-induced transparency in waveguide-coupled surface plasmon resonance sensors. Applied Physics Express, 8(2), 022201.
  * [6] Z. Salamon, H. A. Macleod, and G. Tollin, (1997). Coupled plasmon-waveguide resonators: a new spectroscopic tool for probing proteolipid film structure and properties. Biophysical journal, 73(5), 2791-2797.
  * [7] Q. You, Y. Shan, S. Gan, Y. Zhao, X. Dai, and Y. Xiang, (2018). Giant and controllable Goos-Hänchen shifts based on surface plasmon resonance with graphene-MoS 2 heterostructure. Optical Materials Express, 8(10), 3036-3048.
  * [8] R. Briers, O. Leroy, and G. Shkerdin, (2000). Bounded beam interaction with thin inclusions. Characterization by phase differences at Rayleigh angle incidence. The Journal of the Acoustical Society of America, 108(4), 1622-1630.
  * [9] L. G. Wang, M. Ikram, and M. S. Zubairy, (2008). Control of the Goos-Hänchen shift of a light beam via a coherent driving field. Physical Review A, 77(2), 023811.
  * [10] V. O. de Haan, J. Plomp, T. M. Rekveldt, W. H. Kraan, A. A. van Well, R. M. Dalgliesh, and S. Langridge, (2010). Observation of the Goos-Hänchen shift with neutrons. Physical review letters, 104(1), 010401.
  * [11] V. K. Ignatovich, (2004). Neutron reflection from condensed matter, the Goos–Hänchen effect and coherence. Physics Letters A, 322(1-2), 36-46.
  * [12] D. Felbacq, A. Moreau, and R. Smaali, (2003). Goos-Hänchen effect in the gaps of photonic crystals. Optics letters, 28(18), 1633-1635.
  * [13] L. G. Wang, and S. Y. Zhu, (2006). Giant lateral shift of a light beam at the defect mode in one-dimensional photonic crystals. Optics letters, 31(1), 101-103.
  * [14] Y. Yan, X. Chen, and C. F. Li, (2007). Large and negative lateral displacement in an active dielectric slab configuration. Physics Letters A, 361(1-2), 178-181.
  * [15] P. Hou, Y. Chen, X. Chen, J. Shi, and Q. Wang, (2007). Giant bistable shifts for one-dimensional nonlinear photonic crystals. Physical Review A, 75(4), 045802.
  * [16] W. Kong, Y., Sun, and Y. Lu, (2020). Enhanced Goos-Hänchen shift of graphene coated on one-dimensional photonic crystal. Results in Physics, 17, 103107.
  * [17] L. G. Wang, H. Chen, and S. Y. Zhu, (2005). Large negative Goos–Hänchen shift from a weakly absorbing dielectric slab. Optics letters, 30(21), 2936-2938.
  * [18] A. C. Neto, F. Guinea, N.M. Peres, K.S. Novoselov, A.K. Geim, The electronic properties of graphene, Rev. Modern Phys. 81 (1) (2009) 109
  * [19] M. J. Allen, V. C. Tung, and R. B. Kaner, (2010). Honeycomb carbon: a review of graphene. Chemical reviews, 110(1), 132-145.
  * [20] A. K. Geim, and K. S. Novoselov, (2010). The rise of graphene. In Nanoscience and technology: a collection of reviews from nature journals (pp. 11-19).
  * [21] X. Li, P. Wang, F. Xing, X. D. Chen, Z. B. Liu and J. G. Tian, (2014). Experimental observation of a giant Goos–Hänchen shift in graphene using a beam splitter scanning method. Optics letters, 39(19), 5574-5577.
  * [22] Q. Li, B. Zhang, and J. Shen, (2013). Goos-Hänchen shifts of reflected terahertz wave on a COC-air interface. Optics Express, 21(5), 6480-6487.
  * [23] M. Cheng, P. Fu, X. Chen, X. Zeng, S. Feng, and R. Chen, (2014). Giant and tunable Goos–Hanchen shifts for attenuated total reflection structure containing graphene. JOSA B, 31(10), 2325-2329.
  * [24] L. Jiu-Sheng, W. Jing-Fang, and Z. Le, (2014). Giant tunable Goos–Hänchen shifts based on prism/graphene structure in terahertz wave region. IEEE Photonics Journal, 6(6), 1-7.
  * [25] S. Grosche, M. Ornigotti, and A. Szameit, (2015). Goos-Hänchen and Imbert-Fedorov shifts for Gaussian beams impinging on graphene-coated surfaces. Optics express, 23(23), 30195-30203.
  * [26] C. W. J. Beenakker, R. A. Sepkhanov, A. R. Akhmerov, and J. Tworzydło, (2009). Quantum Goos-Hänchen effect in graphene. Physical Review Letters, 102(14), 146804.
  * [27] J. Tang, J. Xu, Z. Zheng, H. Dong, J. Dong, S. Qian, J. Guo, L. Jiang, and Y. Xiang, (2019). Graphene Tamm plasmon-induced giant Goos–Hänchen shift at terahertz frequencies. Chinese Optics Letters, 17(2), 020007.
  * [28] T. Tang, J. Li, M. Zhu, L. Luo, J. Yao, N. Li, and P. Zhang, (2018). Realization of tunable Goos-Hanchen effect with magneto-optical effect in graphene. Carbon, 135, 29-34
  * [29] M. Born and E. Wolf, Principles of Optics, 6th ed. (Cambridge University Press, Cambridge, 1980).
  * [30] V. P. Gusynin, S. G., Sharapov, and J. P. Carbotte, (2006). Magneto-optical conductivity in graphene. Journal of Physics: Condensed Matter, 19(2), 026222
  * [31] K. S. Novoselov, E. McCann, S. V. Morozov, V. I. Fal’ko, M. I. Katsnelson, U. Zeitler, D. Jiang, F. Schedin and A. K. Geim, (2006). Unconventional quantum Hall effect and Berry’s phase of $2\pi$ in bilayer graphene. Nature physics 2.3 (2006): 177-180.
  * [32] K. S. Novoselovz, Y. Jiang, Y. Zhang, S. V. Morozov, H. L. Stormer, U. Zeitler, J. C. Maan, G. S. Boebinger, P. Kim and A. K. Geim, (2007). Room-temperature quantum Hall effect in graphene. Science 315.5817: 1379-1379.
  * [33] W. Wu, S. Chen, C. Mi, W. Zhang, H. Luo and Sh. Wen, (2017).Giant quantized Goos-Hänchen effect on the surface of graphene in the quantum Hall regime. Physical Review A 96.4 (2017): 043814.
  * [34] M. Shah, A. Akbar, N. A. Khan, Q. Zaman, S. Iqbal, W. Ali, M. Javed and Muzamil Shah, (2022).Quantization of Goos–Hänchen shift in monolayer graphene under partial and total internal reflection conditions.” JOSA B 39.4 (2022): 1082-1090.

Figure 1: (a) Schematic representation of the GH shift of the designed
structure in the presence of a prism with the refractive index of $n=1.5$ and
a graphene layer In QHE regime. (b) Schematic view of the scattering of an
incident lineally polarized light between two media with refractive indices
$n_{1}$ and $n_{2}$ separated by a graphene layer under an applied magnetic
field $B$. (A colour version of this figure can be viewed online.) Figure 2:
The QHE GH shifts of $ss$-, $ps$/$sp$\- and $pp$-polarized light for the
magnetic field interval $B=1-45\ T$ in the case of three different values of
the chemical potential with the photon energy $E_{ph}=1.5\ meV$. (A colour
version of this figure can be viewed online.) Figure 3: The QHE GH effect
versus with different photon energies and scattering angles at $T=1\ K$ for
$\mu=0.4$ and $B=3.3\ T$. (A colour version of this figure can be viewed
online.)  Figure 4: Magneto-optic modulation of GH effect in the prism-
graphene coupling structure for different values of the scattering angle. (A
colour version of this figure can be viewed online.) Figure 5: Modulation of
QHE GH shifts versus the magnetic field for: (a-c) different photon energies
(d-f) different chemical potentials; (g-i) different scattering angles. (A
colour version of this figure can be viewed online.) Figure 6:  Modulation of
QHE GH shifts versus the photon energy for: (a-c) different magnetic fields
(d-f) different chemical potentials; (g-i) two different temperatures. (A
colour version of this figure can be viewed online.)