\documentclass[jair,11pt]{article}

\usepackage{jair}
\usepackage{psfig}
\usepackage{amssymb}
\usepackage{theapa}

\newtheorem{defin}{Definition}
\newtheorem{prop}{Proposition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{example}{Example}

\def\defines{\sqsubseteq_{\Sigma}}

\newcommand{\Omit} [1] {} % pour supprimer les phrases entre les {}

\def\leadsto{\mapsto}
\def\Box{B}
\def\Diamond{D}
\def\happy2p{$\Pi_2^p$}
\def\asigma2p{$\Sigma_2^p$}
\def\2qbfbarre{2-${\overline{\mbox{\sc qbf}}}$}
\def\deuxqbf{2-{\sc qbf} }
\def\np{{\sf NP}}
\def\conp{{\sf coNP}}
\def\bh2{$\mbox{{\sf BH}}_2$}
\def\cobh2{$\mbox{{\sf coBH}}_2$}
\def\defines{\sqsubseteq_{\Sigma}}
\def\endproof{$\diamond$}
\def\iff{if and only if }

\def\blacksquare{\diamond}

\def\qed{\hfill {\scriptsize{$\blacksquare$}}\break}

\long\def\eatpar#1{%
\ifx#1\par                      % se il token e' \par
\let\nextmove=\eatpar           % rimetti \eatpar in coda
\else
\let\nextmove=#1%               altrimenti, rimetti il token in coda
\fi
\noexpand\nextmove%             il token o \eatpar viene rimesso in coda
}

\jairheading{18}{2003}{391-443}{5/02}{5/03}
\ShortHeadings{Propositional Independence}
{Lang, Liberatore, \& Marquis}
\firstpageno{391}

\title{Propositional Independence:\\
Formula-Variable Independence and Forgetting
}


\author{%
\name J\'er\^ome Lang \email lang@irit.fr \\
\addr IRIT-UPS, 118 route de Narbonne \\
31062 Toulouse Cedex, France\\
\name Paolo Liberatore \email liberato@dis.uniroma1.it \\
\addr Dipartimento di Informatica e Sistemistica\\
Universit\`a di Roma ``La Sapienza''\\
via Salaria 113, 00198 Roma, Italy \\
\name Pierre Marquis \email marquis@cril.univ-artois.fr \\
\addr CRIL-CNRS/Universit\'e d'Artois\\
rue de l'Universit\'e\\
S.P. 16, 62307 Lens Cedex, France
}

\begin{document}

\maketitle

\begin{abstract}
 
Independence -- the study of what is relevant to
a given problem of reasoning -- has received an
increasing attention from the AI community. In
this paper, we consider two basic forms of independence,
namely, a syntactic one and a semantic one. We show
features and drawbacks of them. In particular, while
the syntactic form of independence is computationally
easy to check, there are cases in which things that
intuitively are not relevant are not recognized as
such. We also consider the problem of forgetting, i.e., distilling from
a knowledge base only the part that is relevant to
the set of queries constructed from a subset of the
alphabet. While such process is
computationally hard, it allows for a simplification
of subsequent reasoning, and can thus be viewed as
a form of compilation: once the relevant part of
a knowledge base has been extracted, all reasoning
tasks to be performed can be simplified.

\end{abstract}

\section{Introduction}\label{intro}
We successively present some motivations, the scope of the paper,
and the contribution and the organization of the paper.

\subsection{Motivations}

In many situations of everyday life, we are confronted with the problem of 
{\it determining what is relevant}. Especially, as a preliminary step to various 
intelligent tasks (e.g., planning, decision making, reasoning), it is 
natural and reasonable to discard everything but what is relevant to achieve 
them efficiently. For instance, before starting to write this paper, we had 
to consider the relevant literature on the topic, and only it; gathering on 
our desks all the papers about relevance that we have at hand led us to set 
away our favourite cook books, because they are of no help to the task of writing 
this paper. The ability to focus on what is relevant (or dually to discard 
what is not) can be considered as a central, characteristic feature of 
intelligence; it is believed that over 90\% of the neuronal connections of 
our brains are inhibitory and serve to give up sensorial inputs 
\cite{artint97}. This explains why irrelevance, under various names as 
independence, irredundancy, influenceability, novelty, separability, is 
nowadays considered as an important notion in many fields of artificial 
intelligence (see a survey for more details, \citeR<e.g.,>{GreinerSubramanian95,artint97}). 

In the following, we are concerned with {\em relevance for 
reasoning}. In this framework, the task is typically that of
determining whether some piece of knowledge (a query) $\varphi$ can be derived 
from a knowledge base $\Sigma$. Several reasoning schemes can be taken into 
account here, from the classical one (inference is classical entailment) to 
more sophisticated ones (common-sense inference). When dealing with such 
reasoning tasks, relevance is often exploited so as to make inference more 
efficient from a computational point of view. In other reasoning problems, 
the purpose is to explicitly derive some intensionally-characterized pieces 
of knowledge (e.g., tell me all what you know about Tweety). For such 
problems (that are not reducible to decision problems), relevance also has a 
role to play, for instance by allowing us to characterize the pieces of
information we are interested in by forgetting the other ones. 

To what extent is the goal of improving inference 
reachable? In order to address this point, a key issue is the {\em computational 
complexity} one. Indeed, assume that we know that the resolution of some 
reasoning problems can be sped up once relevant information has been 
elicited. In the situation where it is computationally harder to point out 
such information from the input than to reason directly from the input, 
computational benefits are hard to be expected. If so, alternative uses of 
relevance for reasoning are to be investigated. For instance, searching for 
relevance information can be limited by considering only pieces of knowledge 
that can be generated in a tractable way. If such information 
depend only on the knowledge base, another possible approach is to 
(tentatively) compensate the computational resources spent in deriving the 
relevance information through many queries (computing pieces of relevant 
information can then be viewed as a form of compilation). 

\subsection{Scope of the Paper}\label{scope}

Little is known about the computational complexity of relevance. This paper 
contributes to fill this gap. The complexity of several logic-based 
relevance relations is identified in a propositional setting. By logic-based 
we mean that the notions of relevance we focus on are not extra-logical but 
built inside the logic: they are defined using the standard logical notions 
of (classical) formula, model, logical deduction, etc. 
The stress is laid on notions 
of relevance that can prove helpful for improving inference and, in 
particular, the most basic form of it, classical entailment. Relevance is 
captured by relations in the metalanguage of the logic, that is, we 
formalize relevance as a relation between objects of the propositional 
language (formulas or sets of literals/variables) thus expressing the fact 
that some object is relevant to some other one.

\iffalse Arguments of such relations are propositional formulas, encoding 
knowledge bases and pieces of knowledge (including queries), and sets of 
propositional variables or literals that represent, for instance, subject 
matters or topics of interest. \fi

Two notions play a central role in this paper.
The first one, {\em (semantical) formula-variable independence}
(FV-independence
for short) tells that a propositional formula $\Sigma$ is independent from a given set $V$ of 
variables if and only if it can be rewritten equivalently as a formula in 
which none of the variables in $V$ appears.
The second one is the notion of {\em forgetting a given set $V$ of variables in 
a formula $\Sigma$}. It is
intimately linked to the notion of formula-variable independence because, 
as we show,
the result of forgetting the set of variables $V$ in a formula $\Sigma$ can be 
defined as the strongest consequence of $\Sigma$ being independent from $V$.
% (3) why they are useful in AI
Both notions have appeared in the literature under various names and with 
several different
(but equivalent) definitions, and are highly useful for many tasks in 
automated reasoning
and many problems in artificial intelligence:


\begin{enumerate}

\item {\em automated deduction and consequence finding}. 
Formula-variable independence can be useful for 
checking (un)satisfiability or for consequence finding. Indeed, structuring 
the knowledge base by finding useful independencies may be worth doing before 
running any search algorithm. This principle is at work in
\cite{AmirMcIlraith00}. In optimal cases, for example, a satisfiability 
problem will be decomposed into a small number of satisfiability problems on 
easier knowledge bases (with less variables) as shown by \citeA{ParkVanGelder96}. 
As to improving inference, this can be particularly helpful in the situation 
where the set of queries under consideration is limited to formulas $\varphi$ 
that are (syntactically or semantically) independent from a set $V$ of 
variables. 

\item {\em query answering} (see in particular \citeR{AmirMcIlraith00}), 
{\em diagnosis} (see the work by \citeR{Darwiche98}). 
Rendering a formula $\Sigma$ independent from a set $V$ of variables
through variable forgetting gives rise to a 
formula that is query-equivalent to $\Sigma$ w.r.t. $V$ in the sense that 
every logical consequence $\varphi$ of $\Sigma$ that is independent from $V$ 
also is a logical consequence of $\Sigma$ once made independent from $V$, 
and the converse holds as well. Interestingly, the set of all the formulas 
independent from a set of variables is a stable production field 
\cite{Siegel87,Inoue92}, and focusing on such a production field is 
valuable for several reasoning schemes.
For instance, in the consistency-based framework for diagnosis 
\cite{Reiter87}, the queries we are interested in are the conflicts of the
 system to be diagnosed, i.e., the 
clauses that are independent from every variable used to represent the 
system, except the abnormality propositions used to encode the component
failures.

\item {\em knowledge base structuring}, {\em topic-based reasoning}. 
Formula-variable independence is a key notion for decomposing a 
propositional knowledge base (KB for short), i.e., a finite set of propositional 
formulas, into smaller subbases. Such a decomposition is 
all the more valuable as the number of variables the subbases depends on is 
low. Optimally, a knowledge base $\Sigma = \{\varphi_1, ..., \varphi_n\}$ is 
fully decomposable if it can be written as $\Sigma = \Sigma_1 \cup \ \ldots 
\ \cup \Sigma_n$ where
$\Sigma_i$ and $\Sigma_j$ depend on disjoint sets of variables
for all $i \neq j$. Such 
decompositions were considered in several papers \cite{Parikh96,AmirMcIlraith00,MarquisPorquet00} with 
somewhat different motivations. The most intuitive motivation for searching 
such decompositions is that it gives a better understanding of the knowledge 
base, by structuring it with respect to (possible disjoint but not 
necessarily) sets of topics \cite{MarquisPorquet00}.

\item {\em belief revision and inconsistency-tolerant reasoning}. 
Decomposing a propositional knowledge base $\Sigma$ into subbases 
$\{\Sigma_1, \ldots, \Sigma_n\}$ proves also to be relevant for defining 
inconsistency-tolerant relations as well as belief revision operators. The 
approach proposed by \citeA{ChopraParikh99} proceeds as follows: the 
knowledge base $\Sigma$ is first partitioned into $\{\Sigma_1, 
\ldots, \Sigma_n\}$ such that the intersection of the languages of the 
subbases (i.e., the sets $DepVar(\Sigma_i)$ of variables the subbases depend on) 
are as small as possible; then $\varphi$ is inferred from $\Sigma$ 
w.r.t. the given partition if and only if the 
conjunction of all $\Sigma_i$ such that $DepVar(\Sigma_i) \cap 
DepVar(\varphi) \neq \emptyset$ is consistent and entails $\varphi$. 
In a revision situation, this approach also 
ensures that the only old beliefs that may be thrown away are about the 
variables relevant to the input formula. Finally, as
recently shown by some of the authors of the present paper,
forgetting can be advantageously
exploited as a weakening mechanism for recovering consistency from
an inconsistent KB \cite{LangMarquis02}.

\item {\em belief update}. A belief update operator maps a knowledge base 
$\Sigma$ and an input formula $\varphi$ expressing some explicit evolution of the 
world to a new knowledge base $\Sigma \diamond \varphi$; $\Sigma$ and $\Sigma \diamond \varphi$ 
respectively represent the agent's knowledge {\em before} and {\em after} 
the evolution of the world expressed by the update. Several authors argued 
that an update operator should preserve the part of the knowledge base not 
concerned by the update. This leads to the following three-stage process, 
proposed independently by \citeA{Dohertyetal98} and by
\citeA{HerzigRifi98} (and named {\sc mpma} and {\sc 
wss}$\downarrow$, respectively):
(i) determine the variables relevant to the update, 
namely, $DepVar(\varphi)$; (ii) forget these variables in $\Sigma$ to obtain
a new formula $ForgetVar(\Sigma, DepVar(\varphi))$; (iii) expand by 
$\varphi$. In more compact terms, this update operator is expressed by $\Sigma
\diamond \varphi = ForgetVar(\Sigma,DepVar(\varphi))\wedge \varphi$. 
Thus, both our results on FV-independence and variable forgetting are 
relevant to the computational 
issues pertaining to this kind of belief updates.

\item {\em reasoning about action, decision making, planning}. Logical 
languages for reasoning about action express the effects (deterministic or 
not, conditional or not) of actions by means of propositional formulas
\cite{GelfondLifschitz93,Sandewall95,Fargieretal00,HerzigLangMarquisPolacsek01}; finding the variables the effects are 
dependent on enables to identify the variables whose truth value may be 
changed by the action; moreover, formula-literal independence -- a refinement
of FV-independence that we introduce -- also tells us 
in which direction (from false to true and/or from true to false) the 
possible change may occur. This is especially useful for filtering out 
irrelevant actions in a decision making or planning problem.

\item {\em preference representation}. 
Logical languages for representing preference write elementary
goals as propositional formulas and it is crucial to identify those
variables that have no influence on the agent's preference.
Therefore, formula-variable independence has an important
role to play; for instance, the framework of so-called {\em ceteris paribus}
preference statements of \citeA{TanPearl94} interprets a preference
item $\varphi : \psi > \neg \psi$ by: for any pair of worlds $(\omega,\omega')$ 
such that (i) $\omega \models \psi$,  (ii) $\omega' \models \neg \psi$ and 
(iii) $\omega$ and $\omega'$ coincide on all variables 
{\em $\varphi$ and $\psi$ are independent from}, then we have a strict preference
of $\omega$ over $\omega'$.

\end{enumerate}

\subsection{Contribution and Organization of the Paper} 

The rest of the paper is structured as follows. After some formal preliminaries given
in Section \ref{preli}, the key notion of 
formula-variable independence is presented in Section \ref{fvindep}.
Because it captures a very basic form of logic-based independence, this 
relation has already been introduced in the literature under several names, 
like influenceability \cite{Boutilier94}, relevance to a subject matter 
\cite{Lakemeyer97}, or redundancy \cite{Dohertyetal98}.  Although it is 
conceptually and technically simple, this notion has not been studied in a 
systematic way, and our very first contribution aims at filling this gap, 
first by giving several equivalent characterizations of this notion
(this is useful, as several papers introduced and used the
same concepts under different names),
\iffalse(which 
is all the more useful that the definition of this notion in various papers 
in the literature alternatively makes use of any of them)\fi and second by 
investigating carefully its computational complexity. In particular, we show 
that,  in the general case,  checking whether a formula is independent from 
a set of variables is {\sf coNP}-complete.
Then, we go beyond this very simple notion by introducing the more 
fine-grained notion of {\em formula/literal independence} in order to 
discriminate the situation where a formula $\Sigma$ conveys some information 
about a literal but no information about its negation. 
This refinement is helpful whenever the polarity of information is significant,
which is the case in many AI fields (including closed-world reasoning and
reasoning about actions).
We also study several 
interesting notions derived from formula-variable and formula-literal 
independence, such as the notion of {\em simplified formula} ($\Sigma$ is 
Lit- (Var-) simplified if it depends on every literal (variable) occurring 
in it) and the corresponding process of simplifying a formula.
Despite this complexity and because the size of a simplified formula can 
never be larger than the size of the original formula, simplification can 
prove a valuable relevance-based preprocessing for improving many forms of 
inference.


In Section \ref{forg}, we turn to the second key notion, namely {\em 
forgetting a given set of variables in a formula} \cite{LinReiter94}. 
The forgetting process plays an important role in many AI tasks and has been studied in the 
literature under various other names, such as variable elimination, 
or marginalization \cite{Kohlasetal99}.
Several semantical characterizations and metatheoretic properties 
of forgetting are presented. Based on this notion, we introduce an additional notion of 
dependence between two formulas given a set of variables: we state that 
$\Sigma$ is equivalent to $\Phi$ w.r.t. $V$ if and only if both formulas are 
logically equivalent once made independent from every variable except those 
of $V$. Here again, it is important to make a distinction 
between a variable and its negation (for instance, one can be interested in 
the positive conflicts of a system, only). For this purpose, we introduce a 
notion of literal forgetting that refines the corresponding notion of 
variable forgetting. We show how closed-world inference can be simply 
characterized from the corresponding equivalence relation. Finally, we 
identify the complexity of both notions of equivalence and show them to be 
hard ($\Pi_2^p$-complete). As a consequence, forgetting variables or 
literals within a formula cannot be achieved in polynomial time in the 
general case (unless the polynomial hierarchy collapses at the first level). 
We also show that a polysize propositional representation of forgetting is 
very unlikely to exist in the general case. We nevertheless present some 
restricted situations where forgetting is tractable.


Section \ref{other} shows FV-independence closely related to notions of irrelevance
already introduced in the literature by various authors.
Section \ref{related} discusses other related work and sketches further extensions
of some notions and results studied in the paper. Finally, Section \ref{concl} 
concludes the paper. Proofs of the main propositions are reported in an
appendix.
A glossary of the notations is at the end of this paper, right
before the bibliography.


\iffalse In a second part, we consider conditional independence, introduced 
as a logical counterpart to probabilistic independence in \cite{Darwiche97}. 
Two sets of variables $X$ and $Y$ are conditionally independent given a set 
of variables $Z$ and a formula $\Sigma$ if and only if whichever full 
information about $Z$ we consider, the addition of information about $X$ in 
$\Sigma$ does not enable telling anything new about $X$. Several 
applications of this form of irrelevance to reasoning (including deduction, 
abduction and diagnosis) have been pointed out so far. We present a 
probabilistic characterization of conditional independence, and focus on its 
complexity and the complexity of several of its restrictions. It varies from 
{\sf coNP}-complete in some restricted cases, to $\Pi_2^p$-complete in the 
general case. We also introduce two restrictions of conditional 
independence, namely strong conditional independence and perfect conditional 
independence. For these two restrictions, conjunctive information (resp. any 
information) about $Z$ is acceptable. We show that strong conditional 
independence can be used to capture formula/variable independence and 
vice-versa (but not via a polynomial reduction). It also has interesting 
connections with abduction and some other forms of irrelevance intoduced in 
the literature (especially, the notion of irrelevance between two subject 
matters relative to a knowledge base \cite{Lakemeyer97}). We present several 
semantical characterizations for both strong and perfect conditional 
independence and some of their metatheoretic properties. Especially, we 
confront both notions of conditional independence againts the semi-graphoid 
axioms, which are considered reasonable postulates for conditional 
independence relations. We also identify their complexity in the general 
case and in some restricted ones (for the strong form). In a third part, we 
successively consider several forms of (ir)relevance already pointed out so 
far: influenceability \cite{Boutilier94}, relevance under various forms 
\cite{Lakemeyer97} (relevance to a subject matter, strict relevance, 
explanatory relevance, relevance between two subject matters), novelty under 
various forms \cite{GreinerGenesereth83} \cite{Marquis91} (positive and 
negative, novelty-based independence), separability \cite{Levesque98}, 
causal independence \cite{DarwichePearl94}. All these notions can be used to 
enhance reasoning in various contexts. We identify the complexity of 
deciding all these forms of independence.
\fi

\section{Preliminaries}\label{preli}

We first recall some basic notions from propositional logic, and
from complexity theory.

\subsection{Propositional Logic}\label{prelipl}

Let $PS$ be a finite set of propositional variables. $PROP_{PS}$ is the
propositional language built up from $PS$, the connectives and the Boolean
constants $true$ and $false$ in the usual way. For every $V \subseteq PS$,
$PROP_V$ denotes the sublanguage of $PROP_{PS}$ generated from the variables of
$V$ only. A {\em literal} of $PROP_V$ is either a variable of $V$ (positive
literal) or the negation of a variable of $V$ (negative literal).  Their set is
denoted $L_V$, while $L_V^+$ (resp. $L_V^-$) denotes the set of positive (resp.
negative) literals built up from $V$. A clause $\delta$ (resp.\ a term
$\gamma$) of $PROP_V$ is a (possibly empty) finite disjunction (resp.\
conjunction) of literals of $PROP_V$. A CNF (resp.\  a DNF) formula of $PROP_V$
is a finite conjunction of clauses (resp.\  disjunction of terms) of $PROP_V$.  As
usual, every finite set of formulas from $PROP_{PS}$ is identified with the
formula that is the conjunction of its elements.

From now on, $\Sigma$ denotes a propositional formula, i.e., 
a member of $PROP_{PS}$. $Var(\Sigma)$ is the set of propositional variables appearing in
$\Sigma$. 
If $L \subseteq L_{PS}$, $Var(L)$ is the set of variables from $PS$
upon which literals of $L$ are built.
Elements of $PS$ are denoted $v$, $x$, $y$ etc. 
Elements of $L_{PS}$ are denoted $l$, $l_1$, $l_2$ etc.
Subsets of $PS$ are denoted $V$, $X$, $Y$ etc.  In order to simplify notations, we assimilate every
singleton $V = \{v\}$ with its unique element $v$. The {\em size} of 
a formula $\Sigma$, denoted by $|\Sigma|$, is the number of
occurrences of variables it contains. 
A propositional formula $\Sigma$ is said to be in Negation Normal Form (NNF) if and only if 
only propositional symbols are in the scope of an occurrence of $\neg$ in $\Sigma$.
It is well-known that every propositional formula $\Sigma$ built up from the connectives $\wedge$, 
$\vee$, $\neg$, $\Rightarrow$ only, can be turned in linear time
into an equivalent NNF formula by ``pushing down'' every  occurrence of $\neg$ in it
(i.e., exploiting De Morgan's law) and removing double negations (since $\neg$
is involutive). Slightly abusing words, we call the formula resulting from this normalization
process {\em the NNF} of $\Sigma$ and we note $Lit(\Sigma)$ the set of literals from $L_{PS}$
occurring in the NNF of $\Sigma$. For instance, the NNF of 
$\Sigma = \neg ((\neg a \wedge b) \vee c)$ is
$(a \vee \neg b) \wedge \neg c$; hence, we have
$Lit(\Sigma) = \{a, \neg b, \neg c\}$. Note that the NNF of
a formula depends on its syntactical structure, i.e., two
formulae that are synctatically different may have different
NNFs even if they are equivalent.

Full instantiations of variables of $V \subseteq PS$ are called 
$V$-{\em worlds}%
\footnote{The $V$-worlds are also called partial models over $V$.};
they are denoted by $\omega_V$ and their set is denoted 
$\Omega_V$. When $A$ and $B$ are two disjoint subsets of $PS$, 
$\omega_A \wedge \omega_B$ denotes the $A \cup B$-world
that coincides with $\omega_A$ on $A$ and with $\omega_B$ on $B$. An
interpretation $\omega$ over $PROP_{PS}$ is just a $PS$-world, 
and $\omega$ is said to be a model of $\Sigma$ whenever it makes $\Sigma$ true.
\iffalse
Given a set of models $S$, we denote
$for(S)$ a formula that has $S$ as a set of models. Of course, there are many
equivalent formulas having $S$ as models, but $for$ will be used only when this
does not matter. When $S = \{\omega\}$, i.e.,\  $S$ is composed of a single
model, we write $for(\omega)$ instead of $for(\{\omega\})$. Conversely,
\fi
We denote $Mod(\Sigma)$ the set of models of $\Sigma$.

For every formula $\Sigma$ and every variable $x$, $\Sigma_{x \leftarrow 0}$
(resp.\ $\Sigma_{x \leftarrow 1}$) is the formula obtained by replacing every
occurrence of $x$ in $\Sigma$ by the constant $false$ (resp. $true$). 
$\Sigma_{l \leftarrow 1}$ (resp. $\Sigma_{l \leftarrow 0}$) is an 
abbreviation for $\Sigma_{x \leftarrow 1}$ (resp. $\Sigma_{x \leftarrow 0}$)
when $l$ is a positive literal $x$ and for $\Sigma_{x \leftarrow 0}$
(resp. $\Sigma_{x \leftarrow 1}$) when $l$ is a negative literal $\neg x$.

Given an interpretation $\omega$ and a literal $l$, we let 
$Force(\omega,l)$ denote the interpretation that gives the same truth value as
$\omega$ to all variables except the variable of $l$, and such that 
$Force(\omega,l) \models l$. In other words, $Force(\omega,l)$ is the 
interpretation satisfying $l$ that is the closest to $\omega$.
For instance, provided that $PS = \{a, b\}$ and $\omega(a) = \omega(b) = 1$,
we have $Force(\omega, \neg b)(a) = 1$ and $Force(\omega, \neg b)(b) = 0$.
Clearly, if $\omega \models l$ then $Force(\omega,l)=\omega$.
If $L = \{l_1, \ldots, l_n\}$ is a consistent set of literals, then
$Force(\omega,L)$ is defined as 
$$Force(\ldots(Force(\omega,l_1),\ldots),l_n).$$
Lastly, given an interpretation $\omega$ and a variable $x$, we let
$Switch(\omega,x)$ denote the interpretation that gives the same truth value as
$\omega$ to all variables except $x$, and that gives to $x$ the value
opposite to that given by $\omega$. 


\iffalse
We also consider
the model obtained by swapping the truth value of a variable: $Swap(\omega,x)$
is the model which coincides with $\omega$ on every variable, except on $x$.
\fi

Two formulas $\Psi$ and $\Phi$ are said to be {\em equivalent
modulo} a formula $\Sigma$ if and only if $\Sigma \wedge \Psi \equiv \Sigma \wedge \Phi$.

In this paper we use the concepts of prime implicates and prime implicants.
The set of prime implicates of a formula $\Sigma$, denoted by
$IP(\Sigma)$, is defined as:

\[
IP(\Sigma) = \{ \delta \mbox{ clause } ~|~ \Sigma \models \delta \mbox{ and } \not\exists \delta' 
\mbox{ clause s.t.\ } \Sigma \models \delta' \mbox { and } \delta' \models \delta \mbox{ and } \delta \not 
\models \delta'\}.
\]

Among all the implicates of $\Sigma$ (i.e., the clauses entailed by $\Sigma$), the prime
implicates of $\Sigma$ are the minimal ones w.r.t. $\models$ (i.e., the logically strongest ones).
The set of prime implicants of a formula $\Sigma$, denoted by
$PI(\Sigma)$, is defined dually as:

\[
PI(\Sigma) = \{ \gamma \mbox{ term } ~|~ \gamma \models \Sigma \mbox{ and } \not\exists \gamma' 
\mbox{ term s.t.\ } \gamma' \models \Sigma \mbox { and } \gamma \models \gamma' \mbox{ and } \gamma' \not 
\models \gamma\}.
\]


Among all the implicants of $\Sigma$ (i.e., the terms implying $\Sigma$), the prime
implicants of $\Sigma$ are the maximal ones w.r.t. $\models$ (i.e., the logically weakest ones).

\iffalse

We also use the set of prime implicants modulo $\Sigma$ of a formula $\Phi$
over $PROP_X$, which will be denoted by $PI_{\Sigma}^X(\Phi)$ and is defined
by:

\[
PI_{\Sigma}^X(\Phi) = max(\{PI(\Sigma \Rightarrow \Phi) \cap PROP_X\}, \models)
\]

$IP_{\Sigma}^X(\Phi)$ denotes the set of prime implicates of $\Phi$
modulo $\Sigma$ over $PROP_X$, i.e.,

\[
IP_{\Sigma}^X(\Phi) = min(\{IP(\Sigma \Rightarrow \Phi) \cap PROP_X\}, \models)
\]

\fi

Of course, the set of prime implicants/ates
may contain equivalent terms/clauses. We can
restrict our attemption to one term/clause for each set of equivalent
terms/clauses.  Stated otherwise, in $PI(\Sigma)$ and $IP(\Sigma)$,
only one representative per equivalence class is kept.

\begin{example}

Let $\Sigma = \{a \vee b, \neg a \wedge c \Rightarrow e, d \Leftrightarrow e\}$.
The set of prime implicates of $\Sigma$ is, by definition,

\[
IP(\Sigma) =
\{a \vee b, a \vee \neg c \vee e, \neg d \vee e, d \vee \neg e, a \vee \neg c \vee d\}.
\]

\iffalse

The set of prime implicants modulo $\Sigma$ of a formula $e$, with respect
to the alphabets $\{a,b,c,d\}$, $\{a,c\}$, and $\{b,c\}$, are given by:

\begin{eqnarray*}\\
PI_{\Sigma}^{\{a,b,c,d\}}(e) &=& \{d, \neg a \wedge c, \neg a \wedge \neg b\} \\
PI_{\Sigma}^{\{a,c\}}(e) &=& \{\neg a \wedge c\} \\
PI_{\Sigma}^{\{b,c\}}(e) &=& \emptyset
\end{eqnarray*}

The set of prime implicants modulo $\Sigma$ of $a \vee b$, over the alphabet
$\{a,b,c,d\}$ is:

\[
PI_{\Sigma}^{\{a,b,c,d\}}(a \vee b) = \{true\}
\]

\fi

\end{example}


\subsection{Computational Complexity}\label{prelicc}

The complexity results we give in this paper refer to some complexity 
classes which deserve some recalls. More details can be found in 
\citeS{Papadimitriou94} textbook.
Given a problem {\sc a}, we denote by $\overline{\mbox{\sc a}}$ 
the complementary problem of {\sc a}.
We assume that the classes {\sf P}, {\sf NP} and {\sf coNP} are known
to the reader. The following classes will also be considered:

\begin{itemize}

\item
$\mbox{{\sf BH}}_2$ (also known as {\sf DP}) is 
the class of all languages $L$ such that $L = L_1 \cap L_2$, where 
$L_1$ is in {\sf NP} and $L_2$ in {\sf coNP}. The canonical 
$\mbox{{\sf BH}}_2$-complete problem is {\sc sat--unsat}: a pair of 
formulas $\langle \varphi, \psi \rangle$ is in {\sc sat--unsat} if and only if
$\varphi$ is satisfiable and $\psi$ is not. The complementary class
$\mbox{{\sf coBH}}_2$ is the class of all languages $L$ such that 
$L = L_1 \cup L_2$, where 
$L_1$ is in {\sf NP} and $L_2$ in {\sf coNP}. The canonical 
$\mbox{{\sf coBH}}_2$-complete problem is {\sc sat-or-unsat}: a pair of 
formulas $\langle \varphi, \psi \rangle$ is in {\sc sat-or-unsat} if and only if
$\varphi$ is satisfiable or $\psi$ is not.
\item $\Delta_2^p = \mbox{\sf P}^{{\sf NP}}$ is the class of all 
languages recognizable in polynomial time by a deterministic Turing
machine equipped with an {\sf NP} oracle, i.e., a device able to solve any
instance of an {\sf NP} or a {\sf coNP} problem in unit time.
${\sf F}\Delta_2^p$ is the corresponding class of function problems.
\item $\Sigma_2^p = \mbox{\sf NP}^{{\sf NP}}$ is the class of all 
languages recognizable in polynomial time by a nondeterministic Turing
machine equipped with an {\sf NP} oracle.
The canonical $\Sigma_2^p$-complete problem \deuxqbf is the set
of all triples $\langle A = \{a_1,...,a_m\},  B = \{b_1,...,b_n\},
\Phi\rangle$
where $A$ and $B$ are two disjoint sets of propositional variables
and $\Phi$ is a formula from $PROP_{A\cup B}$. A positive instance
of this problem is a triple $\langle A, B, \Phi\rangle$ for which there exists
a $A$-world $\omega_A$ such that for all $B$-world $\omega_B$ we have
$\omega_A \wedge \omega_B \models \Phi$.
\item $\Pi_2^p$ = {\sf co}$\Sigma_2^p =  \mbox{\sf coNP}^{{\sf NP}}$.
The canonical $\Pi_2^p$-complete problem \2qbfbarre is the set
of all triples $\langle A = \{a_1,...,a_m\},  B = \{b_1,...,b_n\},
\Phi\rangle$
where $A$ and $B$ are two disjoint sets of propositional variables
and $\Phi$ is a formula from $PROP_{A\cup B}$. A positive instance
of this problem is a triple $\langle A, B, \Phi\rangle$ such that for every
$A$-world $\omega_A$ there exists a $B$-world $\omega_B$ for which
$\omega_A \wedge \omega_B \models \Phi$.


\end{itemize}

$\Sigma_2^p$ and $\Pi_2^p$  are complexity classes
located at the so-called second level of the polynomial hierarchy,
which plays a prominent role in knowledge representation and reasoning. 

\section{Formula-Literal and Formula-Variable Independence}\label{fvindep}

Formula-literal and formula-variable independence capture some forms 
of independence between the truth values of variables and the possible
truth values of a formula.  Roughly speaking, $\Sigma$ is dependent 
on $l$ because it tells one something positive about $l$: more precisely,
there is a contest, i.e., a conjunction of literals, that,
added to to $\Sigma$ enables one to infer $l$.
For instance, $\Sigma=(a\Rightarrow b)$ is dependent on $b$, since $b$ 
can be inferred from $\Sigma$ under the assumption that $a$ is true.
Of course, we cannot assume contexts that are
inconsistent with $\Sigma$, and we cannot assume $l$ itself.  
A formula $\Sigma$ will be considered as independent from variable 
$x$ if and only if it is both
independent from $x$ and independent from $\neg x$.  Dually, we can
interpret both forms of dependence as aboutness relations; 
when $\Sigma$ is dependent on a literal $l$, it tells one something about 
$l$, and when $\Sigma$ is dependent on a variable $x$, it tells something 
about $x$ or about $\neg x$.

\subsection{Syntactical Independence}

The easiest way to define dependence between a formula $\Sigma$ and a 
literal $l$ is by assuming that $\Sigma$, when put into NNF, 
contains $l$. 
Reminding that $Lit(\Sigma)$ is the set of literals that occur in the NNF of 
$\Sigma$, this can be formally expressed by the following definition:

\begin{defin}[syntactical FL-independence]\label{defsfl}
Let $\Sigma$ be a formula from $PROP_{PS}$, $l$ a literal of $L_{PS}$, and
$L$ a subset of $L_{PS}$. 
\begin{itemize}
\item $\Sigma$ is said to be {\em syntactically Lit-dependent} on $l$ (resp. {\em 
syntactically Lit-independent} from $l$) if and only if $l \in Lit(\Sigma)$ (resp. $l \not \in 
Lit(\Sigma)$).
\item $\Sigma$ is said to be {\em syntactically Lit-dependent} on $L$ 
if and only if there is a $l \in L$ such that $\Sigma$ is syntactically Lit-dependent on $l$.
Otherwise, $\Sigma$ is said to be {\em syntactically Lit-independent} from~$L$.
\end{itemize}
\end{defin}

From this definition it follows immediately that $\Sigma$ is syntactically 
Lit-independent from $L$ if and only if $Lit(\Sigma) \cap L = \emptyset$.
Thus, in order to determine whether a formula $\Sigma$ is syntactically Lit-dependent on 
a set $L$ of literals, it suffices to check whether there exists a literal 
in $L$ that occurs in the NNF of $\Sigma$.

\begin{example}
Let $\Phi = \neg ({\mbox a} \wedge {\mbox b})$. The NNF of $\Phi$ is $(\neg 
{\mbox a} \vee \neg {\mbox b})$; therefore, $\Phi$ is syntactically Lit-dependent 
on both $\neg {\mbox a}$ and $\neg {\mbox b}$, while it is syntactically
Lit-independent from ${\mbox a}$ and ${\mbox b}$.
\end{example}

As this example illustrates, a propositional formula can easily be 
syntactically Lit-independent from a literal while syntactically
Lit-dependent on its negation. This is as expected, since 
$\Sigma$ may imply $l$ in some context, while it may be always 
impossible to derive $\neg l$. In other words, the set of literals $\Sigma$ 
is syntactically Lit-independent from is not closed under negation. Interestingly, a 
notion of syntactical formula-variable independence can be defined from the 
more basic notion of syntactical FL-independence.

\begin{defin}[syntactical FV-independence]\label{defsfv}
Let $\Sigma$ be a formula from $PROP_{PS}$, $v$ a variable of $PS$, and
$V$ a subset of $PS$.
\begin{itemize}
\item $\Sigma$ is said to be {\em syntactically Var-dependent} on $v$ (resp. {\em 
syntactically Var-independent} from $v$) if and only if 
$v \in Var (\Sigma)$ (resp. $v \not \in Var(\Sigma)$).
\item $\Sigma$ is said to be {\em syntactically Var-dependent} on $V$ if and only if there is a variable 
$v$ in $V$ s.t. $\Sigma$ is Var-dependent on it, i.e., if and only if $Var(\Sigma) \cap V \neq 
\emptyset$. Otherwise, $\Sigma$ is said to be {\em syntactically Var-independent} from $V$.
\end{itemize}
\end{defin}

\begin{example} Let $\Sigma = (a \wedge \neg b)$. $\Sigma$ is syntactically 
Var-dependent on $a$ and on $b$ and syntactically Var-independent from $c$.
\end{example}

Syntactical FV-independence can be easily expressed as syntactical FL-independence: 
$\Sigma$ is syntactically Var-independent from $V$ if and only 
if it is syntactically Lit-independent from $V \cup \{ \neg x \ | \ x \in V 
\}$.
Clearly enough, both syntactical formula-literal independence and 
syntactical formula-variable independence can be checked in linear time.

However, these basic forms of independence suffer from two important 
drawbacks. First, they do not satisfy the principle of irrelevance of 
syntax: two equivalent formulas are not always syntactically independent 
from the same literals/variables.
Second, 
syntactical dependence does not always capture the intuitive 
meaning of dependence: for instance, $\Sigma = (a \wedge \neg b \wedge (a 
\vee b))$ is syntactically Lit-dependent on $a$, $\neg b$, $b$; since $\neg b$ 
can be derived from $\Sigma$, $\Sigma$ is about $\neg b$ in some sense. 
Contrastingly, there is no way to derive $b$ from $\Sigma$, unless producing 
an inconsistency.

Handling such a separation requires a more robust notion of independence, 
to be introduced in the following section.

\subsection{Semantical Independence}

We now give a {\em semantical} definition of independence, which does
not suffer from the aforementioned drawbacks, i.e., a definition that
does not depend on the syntactical form in which formulas are
expressed. We will prove that this semantical definition of
independence does not suffer from the second drawback of syntax
independence, i.e., a formula that is semantically dependent on a
literal always enables one to derive the literal in some context.

\begin{defin}[(semantical) FL-independence]\label{semflindep}
Let $\Sigma$ be a formula from $PROP_{PS}$, $l \in L_{PS}$, and $L$ a 
subset of $L_{PS}$. 
\begin{itemize}
\item $\Sigma$ is said to be {\em Lit-independent}\footnote{In order to avoid any ambiguity,
we will refer to the syntactical forms of independence explicitly from now on; in other words,
independence must be taken as semantical by default in the rest of the paper.}  
from $l$, denoted $l \not \leadsto \Sigma$, if
and only if there exists a formula $\Phi$ s.t.\  $\Phi \equiv \Sigma$ and 
$\Phi$ is syntactically Lit-independent from $l$.  
Otherwise, $\Sigma$ is said to be {\em Lit-dependent} on $l$, denoted $l \leadsto \Sigma$.
The set of all literals of $L_{PS}$ such that $l \leadsto \Sigma$ is denoted
by $DepLit(\Sigma)$.
\item $\Sigma$ is said to be {\em Lit-independent} from $L$, 
denoted $L \not \leadsto \Sigma$, if and only if $L \cap DepLit(\Sigma) = \emptyset$.
Otherwise, $\Sigma$ is said to be {\em Lit-dependent} on $L$, denoted $L \leadsto \Sigma$.
\end{itemize}
\end{defin}

Simply rewriting the definition, $\Sigma$ is Lit-independent from $L$ if and 
only if there exists a formula $\Phi$ s.t.\  $\Phi \equiv \Sigma$ and $\Phi$ is
syntactically Lit-independent from $L$. Thus, FL-independence is not affected by the
syntactic form in which a formula is expressed, that is,
replacing $\Sigma$ with any of its equivalent formulas does not modify the relation
$\leadsto$. Since $\Sigma$ is Lit-independent from $L$ if and
only if $\Sigma$ can be made syntactically Lit-independent from $L$ while
preserving logical equivalence, it follows that syntactical Lit-independence implies
Lit-independence, but the converse does not hold in the general case.

\begin{example}
Let $\Sigma = (a \wedge \neg b \wedge (a \vee b))$.
We have $DepLit (\Sigma) =  \{a, \neg b\}$. Note that
$\Sigma$ is Lit-independent from $b$ because it is equivalent to
$\Phi = (a \wedge \neg b)$, in which $b$ does not appear 
positively.
\end{example}

As in the case of syntactical independence, we can formalize the fact that a
formula $\Sigma$ has some effects on the truth value of a variable $v$. 
Indeed,
we define a notion of (semantical) formula-variable independence, which can
also be easily defined from the (semantical) notion of FL-independence.

\begin{defin}[(semantical) FV independence]\label{semfvindep}

Let $\Sigma$ be a formula from $PROP_{PS}$, $v \in PS$, and $V$ a subset of $PS$.
\begin{itemize}
\item $\Sigma$ is said to be {\em Var-independent} from $v$, denoted $v \not \leadsto_{-}^{+}
\Sigma$, if and only if there exists a formula $\Phi$ s.t.\  $\Phi \equiv
\Sigma$ and $\Phi$ is syntactically Var-independent from $v$.
Otherwise, $\Sigma$ is said to be {\em Var-dependent} on $v$, denoted
$v \leadsto_{-}^{+}\Sigma$.
We denote by $DepVar(\Sigma)$ the set of all variables $v$ such that
$v \leadsto_{-}^{+}\Sigma$.
\item $\Sigma$ is said to be {\em Var-independent} from $V$,
denoted $V \not \leadsto_{-}^{+} \Sigma$, if and only if $V \cap 
DepVar(\Sigma) = \emptyset$.
Otherwise, $\Sigma$ is said to be {\em Var-dependent} on $V$, denoted
$V \leadsto_{-}^{+}\Sigma$.
\end{itemize}
\end{defin}

Clearly, $\Sigma$ is Var-independent from $V$ if and only if there exists a
formula $\Phi$ s.t.\  $\Phi \equiv \Sigma$ and $\Phi$ is syntactically Var-independent
from $V$.
Moreover, Var-independence is to Lit-independence as syntactical Var-independence 
is to syntactical Lit-independence; indeed, $\Sigma$ is Var-independent from $V$
if and only if $\Sigma$ is Lit-independent from $L_V$.

\begin{example}
Let $\Sigma = ({\mbox a} \wedge \neg {\mbox b} \wedge
({\mbox a} \vee {\mbox c}))$.
We have $DepVar(\Sigma) = \{a,b\}$.  Note that $\Sigma$
is Var-independent from ${\mbox c}$.
\end{example}

The definition of semantical FL-independence is based on the set of literals 
of formulas equivalent to $\Sigma$. Intuitively, this is the easiest way to 
define
a notion of independence that is not dependent on the syntax. However, 
proving theorems directly from this definition is not so easy. For instance, we will prove
that determining whether a formula $\Sigma$ is Lit-dependent on literal $l$ 
is in \np, but this result cannot be {\em directly} proved from Definition 
\ref{semflindep}, since checking all possible
formulas equivalent to $\Sigma$ cannot be done with a polynomial
non-deterministic guessing. We give now a semantical characterization of FL-independence.


\begin{prop}
\label{sema-inde-lite}
A formula $\Sigma$ is Lit-independent from literal $l$ if and only if, for any
interpretation $\omega \in \Omega_{PS}$, if $\omega \models \Sigma$ then
$Force(\omega,\neg l) \models \Sigma$.
\end{prop}

As a direct corollary, we get that $\Sigma$ is Lit-independent from $L$ if and only if
for any literal $l \in L$ and any interpretation $\omega \in \Omega_{PS}$, 
if $\omega \models \Sigma$
then $Force(\omega,\neg l) \models \Sigma$.

This property gives an idea of how FL-dependence works. Indeed, if $\Sigma$ 
is Lit-dependent on a literal $l$, then there exists an interpretation $\omega$ 
such that $\omega \models \Sigma$ and $Force(\omega,\neg l) \not\models \Sigma$, which means 
that (a) $\omega \models l$ and (b) the literal $l$ in $\omega$ is ``really 
needed'' to make $\omega$ a model of
$\Sigma$, that is, the partial interpretation obtained by removing $l$ in
$\omega$ does
not satisfy $\Sigma$.

This property also explains why FL-dependence formalizes the concept of
``true in some context'', as explained at the beginning of this section.
Indeed, $\Sigma$ is Lit-dependent on $l$ if and only if there is some
context (consistent with $\Sigma$, and that does not imply $l$), in
which $\Sigma$ implies $l$. This can be proved from the above proposition:
if $\omega$ is an interpretation such that $\omega \models \Sigma$ but
$Force(\omega,\neg l) \not\models \Sigma$, then the term:\eatpar

\[
\gamma = \bigwedge (\{ x \in PS ~|~ \omega \models \Sigma \wedge x \} 
\cup \{ \neg x  ~|~ x \in PS ~ and~ \omega \models \Sigma \wedge \neg x \})
\backslash \{l\}
\]

\noindent is consistent with $\Sigma$
(by construction, $\gamma$ is equivalent to the disjunction of a term equivalent
to $\omega$ with a term equivalent to $Force(\omega, \neg l)$); it also holds that
$\gamma \wedge \Sigma \models l$, while
$\gamma \not\models l$, that is, $\gamma$ is a context in which
$\Sigma$ implies $l$.

Moreover, Proposition \ref{sema-inde-lite} shows that our notion of
Lit-independence
coincides with the notion of {\em (anti-)monotonicity} \cite{Ryan91,Ryan92}.
To be more precise, a (consistent) formula is said to be monotonic (resp.
antimonotonic) in variable $v$
if and only if it is Lit-independent from $\neg v$ (resp. from $v$).
Interestingly, a subclassical\footnote{That is, a restriction of 
classical entailment $\models$.}
inference relation, called {\it natural inference}, has been
defined on this ground \cite{Ryan91,Ryan92}.
Basically, a formula $\varphi$ is
considered as a consequence of a formula $\Sigma$ if and only if it is a 
logical consequence of it, and $\Sigma$ Lit-independence of a literal
implies its $\varphi$ Lit-independence.
Accordingly, natural inference prevents us from
considering $p \vee q$ as a consequence of $p$ (it is a relevant implication). 
All our characterization results about Lit-independence,
including complexity results, have an immediate impact on such a natural inference
relation (especially, they directly show that the complexity of natural
inference is in $\Delta_2^p$).

Proposition~\ref{sema-inde-lite} is easily extended to formula-variable
independence:

\begin{corollary}~\label{sema-inde-vars}~
A formula $\Sigma$ is Var-independent from variable $v$ if and only if,
for any interpretation $\omega \in \Omega_{PS}$,
we have $\omega \models \Sigma$ if and only if
$Switch(\omega,v) \models \Sigma$.
\end{corollary}

The following metatheoretic properties of FL-independence are used in the 
rest of this section.

\begin{prop}\label{PropFLI}~\\
(1) $DepLit(\Sigma) \subseteq Lit(\Sigma)$;\\
(2) If $\Sigma \equiv \Phi$, then $DepLit(\Sigma) = DepLit(\Phi)$;\\
(3a) $DepLit(\Sigma\wedge \Phi) \subseteq DepLit(\Sigma) \cup 
DepLit(\Phi)$;\\
(3b) $DepLit(\Sigma\vee \Phi) \subseteq DepLit(\Sigma) \cup 
DepLit(\Phi)$;\\
(4) $l \in DepLit(\Sigma)$ if and only if $\neg l \in DepLit(\neg \Sigma)$.
\end{prop}

FV-independence exhibits similar properties, plus negation stability
(point (4) below), which is not satisfied by FL-independence.

\begin{prop}{~}\label{PropFVI}\\
(1) $DepVar(\Sigma) \subseteq Var(\Sigma)$;\\
(2) If $\Sigma \equiv \Phi$, then $DepVar(\Sigma) = DepVar(\Phi)$;\\
(3a) $ DepVar(\Sigma\wedge \Phi) \subseteq DepLit(\Sigma) \cup 
DepLit(\Phi)$;\\
(3b) $ DepVar(\Sigma\vee \Phi) \subseteq DepLit(\Sigma) \cup 
DepLit(\Phi)$;\\
(4) $DepVar(\neg \Sigma) = DepVar(\Sigma)$.
\end{prop}


Beyond these properties, FL-independence and FV-independence do not exhibit
any particularly interesting structure. In particular, FL-independence and 
FV-independence neither are monotonic nor anti-monotonic w.r.t. expansion of
$\Sigma$ (strengthening or weakening $\Sigma$ can easily make it no longer
independent from a set of literals or variables).

Recall that $L \mapsto \Sigma$  \iff $L \cap DepLit(\Sigma) \neq \emptyset$.
This means that the Lit-dependence of $\Sigma$ on $L$
only implies the Lit-dependence on a literal of $L$, 
not a ``full'' Lit-dependence on any literal of $L$. 
In other words, if we want to check whether a formula 
$\Sigma$
is Lit-dependent on {\em any} literal of $L$, we need a notion stronger 
than FL-dependence, called full FL-dependence. The same can be said for FV-dependence.

\begin{defin}[full FL/FV-dependence]
Let $\Sigma$ be a formula from $PROP_{PS}$, $L$ be a subset of 
$L_{PS}$ and $V$ be a subset of $PS$.
\begin{itemize}
\item $\Sigma$ is {\em fully Lit-dependent} on $L$ if and only if
$L \subseteq DepLit(\Sigma)$.
\item$\Sigma$ is {\em fully Var-dependent} on $V$ if and only if
$V \subseteq DepVar(\Sigma)$.
\end{itemize}
\end{defin}

\begin{example}
$\Sigma = (a \wedge \neg b \wedge (b \vee \neg b))$ is fully Lit-dependent on
$\{a, \neg b\}$ and fully Var-dependent on $\{a, b\}$. Contrastingly, $\Sigma$ 
is not fully Lit-dependent on $\{a, b\}$.
\end{example}

Clearly enough, whenever $\Sigma$ is fully Lit-dependent on $L$, it is also 
fully
Var-dependent on $Var(L)$. However, the converse does not hold, as the 
previous
example shows.

While full FL-dependence (resp. full FV-dependence) can be checked in linear time once
$DepLit(\Sigma)$ (resp. $DepVar(\Sigma)$) is known, at the end of the
section we prove that determining these sets is \np-hard,
and that deciding full FL-dependence (as well as full FV-dependence) 
is \np-complete.


Let us now consider the particular case of full FL-dependence when $L =
Lit(\Sigma)$, or the full FV-dependence when $V = Var(\Sigma)$. If full
dependence holds in these cases, we say that $\Sigma$ is Lit-simplified, or
Var-simplified, respectively. Var-simplification is achieved when $\Sigma$ 
contains no occurrence of any variable it is Var-independent from.  
Lit-simplification
corresponds to the more restricted situation where the NNF of $\Sigma$ does 
not contain any occurrence of a literal it is Lit-independent from.

If a formula $\Sigma$ is not Lit-simplified (resp. Var-simplified), then
there is some literal (resp. variable) that occurs in the NNF of $\Sigma$, 
but $\Sigma$ is not Lit-dependent (resp. Var-dependent) on it. 
This means that the syntactic form in which $\Sigma$ is
expressed contains a literal or variable that is indeed useless.

\begin{defin}[simplified formula]\label{defsimplified}
Let $\Sigma$ be a formula from $PROP_{PS}$.
\begin{itemize}
\item $\Sigma$ is {\em Lit-simplified} if and only if
	$Lit(\Sigma) = DepLit(\Sigma)$.
\item $\Sigma$ is {\em Var-simplified} if and only if
	$Var(\Sigma) = DepVar(\Sigma)$.
\end{itemize}
\end{defin}

As the following example illustrates, every formula that is Lit-simplified 
also is Var-simplified but the converse does not hold in the general case.

\begin{example}
$\Sigma = (a \wedge \neg b \wedge (b \vee \neg b) \wedge (a \vee c))$ 
neither
is Lit-simplified nor Var-simplified. The equivalent formula $(a \wedge \neg b
\wedge (b \vee \neg b))$ is Var-simplified but it is not Lit-simplified. 
Finally, the equivalent formula $(a \wedge \neg b)$ is both Lit-simplified and
Var-simplified.

\end{example}

Simplified formulas do not incorporate any useless literals or variables.
As the next proposition shows it, the notion of simplified formula actually 
is the point where syntactical independence and (semantical) independence
coincide.

\begin{prop}~\label{simplified} Let $\Sigma$ be a formula from $PROP_{PS}$.
\begin{itemize}
\item $\Sigma$ is Lit-simplified if and only if the following equivalence 
holds:
for every
$L \subseteq L_{PS}$,
$\Sigma$ is syntactically Lit-independent from $L$ if and only if $L \not 
\leadsto
\Sigma$ holds.
\item $\Sigma$ is Var-simplified if and only if the following equivalence 
holds:
for every
$V \subseteq PS$,
$\Sigma$ is syntactically Var-independent from $V$ if and only if $V \not
\leadsto_{-}^{+} \Sigma$ holds.
\end{itemize}
\end{prop}

Thus, while a formula can easily be Lit-independent from a set of literals
without being syntactically Lit-independent from it, simplification is a way 
to join Lit-independence with its syntactical restriction (which is easier to 
grasp, and as we will see soon, easier to check in the general case): 
Lit-independence and syntactical Lit-independence coincide on Lit-simplified formulas. The same
holds for Var-independence and syntactical Var-independence.

The strength of the notion of simplification lies in the fact that every
formula can be simplified preserving its models. This is useful, as 
simplified
formulas can be shorter and easier to understand than formulas containing
useless literals.

\begin{prop}~\label{ex-simp}
For every $\Sigma$ from $PROP_{PS}$, there exists a Lit-simplified formula 
$\Phi$
s.t.\  $\Sigma \equiv \Phi$.
\end{prop}

Since Lit-simplified KBs are also Var-simplified, this proposition also shows 
that every KB can be Var-simplified without modifying its set of models.

\

Interestingly, both FL-independence and FV-independence can be characterized
without considering the corresponding syntactic notions of independence, 
just by comparing formulas obtained by setting the truth value of literals we 
want to check the dependence.

\begin{prop}\label{deductionl}
Let $\Sigma$ be a formula from $PROP_{PS}$ and $l$ be a literal of $L_{PS}$.
The next four statements are equivalent:\\
(1) $l \not \leadsto \Sigma$;\\
(2) $\Sigma_{l \leftarrow 1} \models \Sigma_{l \leftarrow 0}$;\\
(3) $\Sigma \models \Sigma_{l \leftarrow 0}$;\\
(4) $\Sigma_{l \leftarrow 1} \models \Sigma$.
\end{prop}


The above properties can be used to check whether a formula is Lit-dependent on a
literal, as the following example shows.

\begin{example}
$\Sigma = (a \wedge \neg b \wedge (b \vee \neg b))$ is Lit-independent from 
$b$ since replacing $b$ by $true$ within $\Sigma$ gives rise to an inconsistent
formula. Contrastingly, $\Sigma$ is Lit-dependent on $\neg b$ since
replacing $b$ by $false$ within
$\Sigma$ gives  $\Sigma_{b \leftarrow 0} \equiv a$, which is not at least as
logically strong as the inconsistent formula obtained by replacing 
$b$ by $true$ within $\Sigma$.
\end{example}

A similar proposition holds for FV-independence, characterizing the 
variables a formula $\Sigma$ depends on, using the formulas $\Sigma_{x \leftarrow
0}$ and $\Sigma_{x \leftarrow 1}$.

\begin{prop}\label{deductionfv}
Let $\Sigma$ be a formula from $PROP_{PS}$ and $x$ be a variable of $PS$.
The next four statements are equivalent:\\
(1) $x \not \leadsto_{-}^{+} \Sigma$;\\
(2) $\Sigma_{x \leftarrow 0} \equiv \Sigma_{x \leftarrow 1}$;\\
(3) $\Sigma \equiv \Sigma_{x \leftarrow 0}$;\\
(4) $\Sigma \equiv \Sigma_{x \leftarrow 1}$.
\end{prop}

As in the case of literal dependence, the above property can be used to find
out whether a formula is Var-dependent on a variable.

\begin{example}
$\Sigma = (a \wedge (b \vee \neg b))$ is Var-independent from $b$ since we 
have $\Sigma_{b \leftarrow 0} \equiv \Sigma_{b \leftarrow 1} \equiv a$.
\end{example}


Interestingly, FL-independence and FV-independence can be determined in an
efficient way when $\Sigma$ is given in some specific normal forms, namely,
prime implicate normal form or prime implicant normal form. For such
normal forms, Lit-independence and Var-independence come down to their
corresponding syntactical forms.

\begin{prop}\label{primel}
Let $\Sigma$ be a formula from $PROP_{PS}$ and $L$ be a subset of
$L_{PS}$.
The next statements are equivalent:\\
(1) $L \not \leadsto \Sigma$;\\
(2) $PI(\Sigma) \subseteq \{\gamma \ | \ \gamma$ is a term that does not 
contain
any literal from
$L\}$;\\
(3) $IP(\Sigma) \subseteq \{\delta \ | \ \delta$ is a clause that does not
contain any literal from
$L\}$.
\end{prop}


\begin{prop}\label{primev}
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ be a subset of 
$PS$.
The next statements are equivalent:\\
(1) $V \not \leadsto_{-}^{+} \Sigma$;\\
(2) $PI(\Sigma) \subseteq \{\gamma \ | \ \gamma$ is a term that does not 
contain
any variable from
$V\}$;\\
(3) $IP(\Sigma) \subseteq \{\delta \ | \ \delta$ is a clause that does not
contain any variable from
$V\}$.
\end{prop}


\begin{example}
Let $\Sigma = (a \wedge \neg b \wedge (b \vee \neg b))$.
We have $PI(\Sigma) = \{(a \wedge \neg b)\}$ and $IP(\Sigma) = \{a, \neg 
b\}$
(up to logical equivalence).
We can easily observe that $\Sigma$ is Lit-independent from $b$ looking at
$PI(\Sigma)$ (or $IP(\Sigma)$). We can also easily state that $\Sigma$ is
Lit-dependent on $\neg b$ and Var-independent from $c$ by considering any
of these normal forms.
\end{example}

Proposition \ref{deductionfv} shows that a KB can be easily Var-simplified 
(i.e., in
polynomial time) as soon as the variables it is Var-independent from have been
determined.
Indeed, we can easily design a greedy algorithm for simplifying KBs.
This algorithm consists in considering every variable $x$ of $Var(\Sigma)$
in a successive way, while replacing $\Sigma$ by $\Sigma_{x \leftarrow 0}$
whenever
$\Sigma$ is Var-independent from $x$. This algorithm runs in time polynomial 
in
the size
of $\Sigma$ once the variables $\Sigma$ is Var-independent from have 
been
computed. At the end, the resulting KB is Var-simplified.

Lit-simplifying a KB is not so easy if no assumptions are made about
its syntax, due to the fact that literals signs are crucial
here. Indeed, looking only at the occurrence of a variable inside a formula
is not sufficient to state whether or not this is a positive occurrence
(or a negative one). Fortunately, turning a formula into its NNF is 
computationally
easy (as long as it does not contain any occurrence of connectives like
$\Leftrightarrow$ or $\oplus$)
and it proves sufficient to design a greedy algorithm for Lit-simplifying
a KB when the literals it is Lit-independent from have been identified.
Indeed, within an NNF formula, every literal can be considered easily as
an atomic object.
This algorithm consists in considering every literal $l$ of $Lit(\Sigma)$
in a successive way, while replacing every occurrence of $l$ in $\Sigma$ by
$false$ considering every literal of $Lit(\Sigma)$ as an atom. Stated 
otherwise,
when $l$ is a positive (resp. negative) literal $x$ (resp. $\neg x$), 
replacing
$l$ by $false$ does not mean replacing $\neg x$ (resp. $x$) by $true$: only 
the
occurrences of $l$ with the right sign are considered.
This algorithm runs in time polynomial in the size
of $\Sigma$ once the literals $\Sigma$ is Lit-independent from have been
computed. At the end, the resulting KB is Lit-simplified.

%\fi

\newpage

\subsection{Complexity Results}~\label{comp-sema}

While syntactical FL and FV-dependence can be easily checked in linear time in
the size of the input, this is far from being expected for (semantical) FL-dependence
and FV-dependence
in the general case:

\begin{prop}[complexity of FL/FV-dependence]\label{cflfv}
{\sc FL dependence}, {\sc FV dependence}, {\sc full FL dependence} 
and {\sc full FV dependence} are {\sf NP}-complete.
\end{prop}


Thus, although they look simple, the problems of determining
whether a formula is independent from a literal or a variable
are as hard as checking propositional entailment.
Interestingly, the complexity of both decision problems fall down to {\sf P}
whenever checking (in)dependence becomes tractable.
Apart from the case of syntactical independence, some other restrictions
on $\Sigma$ makes (in)dependence testable in polynomial time.
Especially, we get:

\begin{prop}~\label{poly}
Whenever $\Sigma$ belongs to a  class ${\mathcal C}$ of CNF formulas that is 
tractable for clausal query answering (i.e., there exists a polytime algorithm to determine
whether $\Sigma \models \gamma$ for any CNF formula $\gamma$) and stable for variable 
instantiation (i.e., replacing in $\Sigma \in {\mathcal C}$ any variable by
{\em true} or by {\em false}
gives a formula that still belongs to ${\mathcal C}$) then 
{\sc FL dependence}, {\sc FV dependence}, {\sc full FL dependence} and 
{\sc full FV dependence} are in {\sf P}.
\end{prop}


In particular, when $\Sigma$ is restricted to a renamable Horn CNF formula 
or to binary clauses (Krom formula), all four decision problems above belong to 
{\sf P}. 

We have also investigated the complexity of checking whether a formula is
Lit-simplified (and Var-simplified):

\begin{prop}~\label{comp-simplif}
{\sc Lit-simplified formula} and {\sc Var-simplified formula} are {\sf NP}-complete.
\end{prop}

All these complexity results
have some impact on the approaches that explicitly need computing 
$DepVar(\Sigma)$ as a preprocessing task.
Namely, we have the following result:

\begin{prop}
\label{computeDepLitVar}\

\begin{enumerate}
%\framebox{\vbox{ \vskip 1cm ~ }}
\item %\framebox{\vbox{ \vskip 1cm ~ }}
Determining whether $DepLit(\Sigma) = L$ (where $L$ is a set of 
literals), and determining  whether $DepVar(\Sigma) = X$ (where $X$ 
is a set of variables) is \bh2-complete.
\item The search problem consisting in {\em computing} $DepLit(\Sigma)$ 
(respectively $DepVar(\Sigma)$) is in ${\sf F}\Delta_2^p$ and
is both {\sf NP}-hard and \conp-hard.
\end{enumerate}
\end{prop}


\subsection{Discussion}

The previous characterizations and complexity results lead to
several questions: when is it worthwhile to preprocess a knowledge
base by computing independence relations? How should these independence
relations be computed? What is the level of generality of the definitions
and results we gave in this section?

Many equivalent characterizations of formula-variable independence have 
been given in the literature, each of which could serve as a definition 
(Definition~\ref{semfvindep}, Corollary~\ref{sema-inde-vars}, 
each of the statements (2), (3) and (4) in Proposition~\ref{deductionfv}
and of the statements (2), (3) in Proposition~\ref{primev}), 
so one may wonder which one has to be used in practice.

In many papers referring explicitly to formula-variable independence,
the prime implicant/cate characterization (Proposition~\ref{primev}) is used
as a definition \cite{Boutilier94,Dohertyetal98}. Generally speaking, 
this is not the cheapest way to compute the set of variables a formula 
depends on, since the size of $PI(\Sigma)$ is
exponential in the size of $\Sigma$ in the worst case.
This characterization is to be used in practice only if the syntactical 
form of $\Sigma$ is such that its prime implicants or prime implicates can 
be computed easily from it (this is the case for instance whenever
$\Sigma$ is a Krom formula). Clearly, the cheapest way to compute 
formula-variable independence consists in using any of the equivalent
formulations of Proposition~\ref{deductionfv}, which all consist of
validity tests. 

Checking whether a formula $\Sigma$ is Var-independent from a variable $x$ is 
\conp-complete, which implies that simplifying a knowledge base by getting
rid of redundant variables needs $|Var(\Sigma)|$ calls to an {\sf NP} oracle,
and is thus in ${\sf F}\Delta_2^p$ and not below (unless {\sf NP} = {\sf coNP}). 
This may look paradoxical (and sometimes useless) to preliminarily 
compute several instances of a \np \ or \conp-hard independence problem to 
help solving a (single) instance of a {\sf NP} or \conp-complete problem. 
However, this negative comment has a general scope only, and in many 
particular cases, this can prove quite efficient (indeed, even when 
$\Sigma$ has no particular syntactical form, the satisfiability
or the unsatisfiability of 
$\Sigma_{x\leftarrow 0} \wedge \neg \Sigma_{x \leftarrow 1}$ may be 
particularly easy to check). 
Furthermore, if the knowledge base $\Sigma$ is to be queried many times,
then the preprocessing phase consisting in Var-simplifying $\Sigma$
by ignoring useless variables is likely to be worthwhile. 

\section{Forgetting}\label{forg}

In this section, we define what forgetting is, present some
of its properties, and finally give some complexity results.


\subsection{Definitions and Properties}

A basic way to simplify a KB w.r.t.\  a set of literals or a set of variables
consists in {\em forgetting} literals/variables in it. Beyond the
simplification task, forgetting is a way to make a formula independent from
literals/variables. Let us first start with literal forgetting:

\begin{defin}[literal forgetting]\label{deflf}
Let $\Sigma$  be a formula from $PROP_{PS}$ and $L$ be a subset of $L_{PS}$.
$ForgetLit(\Sigma, L)$ is the formula inductively defined as follows:\eatpar

\begin{enumerate}

\item $ForgetLit(\Sigma, \emptyset) = \Sigma$,

\item $ForgetLit(\Sigma, \{l\}) = \Sigma_{l \leftarrow 1} 
\vee (\neg l \wedge \Sigma)$,

\item $ForgetLit(\Sigma, \{l\} \cup L) = ForgetLit(ForgetLit(\Sigma, L), \{l\})$.

\end{enumerate}

\end{defin}

This definition is sound since the ordering in which literals of $L$ are 
considered does not matter%
\footnote{The proof of this statement is almost straightforward: 
let $l_1$, $l_2$ be two literals;
\begin{enumerate}
\item if $l_1 \neq l_2$ and  $l_1 \neq \neg l_2$ then 
$ForgetLit(ForgetLit(\Sigma,l_1),l_2)$
$= \Sigma_{l_1 \leftarrow 1, l_2 \leftarrow 1} 
\vee (\neg l_1 \wedge \Sigma)_{l_2 \leftarrow 1}
\vee (\neg l_2 \wedge \Sigma_{l_1 \leftarrow 1})
\vee (\neg l_1 \wedge \neg l_2 \wedge \Sigma)$
$\equiv  \Sigma_{l_1 \leftarrow 1, l_2 \leftarrow 1} 
\vee (\neg l_1 \wedge \Sigma_{l_2 \leftarrow 1})
\vee (\neg l_2 \wedge \Sigma_{l_1 \leftarrow 1})
\vee (\neg l_1 \wedge \neg l_2 \wedge \Sigma)$
is symmetric in $l_1$ and $l_2$;
\item if $l_2 = \neg l_1 = \neg l$ then 
$ForgetLit(ForgetLit(\Sigma,l),\neg l)$
$= (\Sigma_{l \leftarrow 1} \vee (\neg l \wedge \Sigma_{l \leftarrow 0}))_
{l \leftarrow 0} \vee (l \wedge 
(\Sigma_{l \leftarrow 1} \vee (\neg l \wedge \Sigma_{l \leftarrow 0}))_
{l \leftarrow 0})$
$\equiv \Sigma_{l \leftarrow 1} \vee \Sigma_{l \leftarrow 0}$
is symmetric in $l$ and $\neg l$;
\item the case $l_1 = l_2$ is trivial.
\end{enumerate}
}. We can also prove that the definition above is equivalent to the
one in which Point~2. is replaced by

\[
ForgetLit(\Sigma, \{l\}) =
\Sigma_{l \leftarrow 1} \vee (\neg l \wedge \Sigma_{l \leftarrow 0})
\]
\noindent just because $\Sigma$ and $\Sigma_{l \leftarrow 0}$ are equivalent modulo
$\neg l$.

Let us now give a semantical characterization of literal forgetting. If
$L=\{l\}$, that is, $L$ is composed of a single literal, then forgetting $l$
from a formula $\Sigma$ amounts to introducing the model $Force(\omega,\neg l)$ for
each model $\omega$ of $\Sigma$ such that $\omega \models l$.

\begin{prop}
\label{sema-lite-forg}

The set of models of $ForgetLit(\Sigma,\{l\})$ can be expressed 
as:\eatpar

\begin{eqnarray*}
Mod(ForgetLit(\Sigma,\{l\})) 
&=&
Mod(\Sigma) \cup \{ Force(\omega,\neg l) ~|~ \omega \models \Sigma \} \\
&=&
\{ \omega ~|~ Force(\omega,l) \models \Sigma \}
\end{eqnarray*}

\end{prop}

A similar statement can be given for the case in which $L$ is composed of more
than one literal. In this case, for each model $\omega$ of $\Sigma$, we can force any
subset of literals $L_1 \subseteq L$ such that $\omega \models L_1$ to assume the value
false.

\begin{prop}
\label{sema-lits-forg}

The set of models of $ForgetLit(\Sigma,L)$ can be expressed as:\eatpar

\[
Mod(ForgetLit(\Sigma,L)) =
\{ \omega ~|~ Force(\omega,L_1) \models \Sigma \mbox{ where } L_1 \subseteq L \}
\]

\end{prop}

As a corollary, we obtain the following properties of literal forgetting:

\begin{corollary}~\label{coro-forget}
Let $\Sigma$, $\Phi$  be formulas from $PROP_{PS}$ and 
$L_1, L_2 \subseteq L_{PS}$.\eatpar

\begin{itemize}

\item $\Sigma \models ForgetLit(\Sigma, L_1)$ holds.

\item If $\Sigma \models \Phi$ holds, then $ForgetLit(\Sigma, L_1) \models
ForgetLit(\Phi, L_1)$ holds as well.

\item If $L_1 \subseteq L_2$ holds, then $ForgetLit(\Sigma, L_1) \models
ForgetLit(\Sigma, L_2)$ holds as well.

\end{itemize}

\end{corollary}

Let now consider an example.

\begin{example}

Let $\Sigma = (\neg a \vee b) \wedge (a \vee c)$. 
We have $ForgetLit(\Sigma, \{\neg a\}) \equiv (a \vee c) \wedge (b \vee c)$.

\end{example}


The key proposition for the notion of forgetting is the following one:

\begin{prop}\label{keyforget}

Let $\Sigma$  be a formula from $PROP_{PS}$ and $L \subseteq L_{PS}$.
$ForgetLit(\Sigma, L)$ is the logically strongest consequence of $\Sigma$ that is
Lit-independent from $L$ (up to logical equivalence).

\end{prop}


The following immediate consequence of
Proposition~\ref{keyforget} establishes strong relationships
between literal forgetting and Lit-independence:

\begin{corollary}
Let $\Sigma$  be a formula from $PROP_{PS}$ and $L \subseteq L_{PS}$.
$\Sigma$ is Lit-independent from $L$ if and only if 
$\Sigma \equiv ForgetLit(\Sigma, L)$ holds.
\end{corollary}

The following one gives an immediate application of literal
forgetting:\eatpar

\begin{corollary}
If a formula $\varphi$ is Lit-independent from $L$,
then $\Sigma \models \varphi$ holds
if and only if
\mbox{$ForgetLit(\Sigma,L) \models \varphi$}.
\end{corollary}

This result proves that forgetting literals from $L$ does not affect
entailment of formulas that are Lit-independent from $L$. This is in some sense
analogous to the concept of filtration in modal logics \cite{gold-87}; indeed,
if we are interested in knowing whether $\Sigma \models \varphi$ only for
formulas $\varphi$ that are Lit-independent from $L$, then the literals of $L$ can
be forgotten in $\Sigma$. 

Let us now investigate the computation of $ForgetLit(\Sigma, L)$.
Let us first consider DNF formulas $\Sigma$.
Forgetting literals within DNF formulas is a computationally easy task. On the one hand,
forgetting literals within a disjunctive formula comes down to
forgetting them in every disjunct:

\begin{prop}~\label{forget-or}
Let $\Sigma$, $\Phi$  be two formulas from $PROP_{PS}$ and $L \subseteq L_{PS}$.
$$ForgetLit(\Sigma \vee \Phi,L) \equiv ForgetLit(\Sigma, L) \vee
ForgetLit(\Phi, L).$$
\end{prop}


On the other hand, forgetting literals within a consistent term simply consists in 
removing them from the term:

\begin{prop}~\label{forgetterms}
Let $\gamma$ be a consistent term from $PROP_{PS}$ (viewed as the set
of its literals) and $L \subseteq L_{PS}$.
$ForgetLit(\gamma, L) \equiv \bigwedge_{l \in \gamma \setminus L} l$.
\end{prop}

Combining the two previous propositions shows how literals can be
forgotten from a DNF formula $\Sigma$ in polynomial time.
It is sufficient to delete every literal of $L$ from each disjunct 
of $\Sigma$ (if one of the disjuncts becomes empty then $ForgetLit(\Sigma,L) \equiv true$). 

Things are more complicated for conjunctive formulas $\Sigma \wedge \Phi$. Especially,
there is no result similar to Proposition \ref{forget-or} for conjunctive formulas.
While $ForgetLit(\Sigma, L) \wedge ForgetLit(\Phi, L)$ is a logical consequence
of $ForgetLit(\Sigma \wedge \Phi, L)$ (see Corollary \ref{coro-forget}), 
the converse does not hold in the general case.

\begin{example}
Let $\Sigma = a$, $\Phi = \neg a$, and $L = \{a\}$.
Since $a \not \leadsto \Phi$, we have $ForgetLit(\Phi, L) \equiv \Phi$.
Since $ForgetLit(\Sigma, L)$ is valid, we have
$(ForgetLit(\Sigma, L) \wedge ForgetLit(\Phi, L)) \equiv \neg a$.
Since $\Sigma \wedge \Phi$ is inconsistent, $ForgetLit(\Sigma \wedge \Phi, L)$
is inconsistent as well. 
\end{example}


Clearly enough, any non-valid clause $\delta$ is Lit-independent from $L$ 
if and only if $Lit(\delta) \cap L = \emptyset$. Since the conjunction of 
two formulas that are Lit-independent from $L$ is Lit-independent from $L$ 
(see Proposition \ref{PropFLI}), and since every formula is equivalent to a 
CNF formula, Proposition \ref{keyforget} shows
$ForgetLit(\Sigma, L)$ equivalent to the set of all clauses $\delta$ 
that are entailed by $\Sigma$ and are from $\{\delta$ clause $| 
\ Lit(\delta) \cap L = \emptyset\}$.
Because $\{\delta$ clause $| \ Lit(\delta) \cap L = \emptyset\}$ is closed under
subsumption (i.e., it is a stable production field), it is possible to take advantage
of consequence finding algorithms (see \citeR{Marquis00}), to derive a CNF representation 
of $ForgetLit(\Sigma, L)$. Especially, in the case where $\Sigma$ is a CNF formula,
resolution-based consequence finding algorithms like those reported in \cite{Inoue92} or
\cite{DelVal99} can be used; this is not very surprising since resolution is nothing
but {\em variable elimination}.

In contrast to the disjunctive formulas situation, there is no guarantee that
such consequence-finding algorithms run in time polynomial in the input size
when the input is a conjunctive formula (otherwise, as explained in the
following, we would have {\sf P} = {\sf NP}).
Nevertheless, forgetting literals within a conjunctive formula $\Sigma$ can be easy
in some restricted cases, especially when $\Sigma$ is given by the set of its prime 
implicates; in this situation, it is sufficient to give up those clauses containing a literal from $L$.

\begin{prop}~\label{forget-IP}
Let $\Sigma$  be a formula from $PROP_{PS}$ and $L \subseteq L_{PS}$.
$$IP(ForgetLit(\Sigma, L)) = \{\delta \ | \ \delta \in IP(\Sigma)~ and~
Lit(\delta) \cap L = \emptyset\}.$$
\end{prop}

The notion of literal forgetting generalizes the notion of variable elimination from
propositional logic (that was already known by Boole as elimination of middle terms
and has been generalized to the first-order case in a more recent past by
\citeR{LinReiter94}).
Indeed, variable elimination is about {\em variable
forgetting}, i.e., the one achieved not considering the literals signs:

\begin{defin}[variable forgetting]\label{defvf}

Let $\Sigma$  be a formula from $PROP_{PS}$ and let $V$ be a subset of $PS$.
$ForgetVar(\Sigma, V)$ is the formula inductively defined as follows:\eatpar

\begin{itemize}
\item $ForgetVar(\Sigma, \emptyset) = \Sigma$,
\item $ForgetVar(\Sigma, \{x\}) = \Sigma_{x \leftarrow 1} 
\vee \Sigma_{x \leftarrow 0}$,
\item $ForgetVar(\Sigma, \{x\} \cup V) = ForgetVar(ForgetVar(\Sigma, V), \{x\})$.
\end{itemize}

\end{defin}

\begin{example}
Let $\Sigma = (\neg a \vee b) \wedge (a \vee c)$. 
We have $ForgetVar(\Sigma, \{a\}) \equiv (b \vee c)$.
\end{example}

As a direct consequence of the definition, $ForgetVar(\Sigma, \{x_1, ..., x_n\})$
is equivalent to the quantified boolean formula (usually with free variables!)
denoted $\exists x_1 \ldots \exists x_n \Sigma$.

Clearly enough, forgetting a variable $x$ amounts to forgetting
both the literals $x$ and $\neg x$.

\begin{prop}~\label{forgetvar-forgetlit}
Let $\Sigma$  be a formula from $PROP_{PS}$ and $V \subseteq PS$.
We have\eatpar

\[
ForgetVar(\Sigma, V) \equiv ForgetLit(\Sigma, L_V)
\]

\end{prop}

This result, together with the previous results on literal forgetting,
gives us the following corollaries for variable forgetting:

\begin{corollary}
\begin{eqnarray*}
Mod(ForgetVar(\Sigma,\{x\})) 
&=&
Mod(\Sigma) \cup \{ Switch(\omega,x) ~|~ \omega \models \Sigma \}.
\end{eqnarray*}
\end{corollary}


\begin{corollary}\label{keyforgetvar}
Let $\Sigma$  be a formula and $V \subseteq PS$.
$ForgetVar(\Sigma, V)$ is the logically strongest consequence of $\Sigma$ that is
Var-independent from $V$ (up to logical equivalence).
\end{corollary}

\begin{corollary}
If a formula $\varphi$ is Var-independent from $V$, then
$\Sigma \models \varphi$ if and only if
\mbox{$ForgetVar(\Sigma,V) \models \varphi$}.
\end{corollary}

A consequence of the latter result is that forgetting variables is useful when
only a subset of variables are really used in the queries. Thus, if $\Sigma$
represents some pieces of knowledge about a scenario of interest, and we are
interested in knowing whether a fact $\varphi$ is true in the scenario, the
logical operation to do is to query whether $\Sigma \models \varphi$. Now, if
the possible facts $\varphi$ we are interested in do not involve some variables
$V$, then these variables can be forgotten from $\Sigma$, as querying
whether $\varphi$ is implied can be done on $ForgetVar(\Sigma, V)$ instead of
$\Sigma$.

Through the previous proposition, some algorithms for forgetting variables can
be easily derived from algorithms for forgetting literals (some of them have
been sketched before).  Specifically, polynomial time algorithms for forgetting
variables within a DNF formula or a formula given by the set of its prime
implicates can be obtained.  Other tractable classes of propositional formulas
for variable forgetting exist.  For instance, taking advantage of the fact that
$ForgetVar(\Sigma \wedge \Phi, V) \equiv ForgetVar(\Sigma, V) \wedge
ForgetVar(\Phi, V)$ whenever $Var(\Sigma) \cap Var(\Phi) = \emptyset$ holds,
\citeA{Darwiche99} showed that variable forgetting in a formula
$\Sigma$ can be done in linear time as soon as $\Sigma$ is in {\em Decomposable
Negation Normal Form} (DNNF), i.e., a (DAG)NNF formula in which the conjuncts
of any conjunctive subformula do not share any variable.  Interestingly, the
DNNF fragment of propositional logic is strictly more succinct than the DNF one
(especially, some DNNF formulas only admit exponentially-large equivalent DNF
formulas) \cite{DarwicheMarquis01}.

In the general case, just as for the literal situation,
there is no way to forget efficiently (i.e., in polynomial time) a set of variables within a 
formula (unless {\sf P} = {\sf NP}). Nevertheless, the following
decomposition property can be helpful in some situations (actually, it is heavily
exploited in \citeR{Kohlasetal99}).

\begin{prop}~\label{forg-and-ind}
Let $\Sigma$, $\Phi$ be two formulas from $PROP_{PS}$, and
$V$ be a subset of $PS$. If $V \not \leadsto_{-}^{+} \Sigma$, then $ForgetVar(\Sigma \wedge
\Phi, V) \equiv \Sigma \wedge ForgetVar(\Phi, V)$.
\end{prop}

Note that the corresponding property for literal forgetting does not hold
(as a previous example shows).


Forgetting literals or variables proves helpful in various settings
(we already sketched some of them in the introduction). For
instance, minimal model inference (or circumscription \citeR{McCarthy86}) can 
be expressed using literal forgetting (but not directly using
variable forgetting, which shows the interest of the more general form
we introduced). Indeed, it is well-known
that closed world inference from a knowledge base $\Sigma$ can be 
logically characterized as classical entailment from $\Sigma$ completed
with some assumptions. In the circumscription framework \cite{McCarthy86}, given a partition
$\langle P, Q, Z\rangle$ of $PS$, such assumptions are the negations
of the formulas $\alpha$ s.t. $\alpha$ does not contain any variable from $Z$
and for every clause $\gamma$ containing only positive literals built up from $P$
and literals built up from $Q$, if $\Sigma \not \models \gamma$ holds, then
$\Sigma \not \models \gamma \vee \alpha$ holds as well. 
Equivalently, $\neg \alpha$ is considered a reasonable assumption whenever
it is (syntactically) Var-independent from $Z$ and expanding $\Sigma$ with it
does not modify what is already known about $L_P^+ \cup L_Q$.
Clearly enough, the signs of literals from $L_P$ really matter here.
Using our previous notations, $\neg \alpha$ is assumed if and only if
$Z \not \leadsto_{-}^{+} \neg \alpha$ and $\Sigma \equiv_{L_P^+ \cup L_Q} 
\Sigma \wedge \neg \alpha$. As a consequence, we derive the following
characterization of circumscription:

\begin{prop}~\label{circ}
Let $\Sigma$, $\Phi$  be two formulas from $PROP_{PS}$, and $P$, $Q$, $Z$ be 
three disjoint sets of variables from $PS$ (such that $Var(\Sigma) \cup Var(\Phi) 
\subseteq P \cup Q \cup Z$).
It holds:\eatpar

\begin{itemize}
\item If $\Phi$ does not contain any variable from $Z$

\begin{eqnarray*}
& CIRC(\Sigma, \langle P, Q, Z\rangle) \models \Phi & \\
& \mbox{ ~~ if and only if ~~ } & \\
& \Sigma \models ForgetLit(\Sigma \wedge \Phi, L_P^- \cup L_Z) &
\end{eqnarray*}

\item In the general case:

\begin{eqnarray*}
& CIRC(\Sigma, \langle P, Q, Z\rangle) \models \Phi & \\
& \mbox{ ~~ if and only if ~~ }& \\
& \Sigma \models ForgetLit(\Sigma \wedge \neg ForgetLit(\Sigma 
\wedge \neg \Phi, L_Z \cup L_P^{-}), L_Z \cup L_P^{-}) &
\end{eqnarray*}
\end{itemize}

\noindent where $CIRC$ is circumscription as defined in \cite{McCarthy86}.

\end{prop}

Similar characterizations can be derived for the other forms of closed world reasoning
pointed out so far.

Forgetting also is a central concept when we are concerned with query answering
w.r.t. a restricted target language. Indeed, in many problems, there is a set
of variables for which we are not interested in their truth value (so we can
forget them).  For instance, in the SATPLAN framework by \citeA{Kautzetal96}, 
compiling away fluents or actions amounts to forgetting
variables.  Since the only variables we are really interested in within a given
set of clauses representing a planning problem instance are those representing
the plans, we can compile away any other variable, if this does not introduce
an increase of size of the resulting formula.  Another situation where such a
forgetting naturally occurs is model-based diagnosis \cite{Reiter87}; compiling
away every variable except the abnormality ones does not remove any piece of
information required to compute the conflicts and the diagnoses of a system.
Thus, \citeA{Darwiche98} shows how both the set of conflicts and the
set of consistency-based diagnoses of a system is characterized by the formula
obtained by forgetting every variable except the abnormality ones in the
conjunction of the system description and the available observations. Provided
that the system description has first been turned into DNNF, forgetting can be
achieved in linear time and diagnoses containing a minimal number of faulty
components can be enumerated in (output) polynomial time. Interestingly, this
work shows that the diagnosis task does not require the (usually expensive)
computation of prime implicates/implicants to be achieved (actually, computing
prime implicates/implicants is just a {\it way} to achieve variable
forgetting and not a {\it goal} in consistency-based diagnosis).
Forgetting every variable from a formula allows for consistency checking
since $\Sigma$ is consistent if and only if $ForgetVar(\Sigma, Var(\Sigma))$ is
consistent.  The well-known Davis and Putnam algorithm for satisfiability
testing \cite{DavisPutnam60} (recently revisited by \citeA{DechterRish94}under the
name directional resolution) basically consists in
computing a clausal representation of $ForgetVar(\Sigma, Var(\Sigma))$ from a
CNF $\Sigma$ using resolution; if the empty clause is not generated, then
$\Sigma$ is consistent and the converse also holds.


Forgetting can also be used as a key concept in order to organize knowledge so as to
replace one global inference into a number of local inferences as shown (among others) by
\citeA{Kohlasetal99} and \citeA{AmirMcIlraith00,McIlraithAmir01}. 
Loosely speaking, such approaches rely on the idea that
exploiting all the pieces of information given in a knowledge base is typically 
not required for query answering. Focusing on what is relevant to the query is
sufficient. While such techniques do not lower the complexity of inference 
from the theoretical side, they can lead to significant practical improvements.
For instance, assume that $\Sigma$ consists of three formulas $\Phi_1$, $\Phi_2$, and 
$\Phi_3$. For any query $\Psi$, let $V_{\Psi} = (\bigcup_{i=1}^3 Var(\Phi_i)) 
\setminus Var(\Psi)$. We have $\Sigma \models \Psi$ 
if and only if $ForgetVar(\bigwedge_{i=1}^3 \Phi_i, V_{\Psi}) \models \Psi$.
If $Var(\Phi_3) \cap (\bigcup_{i=1}^2 Var(\Phi_i)) = \emptyset$, this amounts to test
{\em independently} whether $ForgetVar(\bigwedge_{i=1}^2 \Phi_i, V_{\Psi}) \models \Psi$ holds or
$ForgetVar(\Phi_3, V_{\Psi}) \models \Psi$ holds. This way, one global inference is replaced
by two local inferences. Now, $ForgetVar(\Phi_1 \wedge \Phi_2, V_{\Psi})$ is 
equivalent to $ForgetVar(\Phi_1 \wedge 
ForgetVar(\Phi_2, V_{\Psi} \cap (Var(\Phi_2) \setminus Var(\Phi_1))), V_{\Psi})$.
Accordingly, every variable from $\Phi_2$ that is not a variable of $\Phi_1$ or a variable
of $\Psi$ can be forgotten first within $\Phi_2$ because it gives no information relevant to
the query; thus, only a few pieces of knowledge have to be ``propagated'' from
$\Phi_2$ to $\Phi_1$ before answering the query, and forgetting allows for characterizing
them exactly. 

As evoked in the introduction, another scenario in which 
forgetting is useful is that of belief update. Indeed,
there are many formalizations of belief update that are based on a form of
variable forgetting. The basic scenario is the following one: we have a formula
$\Sigma$ that represents our knowledge; there are some changes in the world,
and what we know is that after them a formula $\varphi$ becomes true. The simplest
way to deal with the update is to assume that $\varphi$ represents all we know
about the truth value of the variables in $\varphi$. As a result, we have to
``forget'' from $\Sigma$ the value of the variables in $Var(\varphi)$. There are
different formalizations of this schema, based on whether formula $\varphi$ is
considered to carry information about variables it mentions \cite{Winslett90} or
only on the variables it depends on \cite{Hegner87}, or also on variables
related to dependent variables via a dependence function \cite{Herzig96}. This
kind of update schema, while less known than the Possible Models Approach
by \citeA{Winslett90}, has proved to be suited for reasoning about 
actions \cite{Dohertyetal98,Herzigetal99}.
Furthermore, the possibility to forget literals (and not variables) is also
valuable in this framework to take account for persistent information, 
as shown recently by some of us \cite{HerzigLangMarquisPolacsek01}, since the
polarity of information is often significant. For instance, while forgetting
the fluent $alive$ from a knowledge base is not problematic, forgetting
the persistent fluent $\neg alive$ would surely be inadequate.


Forgetting can also be used to characterize a dependence relation called
definability \cite{LangMarquis98b} as well as the strongest necessary (resp.
weakest sufficient) conditions of a propositional variable on a set $V$ of
variables given a theory $\Sigma$ \cite{Lin00,Dohertyetal01}. As shown
in \cite{LangMarquis98b,Lin00,Dohertyetal01}, all these notions
have many applications in various AI fields, including hypothesis
discrimination, agent communication, theory approximation and abduction.


Finally, based on literal and variable forgetting, valuable equivalence
relations over formulas can also be defined:

\begin{defin}[Lit-equivalence, Var-equivalence]\label{defequiv}
Let $\Sigma$, $\Phi$ be two formulas from $PROP_{PS}$, $L$ be a subset of $L_{PS}$, and
$V$ be a subset of $PS$.
\begin{itemize}
\item $\Sigma$ and $\Phi$ are said to be {\em Lit-equivalent} given $L$, denoted $\Sigma \equiv_L \Phi$, if and only if\\
$ForgetLit(\Sigma, Lit(\Sigma) \setminus L) \equiv ForgetLit(\Phi, Lit(\Phi) \setminus L)$.
\item $\Sigma$ and $\Phi$ are said to be {\em Var-equivalent} given $V$, denoted $\Sigma \equiv_V \Phi$, if and only if\\
$ForgetVar(\Sigma, Var(\Sigma) \setminus V) \equiv ForgetVar(\Phi, Var(\Phi) \setminus V)$.
\end{itemize}
\end{defin}

\begin{example} 
Let $\Sigma = (a \Rightarrow b) \wedge (b \Rightarrow c)$ and
$\Phi = (a \Rightarrow d) \wedge (d \Rightarrow c)$. Let $L = \{\neg a, c\}$.
$\Sigma$ and $\Phi$ are Lit-equivalent given $L$.
\end{example}

Such equivalence relations capture some forms of dependence between formulas.
They are useful in the various situations where it is required to formally
characterize the fact that two knowledge bases share some theorems. Thus, two
formulas are Lit-equivalent given $L$ whenever every clause containing literals
from $L$ only is a logical consequence of the first formula if and only if it
is a logical consequence of the second formula.  In the same vein, two
Var-equivalent formulas given $V$ have the same clausal consequences built up
from $V$. Clearly, Lit-equivalence is more fine-grained than Var-equivalence in
the sense that two formulas Var-equivalent given $V$ are also Lit-equivalent
given $L = L_V$, the set of literals built upon $V$, but the converse does not
hold in the general case.  Some applications are related to knowledge
approximation ($\Phi$ is a correct approximation of $\Sigma$ over $L$ if and
only if $\Phi$ and $\Sigma$ are Lit-equivalent given $L$), normalization
(turning a formula $\Sigma$ into a CNF $\Phi$ by introducing new symbols is
acceptable as long as the two formulas are equivalent over the original
language, i.e., $\Sigma$ and $\Phi$ are Var-equivalent given $V =
Var(\Sigma)$), and so on.

\subsection{Complexity Results}

It is quite easy to prove that forgetting is a computationally
expensive operation in the general case. Indeed, since a formula
$\Sigma$ is consistent if and only if $ForgetLit(\Sigma, Lit(\Sigma))$ 
is consistent and since the latter formula is Lit-independent from
every literal (i.e., it is equivalent to $true$ or equivalent to $false$),
there is no way to compute a formula $\Phi$ equivalent to 
$ForgetLit(\Sigma, L)$ in polynomial time, unless {\sf P} = {\sf NP}.
Actually, we can derive the more constraining result, showing that
the {\em size} of any formula equivalent to $ForgetLit(\Sigma, L)$ may be
superpolynomially larger than the size of $\Sigma$.

\begin{prop}~\label{forget-not-polsize}
Let $\Sigma$ be a formula from $PROP_{PS}$ and
let $L$ be a finite subset of $L_{PS}$.
In the general case, there is no propositional formula $\Phi$
equivalent to $ForgetLit(\Sigma, L)$ s.t. the size of $\Phi$ is
polynomially bounded in $|\Sigma|+|L|$, unless {\sf NP} $\cap$ {\sf coNP}
$\subseteq$ {\sf P/poly} (which is considered unlikely in complexity theory).
\end{prop}

This result shows that computing an explicit representation of
$ForgetLit(\Sigma, L)$ under the form of a propositional formula
is hard, even in a compilation-based approach where the time needed
to derive such a formula is neglected.

Finally, we have also derived:

\begin{prop}[complexity of Lit/Var-equivalence]~\label{comp-LVequivalence}\\
{\sc Lit-equivalence} and {\sc Var-equivalence} are $\Pi_2^p$-complete.
\end{prop}

\section{Influenceability, Relevance, and Strict Relevance}\label{other}

In this section, we show that several notions of dependence
introduced in the literature are equivalent to, or can
be expressed in terms of, semantical independence.
In particular, we show that Boutilier's definition of
influenceability \cite{Boutilier94} is in fact
equivalent to (semantical) FV-dependence. The definition of relevance
as given by \citeA{Lakemeyer97} can also be proved to
be equivalent to FV-dependence. One of the two definitions
given by \citeA{Lakemeyer97} for strict relevance
can also be expressed in terms of FV-dependence. These
results allow for finding the complexity of all these
forms of dependence as a direct corollary to the complexity results
reported in the previous section. For the sake of completeness,
we also give the complexity of the original definition of 
strict relevance \cite{Lakemeyer95} (which is not directly related
to FV-dependence), which turns out to be computationally
simpler than the subsequent definition given by
\citeA{Lakemeyer97}.


\subsection{Influenceability}

\citeA{Boutilier94} introduces a notion of
influenceability. Roughly speaking, a formula $\Sigma$
is influenceable from a set of variables $V$ if there
exists a scenario in which the truth value of $\Sigma$
depends on the value of the variables in $V$. 
This idea can be formalized as follows.

\begin{defin}[influenceability]\label{definflu}

Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is {\em influenceable} from $V$ if and only if there exists
a $PS \setminus V$-world $\omega$, and two $V$-worlds $\omega_1$
and $\omega_2$ s.t. $\omega \wedge \omega_1 \models \Sigma$ and
$\omega \wedge \omega_2 \models \neg \Sigma$ hold.
\end{defin}

In other words, there is a scenario $\omega$ in which the
formula $\Sigma$ can be true or false, depending on the
value of the variables in $V$. While influenceability looks
different from the definitions given in this paper, it can
be shown that in fact influenceability coincides with
FV-dependence.

\begin{prop}~\label{infl}
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is influenceable from $V$ if and only if $\Sigma$ is Var-dependent on $V$.
\end{prop}


As a consequence, a model-theoretic characterization of influenceability 
can be easily derived from the one for FV-independence. The complexity
of influenceability is an easy corollary to this property: 
{\sc influenceability} is {\sf NP}-complete.

\subsection{Relevance}

\citeA{Lakemeyer95,Lakemeyer97} introduces
several forms of relevance. We show how these forms of relevance
are strongly related to FV-independence.
We also complete the results given in \cite{Lakemeyer97}, by
exhibiting the computational complexity of each form of relevance
introduced in \cite{Lakemeyer97}.

\subsubsection{Relevance of a formula to a subject matter}

Lakemeyer's notion of relevance of a formula to a subject matter
can be defined in terms of prime implicates of the formula,
as follows (see Definition 9 in \citeR{Lakemeyer97}):

\begin{defin}[relevance to a subject matter]\label{defrsm}
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is {\em relevant to} $V$ if and only if there exists a prime implicate of
$\Sigma$ mentioning a variable from $V$.
\end{defin}

\begin{example}
Let $\Sigma = (a \wedge c)$ and $V = \{a, b\}$. $\Sigma$ is relevant to $V$.
\end{example}

As a consequence, Lakemeyer's notion of irrelevance of a formula to a subject matter
coincides with FV-independence.

\begin{prop}~\label{rtsm}
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is relevant to $V$ if and only if $\Sigma$ is Var-dependent on $V$.
\end{prop}

Thus, the model-theoretic characterization of FV-independence also applies to
irrelevance of a formula to a subject matter. We also have that the 
irrelevance of a formula to a subject matter coincides with Boutilier's 
definition of influenceability. Finally, the above proposition allows for an 
easy proof of complexity for relevance, namely, 
{\sc relevance of a formula to a subject matter} is 
{\sf NP}-complete.


\subsubsection{Strict relevance of a formula to a subject matter}

Lakemeyer has introduced two forms of {\em strict relevance}. The 
(chronologically) first one has been given in \cite{Lakemeyer95},
as follows.

\begin{defin}[strict relevance to a subject matter, \citeR{Lakemeyer95}]\label{defsrsm}

Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is {\em strictly relevant to} $V$
if and only if every prime implicate of $\Sigma$ contains a variable from $V$.

\end{defin}

Lakemeyer has also introduced another notion of strict relevance
\cite{Lakemeyer97}, more demanding than the original one. Here we 
consider an equivalent definition.

\begin{defin}[strict relevance to a subject matter, \citeR{Lakemeyer97}]

Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is {\em strictly relevant to} $V$ 
if and only if there exists a prime implicate of $\Sigma$ mentioning a variable from $V$,
and every prime implicate of $\Sigma$ mentions only variables from $V$.

\end{defin}


Both definitions prevent tautologies and contradictory formulas from being
strictly relevant to any set of variables.
The basic difference between these two definitions is that in the first one we want that
every prime implicate of $\Sigma$ contains {\em at least} a variable from $V$,
while in the second case we impose that every prime implicate of $\Sigma$ must
contain {\em only} variables from $V$%
\footnote{Strict relevance as in \cite{Lakemeyer97} could also be shown to be
strongly related to controllability \cite{Boutilier94,LangMarquis98b}.}.
As the following example shows, there are formulas for which the two
definitions of strict relevance do not coincide.

\begin{example}

Let $\Sigma = (a \vee b)$ and $V=\{a\}$. There is only one prime implicate of
$\Sigma$, namely $a \vee b$. Since it contains at least a variable of $V$, it
follows that $\Sigma$ is strictly relevant to $V$ w.r.t.\  \cite{Lakemeyer95}.
However, since the prime implicate $a \vee b$ is not composed {\em only of}
variables of $V$ (because $b \not\in V$), it follows that $\Sigma$ is not
strictly relevant to $V$ w.r.t.\  \cite{Lakemeyer97}.

\end{example}

\iffalse

\begin{example}

Let $\Sigma = (a \wedge c)$. $\Sigma$ is strictly relevant to $\{a, b, c\}$
but is not strictly relevant to $\{a, b\}$.

\end{example}

\fi

Through FV-independence, we can derive an alternative characterization of the
notion of {\em strict relevance} introduced by \citeA{Lakemeyer97}.
Indeed, as a straightforward consequence of the definition, we have:

\begin{prop}~\label{srsm1}
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is strictly relevant to $V$ if and only if 
$\Sigma$ is Var-dependent on $V$ and Var-independent from 
$Var(\Sigma) \setminus V$.
\end{prop}

We have identified the complexity of both definitions of strict relevance, and
they turn out to be different: the first definition is harder than the
second one.

\begin{prop}[complexity of strict relevance]~\label{comp-strict-rel}\\
(1) {\sc strict relevance 
of a formula to a subject matter} \cite{Lakemeyer95} is\\ 
$\Pi_2^p$-complete.\\
(2) {\sc strict relevance 
of a formula to a subject matter} \cite{Lakemeyer97} is \bh2-complete.
\end{prop}

These complexity results improve Theorem 50 from \cite{Lakemeyer97},
which only
points out the \np-hardness of irrelevance and strict irrelevance as defined
in \cite{Lakemeyer97}.


\section{Other Related Work and Further Extensions}\label{related}
In this section, we first discuss other related work, then
some possible extensions of the notions and results we have
presented before.

\subsection{Other Related Work}

As already evoked, independence has been considered under various
forms in various AI fields.

\subsubsection{Independence in propositional logic}
There are other forms of independence in propositional logic that we have not
considered in this article, especially, definability, controllability
\cite{LangMarquis98b} as well as conditional independence 
\cite{Darwiche97}. If $X$, $Y$ and $Z$ are three disjoint sets of variables
and $\Sigma$ is a knowledge base then  $X$ and $Y$ are conditionally 
independent w.r.t. $Z$ knowing $\Sigma$ if and only if for any $Z$-world 
$\omega_Z$, once we know $\omega_Z$ (and $\Sigma$), learning something
about $X$ cannot make us learn anything new about $Y$ 
(and {\em vice versa}). The computational issues pertaining to conditional
independence and to stronger notions as well as related notions such
as relevance between subject matters \cite{Lakemeyer97} and novelty
\cite{GreinerGenesereth83}, have been extensively
studied in a companion paper \cite{LangLiberatoreMarquis02}.

\subsubsection{Implicit and explicit dependence}
Several approaches to belief change make use of a explicit dependence 
relation, which means that it is part of the input (while ours is implicit, 
i.e., derived from the input). 
Thus, computing independence relations from a knowledge base can be
seen as an upstream task enabling us to specify the ``core'' (minimal)
independence relation upon which the belief change operator is based; 
this core independence relation can then be completed by specifying
explicitly some additional dependencies using knowledge about the domain. 
Such an approach has been  proposed for belief revision in
\cite{FarinasHerzig96}, for belief update in \cite{Marquis94}
and \cite{Herzig96} and for reasoning about action in \cite{Herzigetal99}.

\subsubsection{Independence and contexts}

Contextual reasoning \cite{ghid-giun-01}
has been introduced for formalizing domains
in which knowledge can naturally be divided
into parts (contexts). Each context is
characterized by its own language and alphabet.
The knowledge base of a context contains what
is relevant to a part of the domain. However,
it is not guaranteed that the different parts
of the domain do not interact, so inference in
one context may be affected by the knowledge of
some other context. 

The main difference between contextual reasoning
and independence is that the latter is a study
of the relevance relation that can be drawn from
a ``flat'' (i.e.,  not divided into contexts)
knowledge base; whereas contextual reasoning is
on knowledge about specific contexts, that is,
knowledge is expressed by specifying which context
it refers to. In other words, the relevance relation
is a result of reasoning about knowledge in studying
dependency; on the other hand, it is one of the
data that has to be provided for reasoning about
contexts.

\subsubsection{The definition of irrelevance by Levy et al.}

The definition of irrelevance given by
\citeA{levy-etal-97} aims at
establishing which facts of a knowledge base are
irrelevant to the derivation of a query. In
particular, they consider a first-order logic
with no function symbols and a set of inference
rules. A knowledge base is a set of closed formulas
(formulas with no free variables). Derivation of
a query (another closed formula) is obtained by
applying the inference rules to the knowledge
base and the logical axioms of the theory.

A formula $\phi$ of the knowledge base is irrelevant
to the derivation of another formula $\psi$ if $\phi$
does not ``participate'' to the process of inferring
$\psi$ from the knowledge base. For example, in the
knowledge base $\{ A(1), C(2), A(X) \Rightarrow B(X) \}$, it
is clear that $A(1)$ is relevant to $B(1)$, while
$C(2)$ is not.

This definition becomes complicated when more complex
scenarios are considered. Namely, Levy et al. consider
three different ``coordinates'': first, whether all
derivations are considered or just one; second, whether
we consider all derivations or just minimal ones; third,
whether we consider membership to the proof or just
derivability from the formulas that compose the proof
(in this case, we have four possible choices).

Besides the fact that this notion of irrelevance is
based on first-order logic, there are other, more
substantial, differences between it and the ideas
investigated in this paper. First, it is a relation
between two formulas, given a background knowledge
base. As such, it is more related to other notions
of relevance in the literature \cite{LangMarquis98a}.
Second, it is based on the concept of proof, which
is something not completely dependent on the semantics.
For example, replacing the usual modus ponens with
the strange inference rule
$\alpha, \beta, \alpha \Rightarrow \gamma  \rightarrow \gamma$, which does not
change the semantics of the logics, then the formula
$C(2)$ of the knowledge base above becomes magically
relevant to $B(1)$. This is perfectly reasonable in
the approach by Levy et al., where improving efficiency
using a specific proof theory is the aim.

\subsection{Extending our Notions and Results}

The notions and results presented in this paper can be extended
in several directions.

\subsubsection{Numerical and ordinal notions of formula-variable independence;
forgetting in more general structures}
It may be worth wondering about how the notions of FL-independence and
FV-independence can be generalized to the case where the knowledge base
is not a mere propositional formula but a probability distribution over
$\Omega_{PS}$, or an incomplete probability (or equivalently a set of
probability distributions), or a stratified knowledge base, or any other 
ordinal or numerical structure.

First, let us notice that some of our characterizations lead to quite 
intuitive and general ideas. To take the case of FV-independence,
we have shown that the following three statements are equivalent when
$\Sigma$ is a propositional knowledge base:\\
(a) $\Sigma$ does not tell anything about $x$, in any context;\\
(b) $\Sigma$ can be rewritten equivalently in a formula $\Sigma'$ in
which $x$ does not appear\\ 
(Definition~\ref{semfvindep});\\
(c) for any two interpretations $\omega$ and $\omega'$ that differ only in the
value given to $x$, the status of $\omega$  with respect to 
$\Sigma$ (i.e., model or countermodel) is the same as that
of $\omega'$ (Corollary~\ref{sema-inde-vars}).\\

\noindent As to variable forgetting: \\
(d) $ForgetVar(\Sigma,V)$ is the most general consequence of $\Sigma$ that 
is Var-independent from $V$ (Corollary~\ref{keyforget}).\\
Now, these definitions have a sufficient level of generality to be extended
to the case where the knowledge base $\Sigma$ is replaced by another 
structure.

Thus, some of us have extended the notion of Var-independence 
(characterized using (b)) and
variable forgetting to ordinal conditional functions (represented as
stratified bases) \cite{Langetal01}. The basic purpose was to
extend the ``forget and expand'' approach at work for updating ``flat'' knowledge bases
(as briefly discussed in Section \ref{forg})
to updating more sophisticated epistemic states.

The case of incomplete probabilities is also interesting since generalizing
(a), (b) and (c) will lead to the same intuitive notion 
\footnote{This is not the case for single probability distributions:
when the knowledge base is represented by a probability distribution $pr$,
(a) does not lead to an acceptable definition (because a full probability
distribution on $\Omega_{PS}$ always tell something about $x$); (c) suggests
the definition $\forall \omega \in \Omega_{PS}, pr(Switch(\omega,x)) = pr(\omega)$,
which leads to the decomposability of $pr$ w.r.t. $x$: $pr$ is a
joint probability distribution obtained from a probability distribution
$pr_{PS\setminus \{x\}}$ on $\Omega_{PS\setminus \{x\}}$ and the probability distribution
$pr_x$ on $\{x\}$ defined by $pr_x(x) = \frac{1}{2} (= pr_x(\neg x))$.
(b) would lead to the same definition, noticing that a full probability
distribution can be expressed more compactly by a ``partial'' probability
distribution (here, a probability distribution on $\Omega_{PS\setminus \{x\}}$)
from which $pr$ is induced by the maximum entropy principle.}.
As to variable forgetting, it is not hard to notice that it corresponds
to the well-known notion of {\em marginalization}.          

\subsubsection{Formula-variable independence in nonclassical (propositional)
logics}
The definition of FL- and FV-independence ($\Sigma$ can be rewritten 
equivalently in a formula $\Sigma'$ in which $l$ (resp. $x$) does not appear)
is quite general, in the sense that the logical language {\em and/or} the 
consequence relation (and thus the notion of logical equivalence) may vary, 
which enables us to draw from this principle notions of FL- and 
FV-independence (and from then on, notions of literal and variable forgetting) for 
nonclassical logics. This is what has been done (at least partly) in 
\cite{Lakemeyer97}. Here we briefly consider two cases:\\
(i) {\em subclassical logics}. These logics are built on a classical
language but have a weaker consequence relation than classical logic.
For instance, in most multivalued logics, due to the fact that the excluded 
middle $(a \vee \neg a)$ is not a theorem, a formula such as $a \vee (\neg b
\wedge b)$ will depend both on $a$ and on $b$ (whereas it depends 
only on $a$ in classical logic), because it cannot be rewritten
equivalently into a formula in which $b$ does not appear (in particular,
$a$ is not always equivalent to  $a \vee (\neg b \wedge b)$ in such logics); 
on the contrary, the formula $a \vee (a \wedge b)$ is equivalent to $a$ in
usual multivalued logics and thus depends on $a$ only.\\
(ii) {\em modal logics}. Now, the language is obtained by extending
a classical propositional language with one or more modalities,
while the consequence relation extends that of classical logic 
(in the sense that a modality-free formula is a theorem if and only if it is
a theorem of classical logic). Therefore, results such as
Propositions~\ref{deductionl} and ~\ref{deductionfv}
still make sense and we conjecture that they are still valid.
To take an example, in the logic $S5$ where $\square \Sigma \Rightarrow
\lozenge \Sigma$ is a theorem, a formula such as 
$\square \Sigma \wedge \lozenge (\Sigma \vee \Phi)$ is independent from $\Phi$
while $\lozenge \Sigma \wedge \square (\Sigma \vee \Phi)$ is not. 

\subsubsection{Restricted queries and characteristic models}

Forgetting a set of variables modifies a knowledge
base while preserving some of the consequences,
namely, those built on variables that are not forgotten.
Other frameworks are based on restricting the possible
queries in other ways, i.e., considering only
queries in Horn form \cite{kaut-kear-selm-95}.

Reasoning with characteristic models \cite{kaut-kear-selm-93}
is based on using only a subset of models of the original
formula. As for forgetting, this may increase the size of
the representation of a knowledge base exponentially.
\citeA{khar-roth-96} have shown that
characteristic models can be used for efficient reasoning
on some sets of restricted queries.

\section{Concluding Remarks}\label{concl}

We have investigated several ways of answering the key question of
determining what a propositional knowledge base tells about the 
(in)dependencies between variables and formulas. 
For each of the notions studied, we have related it to other
previously known notions and we have studied it from a computational
point of view, giving both complexity results and characterization 
results to be used for practical computation. In the light of our
results, it appears that  the various forms of logical independence 
are closely connected.
Especially, several of them had been proposed by different authors
without being explicitely related. Boutilier's influenceability and 
Lakemeyer's relevance of a formula to a subject matter are identical 
to FV-independence (Propositions~\ref{infl} and~\ref{rtsm}). 
We also discussed much related work, and suggest some extensions
to more general framework than mere propositional logic.

The following table gives a synthetic view of many notions addressed
in this paper and the corresponding complexity results.

\vspace{4mm}

\begin{tabular}{llll}
Problem &
Notation &
Definition &
Complexity\\
\hline
Synt. Lit-independence & 
&
$Lit(\Sigma) \cap L = \emptyset$ & {\sf P}
\\
Lit-independence &
$L \not\leadsto \Sigma$ &
$\exists \Phi ~.~ \Phi \equiv \Sigma ,~ Lit(\Phi) \cap L = \emptyset$ &
\conp-complete
\\
Dependent literals &
$DepLit(\Sigma)$ &
$\{ l ~|~ \{l\} \leadsto \Sigma \}$ &
$\mbox{{\sf BH}}_2$-complete
\\
FullLit-independence &
&
$L \subseteq DepLit(\Sigma)$ &
\conp-complete
\\
Lit-simplified &
&
$\forall l ~.~ \{l\} \not\leadsto \Sigma \Leftrightarrow l \not\in Lit(\Sigma)$ &
\np-complete
\\
Lit-equivalence &
$\Sigma \equiv_L \Phi$ &
$ForgetLit(\Sigma, Lit(\Sigma) \setminus L) \equiv$ \\
& & $ForgetLit(\Phi, Lit(\Phi) \setminus L)$ &
$\Pi_2^p$-complete
\\
\hline
\end{tabular}

\

\hfil Problems on literals and their complexity.\hfil

\

\begin{tabular}{llll}
Problem &
Notation &
Definition &
Complexity\\
\hline
Synt. Var-independence & 
&
$Var(\Sigma) \cap V = \emptyset$ & {\sf P}
\\
Var-independence &
$V \not\leadsto_-^+ \Sigma$ &
$\exists \Phi ~.~ \Phi \equiv \Sigma ,~ Var(\Phi) \cap \Sigma = \emptyset$ &
\conp-complete
\\
Dependent variables &
$DepVar(\Sigma)$ &
$\{ v ~|~ v \leadsto_-^+ \Sigma \}$ &
$\mbox{{\sf BH}}_2$-complete
\\
FullVar-independence &
&
$V \subseteq DepVar(\Sigma)$ &
\conp-complete
\\
Var-simplified &
&
$\forall v ~.~ \{v\} \not\leadsto_-^+ \Sigma \Leftrightarrow v \not\in Var(\Sigma)$ &
\np-complete
\\
Var-equivalence &
$\Sigma \equiv_V \Phi$ &
$ForgetVar(\Sigma, Var(\Sigma) \setminus V) \equiv$ \\
& & $ForgetVar(\Phi, Var(\Phi) \setminus V)$ &
$\Pi_2^p$-complete
\\
\hline
\end{tabular}

\

\hfil Problems on variables and their complexity.\hfil

\vspace{4mm}

The fact that both notions of formula-variable independence and forgetting
have been used as key concepts in many AI fields (including automated
reasoning, belief revision and update, diagnosis, reasoning about actions etc.)
has been discussed before (Sections \ref{intro} and \ref{forg}), so we will refrain from
repeating it here. The gain of generality offered by the corresponding
literal-oriented notions introduced in this paper has also been established
(e.g., Proposition \ref{forgetvar-forgetlit}), and their application to several AI problems
(like closed-world reasoning and belief update) has been sketched.

Primarily, one of the main motivations for the notions of formula-variable
independence and forgetting was to improve inference from a computational side, by enabling
to focus on relevant pieces of knowledge. The extent to which this goal can be reached
can be discussed at the light of our complexity results:
\begin{itemize}
\item {\em Most (in)dependence relations have a high complexity.}
The notions connected to FV-dependence 
(FL-dependence, full FV- and FL-dependence, influenceability, relevance
to a subject matter and strict relevance second form) have a complexity
at the first level of the polynomial hierarchy, which means that they can be 
checked by a satisfiability or/and an unsatisfiability solver. They become
``tractable'' when syntactical restrictions are made (Proposition~\ref{poly}).
Forgetting (literals or variables) also is computationally expensive.
The remaining notions are in
complexity classes located at the second level of the polynomial hierarchy.
Worse, under the standard assumptions of complexity theory, the 
explicit computation of literal or variable forgetting cannot be achieved
in polynomial space in the general case (Proposition \ref{forget-not-polsize}).
This pushes towards the negative conclusion that all these notions are hard to be computed
(at least in the worst case)
except if the size or the syntactical form of the input enables it.
The fact that these problems fall in the second level of the polynomial
hierarchy are not that surprising since this is where a large part
(if not the majority) of
important problems in knowledge representation\footnote{Such as 
abduction, nonmonotonic inference, belief revision,
belief update, some forms of planning and decision making.}
fall.
\item {\em But a high worst-case complexity does not necessarily prevent from
practical algorithms!}
Thus, Amir and McIlraith have shown the computational benefits that can be achieved 
by structuring a KB (through the forgetting operation) so as to achieve 
inference and consequence finding more efficiently \cite{AmirMcIlraith00,McIlraithAmir01}.
A similar discrepancy between the worst case situation and the practical ones
can be observed in other domains; especially,
satisfiability-based checkers for quantified boolean formulas \cite{Biereetal99,Williamsetal00} 
used for formal verification purposes (bounded model checking) exhibit
interesting computational behaviours (actually, they typically perform 
better than specialized algorithms, as shown in \citeR{Rintanen01}), despite the
fact that they are confronted to the problem of variable forgetting (i.e., elimination
of existentially quantified variables).
\item {\em Moreover, preprocessing may play an important role}.
What we mean with ``preprocessing'' refers to the
task of computing (in)dependence relations and forgetting {\em before} performing
more problem-oriented tasks such as consequence finding,
diagnosis, action/update, decision making etc.
Thus, Lit-simplifying (or Var(simplifying) a KB during a preliminary
off-line phase can  prove helpful for improving on-line inference since 
simplification never increases the size of a KB. 
As shown by Proposition \ref{forget-not-polsize}, a similar conclusion cannot be drawn
to what concerns forgetting. 
This seems to be the price to be paid to benefit from the power of forgetting.
However, this negative conclusion must be tempered by the two following
comments. On the one hand, forgetting is interesting {\it per se}; it is
not only a tool that can help improving inference in some cases but also a goal in
several AI applications. On the other hand, our complexity
results relate to the worst case situation, only, and, as evoked before,
forgetting is feasible in many practical cases.
Finally, let us note that there are several complete propositional
fragments for which forgetting is easy. Especially, as advocated 
by \citeA{Darwiche99}, compiling a KB into a DNNF formula during
an off-line step can prove practically valuable to achieve forgetting
in an efficient way, provided that the size of the compiled form remains
small enough (which cannot be guaranteed in the worst case). Since it 
is not known whether the DNNF fragment is strictly
more succinct than the prime implicates one \cite{DarwicheMarquis01},
the prime implicates fragment can also be targeted with
profit as a compilation language for some knowledge bases;
especially, some recent approaches to the implicit representation
of prime implicates \cite{SimondelVal01} exhibit very significant empirical performances
(they enable the computation of sets of prime implicates containing
up to $10^{70}$ clauses). Accordingly, they can prove valuable
for the practical computing of independence and forgetting.
\end{itemize}

\section*{Acknowledgements}

The third author has been partly supported by
the IUT de Lens, the Universit\'e d'Artois, the R\'egion Nord / Pas-de-Calais
under the TACT-TIC project, and by the European Community
FEDER Program. Some results of this paper 
already appeared in Section 3 of the paper \cite{LangMarquis98a} 
``Complexity results for independence and definability in propositional logic'',
{\it Proc. of the $6^{th}$ International Conference on Principles of Knowledge Representation
and Reasoning (KR'98)}, pages 356-367, 1998.

\newpage

\section*{Appendix A: Proofs}

% --------------------------------------------------------------------------
% PROOFS FL- and FV-INDEPENDENCE 
% --------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{sema-inde-lite}~~ \em
A formula $\Sigma$ is Lit-independent from $l$ if and only if, for any
interpretation $\omega \in \Omega_{PS}$, if $\omega \models \Sigma$ then
$Force(\omega,\neg l) \models \Sigma$.\\ \rm 

\noindent{\bf Proof:} Assume that $\Sigma$ is Lit-independent from $l$.
Then, there exists a formula $\Phi$ in NNF that is equivalent to $\Sigma$, 
and
does not contain $l$.  Then, for any $\omega \in \Omega_{PS}$ such that $\omega \models 
\Phi$ we
have $Force(\omega,\neg l) \models \Phi$. Since $\Phi$ is equivalent to
$\Sigma$,
we conclude that the same property holds for $\Sigma$.

Assume that, for any interpretation $\omega \in \Omega_{PS}$, 
$\omega \models \Sigma$ implies
$Force(\omega,\neg l) \models \Sigma$. We prove that $\Sigma$ is 
Lit-independent
from $l$. Indeed, let $\gamma_{\omega}$ be the term whose only model is
$\omega$.
The following equivalence holds:\eatpar

\begin{eqnarray*}
\Sigma
&\equiv&
\bigvee \{ \gamma_{\omega}  ~|~  \omega \models \Sigma \} \\
&\equiv&
\bigvee \{ \gamma_{\omega}  ~|~ \omega \models \Sigma \mbox{ and } \omega
\not\models l \}
     \cup \{ \gamma_{\omega}  ~|~ \omega \models \Sigma \mbox{ and } \omega
\models l \} \\
&\equiv&
\bigvee \{ \gamma_{\omega}  ~|~ \omega \models \Sigma \mbox{ and } \omega
\not\models l \}
     \cup \{ \gamma_{\omega}  \vee \gamma_{Force(\omega,\neg l)} ~|~  \omega
\models \Sigma \mbox{ and } \omega \models l \}
\end{eqnarray*}

The latter step can be done because $\omega \models \Sigma$ implies that
$Force(\omega,\neg l)$ is also a model of $\Sigma$. Now, if $\omega 
\not\models
l$ then
$\gamma_{\omega}$ does not contain $l$. On the other hand, if $\omega 
\models
l$, then
$\gamma_{\omega}  \vee \gamma_{Force(\omega,\neg l)}$ can be rewritten as a
conjunction of
literals not containing neither $l$ nor its negation. As a result, the above
formula (which is in NNF) does not contain $l$, which means that $\Sigma$
is Lit-independent from $l$.~\qed

% -------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{PropFLI}~\\ \em
(1) $DepLit(\Sigma) \subseteq Lit(\Sigma)$;\\
(2) If $\Sigma \equiv \Phi$, then $DepLit(\Sigma) = DepLit(\Phi)$;\\
(3a) $ DepLit(\Sigma\wedge \Phi) \subseteq DepLit(\Sigma) \cup 
DepLit(\Phi)$;\\
(3b) $ DepLit(\Sigma\vee \Phi) \subseteq DepLit(\Sigma) \cup 
DepLit(\Phi)$;\\
(4) $l \in DepLit(\Sigma)$ if and only if $\neg l \in DepLit(\neg \Sigma)$.
\\ \rm

\noindent{\bf Proof:}
\begin{enumerate}
\item Trivial.
\item $L \leadsto \Sigma$ if and only if there exists a formula $\Psi$ that 
is equivalent to $\Sigma$, and such that $\Psi$ is syntactically Lit-independent
from $L$. Since $\Sigma \equiv \Phi$, it follows that $\Phi \equiv \Psi$.
\item Let $\Psi$ (resp. $\Pi$) be a NNF formula equivalent to $\Sigma$ 
(resp.
$\Phi$) s.t. no literal of $L$ occurs in it. Then $\Psi \wedge \Pi$ (resp.
$\Psi \vee \Pi$) is a formula equivalent to $\Sigma \wedge \Phi$ (resp. 
$\Sigma
\vee \Phi$), which is in NNF, and no literal of $L$ occurs in it.
\item Straightforward from the fact that $l$ appears in a NNF formula
$\Sigma$ if and only if $\neg l$ appears in the NNF form of $\neg \Sigma$.
\end{enumerate}
\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{PropFVI}\\ \em
(1) $DepVar(\Sigma) \subseteq Var(\Sigma)$;\\
(2) If $\Sigma \equiv \Phi$, then $DepVar(\Sigma) = DepVar(\Phi)$;\\
(3a) $DepVar(\Sigma\wedge \Phi) \subseteq DepLit(\Sigma) \cup 
DepLit(\Phi)$;\\
(3b) $DepVar(\Sigma\vee \Phi) \subseteq DepLit(\Sigma) \cup 
DepLit(\Phi)$;\\
(4) $DepVar(\neg \Sigma) = DepVar(\Sigma)$.\\ \rm

\noindent {\bf Proof:} (1) is trivial; (2) and (3) are similar to the proof 
of points (2) and (3) of Proposition~\ref{PropFLI}, replacing ``literal'' 
by ``variable'', $l$ by $v$, and  $DepLit$ by $DepVar$.
As to (4): if $x \not \in DepVar(\Sigma)$ then there exists a formula $\Phi$ 
equivalent to $\Sigma$ in which $x$ does not appear; since $x$ does not 
appear in $\neg \Phi$  either, $\neg \Phi$ is a formula equivalent to 
$\neg \Sigma$ in which $x$ does not appear.
\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{simplified} \em
Let $\Sigma$ be a formula from $PROP_{PS}$.
\begin{itemize}
\item $\Sigma$ is Lit-simplified if and only if the following equivalence 
holds:
for every
$L \subseteq L_{PS}$,
$\Sigma$ is syntactically Lit-independent from $L$ if and only if $L \not 
\leadsto
\Sigma$ holds.
\item $\Sigma$ is Var-simplified if and only if the following equivalence 
holds:
for every
$V \subseteq PS$,
$\Sigma$ is syntactically Var-independent from $V$ if and only if $V \not
\leadsto_{-}^{+} \Sigma$ holds.
\end{itemize} \rm

\noindent {\bf Proof:}
\begin{itemize}
\item Lit-simplification
\begin{itemize}
\item $\Rightarrow$: Assume $\Sigma$ is Lit-simplified (thus
$Lit(\Sigma) = DepLit(\Sigma)$) and let $L \subseteq L_{PS}$.
If $\Sigma$ is syntactically Lit-independent from $L$, then
$L \cap Lit(\Sigma) = \emptyset$, thus $L \cap DepLit(\Sigma)
= \emptyset$, i.e., $L \not \leadsto \Sigma$.
\item $\Leftarrow$: Assume that $\Sigma$ is not Lit-simplified. Then there 
exists
$l \in Lit(\Sigma)$ s.t.\  $\Sigma$ is Lit-independent from $l$. With $L =
\{l\}$, it is clear that $\Sigma$ is syntactically Lit-dependent on $L$, while
Lit-independent from it,
contradiction.
\end{itemize}
\item Var-simplification. The proof is similar to the Lit-simplification case,
replacing
``Lit-independent'' by ``Var-independent'', $L$ by $V$, $L_{PS}$ by $PS$, $l$ by
$x$, $Lit(\Sigma)$
by $Var(\Sigma)$.
\end{itemize}
\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{ex-simp}~~ \em
For every $\Sigma$ from $PROP_{PS}$, there exists a Lit-simplified formula 
$\Phi$
s.t.\  $\Sigma \equiv \Phi$.\\ \rm

\noindent{\bf Proof:} Since $\Sigma$ is Lit-independent from $L \setminus 
DepLit(\Sigma)$
we know that there exists a NNF formula $\Phi$ equivalent to $\Sigma$ such 
that $Lit(\Phi) \cap (L \setminus DepLit(\Sigma)) = \emptyset$, i.e., such 
that  $Lit(\Phi) \subseteq DepLit(\Sigma)$. By point (2) of Proposition 
\ref{PropFLI} we have $DepLit(\Phi) =
DepLit(\Sigma)$. Thus, $DepLit(\Phi) \subseteq Lit(\Phi) ) \subseteq 
DepLit(\Sigma) =
DepLit(\Phi)$, from which we conclude that $DepLit(\Phi) = Lit(\Phi)$, i.e., 
$\Phi$ is Lit-simplified.
\qed

% ------------------------------------------------------------------------


\noindent{\bf Proposition}~\ref{deductionl}~~ \em
Let $\Sigma$ be a formula from $PROP_{PS}$ and $l$ be a literal of $L_{PS}$.
The next four statements are equivalent:\\
(1) $l \not \leadsto \Sigma$;\\
(2) $\Sigma_{l \leftarrow 1} \models \Sigma_{l \leftarrow 0}$;\\
(3) $\Sigma \models \Sigma_{l \leftarrow 0}$;\\
(4) $\Sigma_{l \leftarrow 1} \models \Sigma$.\\ \rm

\noindent{\bf Proof:}
\begin{description}
\item[$(1) \Rightarrow (2)$:] Let $v$ the variable of $l$ and
assume that
$\Sigma_{l \leftarrow 1} \not \models \Sigma_{l \leftarrow 0}$,
which means that there is a $PS\setminus\{v\}$-world
$\omega$ such that $\omega \models \Sigma_{l \leftarrow 1} \wedge \neg
\Sigma_{l \leftarrow 0}$; since $\Sigma$ is equivalent to
$(l\wedge\Sigma_{l \leftarrow 1})
	\vee (\neg l\wedge\Sigma_{l \leftarrow }0)$, we have
$\omega \wedge \{l\} \models \Sigma_{l \leftarrow 1} \wedge l \models
\Sigma$ and $Force(\omega \wedge \{l\}, \neg l) = \omega \wedge \{\neg l\}
\models \Sigma_{l \leftarrow 1}\wedge \neg \Sigma_{l \leftarrow 0}$;
hence, $Force(\omega\wedge\{l\},\neg l) \not \models \Sigma$ and
therefore $l \leadsto \Sigma$ by Proposition 1.

\item[$(2) \Rightarrow (3)$:] Assume
$\Sigma_{l \leftarrow 1} \models \Sigma_{l \leftarrow 0}$.
We have the following chain of implications:\eatpar

\begin{eqnarray*}
\Sigma
&\equiv&
(l \wedge \Sigma_{l \leftarrow 1} ) \vee ( \neg l \wedge \Sigma_{l 
\leftarrow 0}
) \\
\Sigma
& \models &
(l \wedge \Sigma_{l \leftarrow 0} ) \vee ( \neg l \wedge \Sigma_{l 
\leftarrow 0}
) \\
\Sigma
& \models & \Sigma_{l \leftarrow 0}
\end{eqnarray*}

\item[$(3) \Rightarrow (1)$:] Let us assume that $\Sigma \models \Sigma_{l
\leftarrow 0}$, and prove that $l \not\leadsto \Sigma$. Indeed, the 
assumption
can be rewritten as:\eatpar

\[
\forall \omega \in \Omega_{PS} ~.~ (\omega \models \Sigma ~~ \Rightarrow \omega \models 
\Sigma_{l
\leftarrow 0})
\]

Now, $\omega \models \Sigma_{l \leftarrow 0}$ is equivalent to say that 
changing
the
truth value of $l$ to false, $\omega$ is still a model of $\Sigma$. In
formulas,\eatpar

\[
\forall \omega \in \Omega_{PS} ~.~ (\omega \models \Sigma ~~ \Rightarrow Force(\omega,\neg l)
\models \Sigma)
\]

This is exactly the definition of $l \not\leadsto \Sigma$.

\item[$(2) \Rightarrow (4)$:] Same as the proof of $(2) \Rightarrow (3)$.

\item[$(4) \Rightarrow (1)$:] Similar to the proof of $(3) \Rightarrow (1)$.

\end{description}\qed

\iffalse

\begin{itemize}

\item $(1) \Leftrightarrow (2)$:

\begin{itemize}

\item $\Rightarrow$: Let $\Phi$ be a NNF formula equivalent to $\Sigma$ s.t.
$l \not \in Lit(\Phi)$. Clearly enough, $\Phi$ can be turned into CNF while
preserving this property, i.e. $l \not \in Lit(\Phi)$. Let $\Psi$ such a CNF 
of
$\Phi$: no clause $\gamma$ of $\Psi$ contains $l$ (but some of them may 
contain
$\neg l$). Clearly enough, $\Sigma_{l \leftarrow 1} \equiv \Psi_{l 
\leftarrow
1}$ and $\Sigma_{l \leftarrow 0} \equiv \Psi_{l \leftarrow 0}$. For every
clause $\gamma$ of $\Psi$, there are two possibilities: (1) $\gamma$ 
contains
$\neg l$ or (2) $\gamma$ does not contain $\neg l$.  In the case (1),
$\gamma_{l \leftarrow 0}$ is valid. Hence, all such clauses are consequences 
of
$\Psi_{l \leftarrow 1}$. In the remaining case (2), $\gamma_{l \leftarrow 0}
\equiv \gamma_{l \leftarrow 1}$, hence $\Psi_{l \leftarrow 1} \models 
\gamma_{l
\leftarrow 0}$.  Thus, in both cases, we have $\Psi_{l \leftarrow 1} \models
\Psi_{l \leftarrow 0}$.  Equivalently, we have $\Sigma_{l \leftarrow 1} 
\models
\Sigma_{l \leftarrow 0}$.

\item $\Leftarrow$: $\Sigma$ is equivalent to the formula $(l \wedge 
\Sigma_{l
\leftarrow 1}) \vee (\neg l \wedge \Sigma_{l \leftarrow 0})$, which is also
equivalent to $(\Sigma_{l \leftarrow 1} \vee \neg l) \wedge (\Sigma_{l
\leftarrow 0} \vee l) \wedge (\Sigma_{l \leftarrow 1} \vee \Sigma_{l 
\leftarrow
0})$ (distributing $\vee$ over $\wedge$).  Whenever $\Sigma_{l \leftarrow 1}
\models \Sigma_{l \leftarrow 0}$ holds, this expression can be simplified to
$(\Sigma_{l \leftarrow 1} \vee \neg l) \wedge \Sigma_{l \leftarrow 0}$.  
Since
neither $l$ nor $\neg l$ appears in $\Sigma_{l \leftarrow 1}$ and in 
$\Sigma_{l
\leftarrow 0}$, the NNF of this simplified formula contains no occurrence of
$l$. Since it is equivalent to $\Sigma$, $\Sigma$ is Lit-independent from $l$.

\end{itemize}

\item $(2) \Leftrightarrow (3)$:

\begin{itemize}

\item $\Rightarrow$: If $\Sigma_{l \leftarrow 1} \models \Sigma_{l 
\leftarrow
0}$ holds, then $(l \wedge \Sigma_{l \leftarrow 1}) \models \Sigma_{l
\leftarrow 0}$ holds as well.  Since $\Sigma_{l \leftarrow 0} \models 
\Sigma_{l
\leftarrow 0}$ trivially holds, it is also the case that $(\neg l \wedge
\Sigma_{l \leftarrow 0}) \models \Sigma_{l \leftarrow 0}$ holds.  Hence 
$(\neg
l \wedge \Sigma_{l \leftarrow 0}) \vee (l \wedge \Sigma_{l \leftarrow 1})
\models \Sigma_{l \leftarrow 0}$ holds. The fact that $\Sigma$ is equivalent 
to
$(\neg l \wedge \Sigma_{l \leftarrow 0}) \vee (l \wedge \Sigma_{l \leftarrow
1})$ completes the proof.

\item $\Leftarrow$: $\Sigma$ is equivalent to $(\neg l \wedge \Sigma_{l
\leftarrow 0}) \vee (l \wedge \Sigma_{l \leftarrow 1})$.  Hence, if $\Sigma
\models \Sigma_{l \leftarrow 0}$ holds, it must be the case that both $(\neg 
l
\wedge \Sigma_{l \leftarrow 0}) \models \Sigma_{l \leftarrow 0}$ and $(l 
\wedge
\Sigma_{l \leftarrow 1}) \models \Sigma_{l \leftarrow 0}$ hold.  Since 
neither
$l$ nor $\neg l$ occurs in $\Sigma_{l \leftarrow 1}$ and $\Sigma_{l 
\leftarrow
0}$, $(l \wedge \Sigma_{l \leftarrow 1}) \models \Sigma_{l \leftarrow 0}$ 
holds
only if $\Sigma_{l \leftarrow 1} \models \Sigma_{l \leftarrow 0}$ holds.

\end{itemize}

\item $(2) \Leftrightarrow (4)$:

\begin{itemize}

\item $\Rightarrow$: $\Sigma$ is equivalent to $(\neg l \wedge \Sigma_{l
\leftarrow 0}) \vee (l \wedge \Sigma_{l \leftarrow 1})$, which is also
equivalent to $(\neg l \wedge \Sigma_{l \leftarrow 0}) \vee (l \wedge 
\Sigma_{l
\leftarrow 1}) \vee (\Sigma_{l \leftarrow 0} \wedge \Sigma_{l \leftarrow 
1})$.
If $\Sigma_{l \leftarrow 1} \models \Sigma_{l \leftarrow 0}$ holds, then
$\Sigma_{l \leftarrow 1} \models (\Sigma_{l \leftarrow 0} \wedge \Sigma_{l
\leftarrow 1})$ holds as well. Hence, $\Sigma_{l \leftarrow 1} \models 
\Sigma$
holds.

\item $\Leftarrow$: $\Sigma$ is equivalent to $(\neg l \wedge \Sigma_{l
\leftarrow 0}) \vee (l \wedge \Sigma_{l \leftarrow 1})$, which is also
equivalent to $(\Sigma_{l \leftarrow 1} \vee \neg l) \wedge (\Sigma_{l
\leftarrow 0} \vee l) \wedge (\Sigma_{l \leftarrow 1} \vee \Sigma_{l 
\leftarrow
0})$ (distributing $\vee$ over $\wedge$). Thus, if $\Sigma_{l \leftarrow 1}
\models \Sigma$ holds, it must also be the case that $\Sigma_{l \leftarrow 
1}
\models (\Sigma_{l \leftarrow 0} \vee l)$.  Since neither $l$ nor $\neg l$
occurs in $\Sigma_{l \leftarrow 1}$ and $\Sigma_{l \leftarrow 0}$, this 
implies
that $\Sigma_{l \leftarrow 1} \models \Sigma_{l \leftarrow 0}$ holds.

\end{itemize}

\end{itemize}\qed

\fi

% ------------------------------------------------------------------------


\noindent{\bf Proposition}~\ref{deductionfv}~~ \em
Let $\Sigma$ be a formula from $PROP_{PS}$ and $x$ be a variable of $PS$.
The next four statements are equivalent:\\
(1) $x \not \leadsto_{-}^{+} \Sigma$;\\
(2) $\Sigma_{x \leftarrow 0} \equiv \Sigma_{x \leftarrow 1}$;\\
(3) $\Sigma \equiv \Sigma_{x \leftarrow 0}$;\\
(4) $\Sigma \equiv \Sigma_{x \leftarrow 1}$.\\ \rm

\noindent {\bf Proof}: Easy consequence of the definition of FV-independence
($\Sigma$ is Var-independent from $x$ if and only if it is Lit-independent from
$\{x, \neg x\}$), and Proposition~\ref{deductionl}).\qed


% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{primel}~~ \em
Let $\Sigma$ be a formula from $PROP_{PS}$ and $L$ be a subset of
$L_{PS}$.
The next statements are equivalent:\\
(1) $L \not \leadsto \Sigma$;\\
(2) $PI(\Sigma) \subseteq \{\gamma \ | \ \gamma$ is a term that does not 
contain
any literal from
$L\}$;\\
(3) $IP(\Sigma) \subseteq \{\delta \ | \ \delta$ is a clause that does not
contain any literal from
$L\}$.\\ \rm

\noindent {\bf Proof:}

\begin{itemize}

\item $(1) \Leftrightarrow (2)$:

\begin{itemize}

\item $\Rightarrow$: If $\Sigma$ is Lit-independent from $L$, then there 
exists a NNF formula $\Phi$ equivalent to $\Sigma$ s.t. $Lit(\Phi) \cap L = 
\emptyset$. Clearly enough, the property $Lit(\Phi) \cap L = \emptyset$ is still 
satisfied if $\Phi$ is turned into DNF, especially when $\Phi$ is turned into its 
prime implicant normal form. Since two equivalent formulas have the same prime
implicants, no term of $PI(\Sigma)$ contains a literal from $L$.

\item $\Leftarrow$: $PI(\Sigma)$ is a NNF formula that is equivalent to 
$\Sigma$ and syntactically Lit-independent from $L$. Hence, $\Sigma$ is Lit-independent from 
$L$.

\end{itemize}

\item $(1) \Leftrightarrow (3)$: Similar to the prime implicant situation, 
using CNF instead of DNF.

\end{itemize}\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{primev}~~ \em
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ be a subset of 
$PS$.
The next statements are equivalent:\\
(1) $V \not \leadsto_{-}^{+} \Sigma$;\\
(2) $PI(\Sigma) \subseteq \{\gamma \ | \ \gamma$ is a term that does not 
contain
any variable from
$V\}$;\\
(3) $IP(\Sigma) \subseteq \{\delta \ | \ \delta$ is a clause that does not
contain any variable from
$V\}$.\\ \rm


\noindent {\bf Proof:}
Easy consequence of the definition of FV-independence, plus 
Proposition~\ref{primev} above.
\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{cflfv}~~ \em 
{\sc FL dependence}, {\sc FV dependence}, {\sc full FL dependence} 
and {\sc full FV dependence}  are {\sf NP}-complete.\\ \rm

\noindent {\bf Proof:}

\begin{itemize}

\item {\bf FL dependence}

\begin{itemize}

\item Membership. In order to show that $\Sigma$ is Lit-dependent on $L$,
it is sufficient to guess a literal $l$ from $L$ and a 
$(Var(\Sigma) \setminus \{Var(l)\})$-world
$\omega$ that is a model of $\Sigma_{l \leftarrow 1}$ but not a model of
$\Sigma_{l \leftarrow 0}$.
These tests can be achieved in time polynomial in $|\Sigma|$.

\item Hardness. Let us consider the mapping $M$ s.t. $M(\Sigma) = \langle
\Sigma \wedge new, new\rangle$, where $new$ is a propositional variable that
does not occur in $\Sigma$. Clearly enough, $M(\Sigma)$ can be computed in time
polynomial in $|\Sigma|$. Moreover, $\Sigma$ is satisfiable if and only if $\Sigma \wedge
new$ is Lit-dependent on $\{new\}$.

\end{itemize}

\item {\bf FV dependence}

\begin{itemize}

\item Membership. In order to show that $\Sigma$ is Var-dependent on $V$, it is
sufficient to guess a variable $x$ from $V$ and a $(Var(\Sigma) \setminus
\{x\})$-world $\omega$ that is not a model of the formula  $\Sigma_{x
\leftarrow 0} \Leftrightarrow \Sigma_{x \rightarrow 1}$. This test can be
achieved in time polynomial in $|\Sigma|$.

\item Hardness. Similar to the hardness proof of FL-dependence, replacing
``Lit-dependent'' by ``Var-dependent''.

\end{itemize}

\item {\bf full FL dependence}

\begin{itemize}

\item Membership. $\Sigma$ is fully Lit-dependent on $L = \{l_1, ..., l_n\}$ if and only if
$\Sigma_{l_1 \leftarrow 1} \not \models \Sigma_{l_1 \leftarrow 0}$ and ... and
$\Sigma_{l_n \leftarrow 1} \not \models \Sigma_{l_n \leftarrow 0}$ holds.
Equivalently, $\Sigma$ is fully Lit-dependent on $L = \{l_1, ..., l_n\}$ if and only if the
formula $rename_1(\Sigma_{l_1 \leftarrow 1} \wedge \neg \Sigma_{l_1 \leftarrow
0}) \wedge ... \wedge rename_n(\Sigma_{l_n \leftarrow 1} \wedge \neg
\Sigma_{l_n \leftarrow 0})$ is satisfiable, where each $rename_i$ is a renaming
that maps variables to new symbols (in a uniform way).  Since this formula can
be computed in time polynomial in $|\Sigma|+|V|$, the membership of {\sc full
FL dependence} to {\sf NP} follows.

\iffalse

\item Hardness. Let us consider the mapping $\omega$ from $PROP_{PS}$ to $PROP_{PS}
\times 2^{PS}$ s.t. $M(\Sigma) = \langle \Sigma \wedge new, \{new\}\rangle$,
where $new \in PS \setminus Var(\Sigma)$. $M(\Sigma)$ can be easily computed in
time polynomial in $|\Sigma|$. Moreover, we have $\Sigma \in SAT$ if and only if
$M(\Sigma) \in$ {\sc full FL dependence}.  Indeed, if $\Sigma$ is satisfiable,
$(\Sigma \wedge new)_{new \leftarrow 0}$ is unsatisfiable, while $\Sigma \wedge
new$ is satisfiable, hence $(\Sigma \wedge new)_{new \leftarrow 0} \not \equiv
(\Sigma \wedge new)$ holds. In the remaining case ($\Sigma$ is unsatisfiable),
then $(\Sigma \wedge new)_{new \leftarrow 0} \equiv (\Sigma \wedge new)$ holds,
hence $\Sigma$ is not fully Lit-dependent on $\{new\}$.

\fi

\item Hardness. Full FL-dependence and FL-dependence coincide in the case in
which $L$ is composed of a single literal.  Since the {\sf NP}-hardness of FL-dependence 
has been proved using a set $L$ composed of a single literal, the
{\sf NP}-hardness of full FL dependence follows.

\end{itemize}

\item {\bf full FV dependence}

\begin{itemize}

\item Membership. $\Sigma$ is fully Var-dependent on $V = \{x_1, ..., x_n\}$ if and only if
$\Sigma \not \equiv \Sigma_{x_1 \leftarrow 0}$ and ... and $\Sigma \not \equiv
\Sigma_{x_n \leftarrow 0}$ holds.  Equivalently, $\Sigma$ is fully Var-dependent
on $V = \{x_1, ..., x_n\}$ if and only if the formula $rename_1(\Sigma \oplus \Sigma_{x_1
\leftarrow 0}) \wedge ... \wedge rename_n(\Sigma \oplus \Sigma_{x_n \leftarrow
0})$ is satisfiable, where each $rename_i$ is a renaming that maps variables to
new symbols (in a uniform way).  Since this formula can be computed in time
polynomial in $|\Sigma|+|V|$, the membership of {\sc full FV dependence} to
{\sf NP} follows.

\item Hardness. Full FV-dependence and FV-dependence coincide if $L$ is
composed of a single literal. Since the {\sf NP}-hardness of FV-dependence has
been proved using a set $L$ composed of a single literal, the {\sf NP}-hardness
of full FV-dependence follows.

\iffalse
Similar to the hardness proof of FL dependence, replacing
``Lit-dependent'' by ``Var-dependent''.
\fi

\end{itemize}

\end{itemize}\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{poly}~~ \em 
Whenever $\Sigma$ belongs to a  class ${\mathcal C}$ of CNF formulas that is 
tractable for clausal query answering (i.e., there exists a polytime algorithm
to determine whether $\Sigma \models \gamma$ for any CNF formula $\gamma$) 
and stable for variable 
instantiation (i.e., replacing in $\Sigma \in {\mathcal C}$ any variable by
{\em true} or by {\em false}
gives a formula that still belongs to ${\mathcal C}$) then 
{\sc FL dependence}, {\sc FV dependence}, {\sc full FL dependence} and 
{\sc full FV dependence} are in {\sf P}.
\\ \rm

\noindent {\bf Proof:}
This is a straightforward consequence of Propositions \ref{deductionl}
and \ref{deductionfv}. 
When $\Sigma$ belongs to a  class ${\mathcal C}$ of formulas that is 
tractable for clausal query answering and stable for variable 
instantiation, we can easily check whether $\Sigma \models \Sigma_{x \leftarrow 0}$
and $\Sigma_{x \leftarrow 0} \models \Sigma$ holds.
\qed

% ------------------------------------------------------------------------


\noindent{\bf Proposition}~\ref{comp-simplif}~~ \em 
{\sc Lit-simplified formula} and {\sc Var-simplified formula} are 
{\sf NP}-complete.\\ \rm

\noindent {\bf Proof:}
\begin{itemize}

\item {\bf Lit-simplification}

\begin{itemize}

\item Membership. Easy consequence of the fact that {\sc Lit-simplified
formula} is a restriction of {\sc full FL dependence} that is in {\sf NP} (and
{\sf NP} is closed under polynomial reductions).

\item Hardness. We prove that a formula $\Phi$, built over an alphabet
$X=\{x_1,\ldots,x_n\}$, is satisfiable if and only if formula $\Sigma$ is
L-simplified, where\eatpar

\[
\Sigma = (\Phi \vee \Phi[X/\neg X]) \wedge \bigwedge_{x_i \in X} x_i \Leftrightarrow y_i
\]

\noindent where $\Phi[X/\neg X]$ is the formula obtained by replacing 
in $\Phi$ each occurrence of $x_i$ (resp. $\neg x_i$) with $\neg x_i$ 
(resp. $x_i$).

First, if $\Phi$ is not satisfiable, neither $\Phi[X/\neg X]$ is, thus $(\Phi \vee
\Phi[X/\neg X])$ is not satisfiable. As a result, $\Sigma$ is not satisfiable, thus
it is not Lit-simplified, because $DepLit(\Sigma)=\emptyset$ but $\Sigma$ mentions
variables $x_i$ and $y_i$.

Assume $\Phi$ satisfiable. Clearly, $\Sigma$ is satisfiable as well: let $\omega$ be a model
of $\Sigma$. We prove that $\Sigma$ is  Lit-simplified by showing that it is Lit-dependent on each
literal it contains. We have $Lit(\Sigma) = \{x_1,\ldots, x_n, y_1,\ldots, y_n,
\neg x_1, \ldots, \neg x_n, \neg y_1, \ldots, \neg y_n\}$. Let $l_i \in
Lit(\Sigma)$.

\begin{enumerate}

\item[(1)] Assume that $\omega \models l_i$. Then, $Force(\omega, \neg l_i) \not \models \Sigma$.
Indeed, let $Var(l_i) = x_i$ (resp.\  $y_i$): $\omega$ satisfies $x_i \Leftrightarrow y_i$ so
changing the truth value of $x_i$ only (resp.\  $y_i$ only) leads to a model
that does not satisfy $x_i \Leftrightarrow y_i$.

\item[(2)] Otherwise, we have $\omega \models \neg l_i$. Replacing $l_i$ by $\neg l_i$ in
the proof of case~(1) enables deriving the expected conclusion.

\end{enumerate}

\item {\bf Var-simplification}
\begin{itemize}
\item Membership. Easy consequence of the fact that {\sc Var-simplified formula} is a
restriction of {\sc full FV dependence} that is in {\sf NP} (and {\sf NP} is closed
under polynomial reduction).
\item Hardness. The proof is similar to the proof of {\sf NP}-hardness of {\sc Lit-simplified
formula}, replacing ``Lit-simplified'' with ``Var-simplified''.
\end{itemize}
\end{itemize}
\end{itemize}
\qed

% ----------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{computeDepLitVar}~~ \em
\begin{enumerate}
\item Determining whether $DepLit(\Sigma) = L$ (where $L$ is a set of 
literals), and determining  whether $DepVar(\Sigma) = X$ (where $X$ 
is a set of variables) is \bh2-complete.
\item The search problem consisting in {\em computing} $DepLit(\Sigma)$ 
(respectively $DepVar(\Sigma)$) is in ${\sf F}\Delta_2^p$ and is 
both {\sf NP} and \conp-hard.
\end{enumerate}
\rm

\noindent {\bf Proof}: 

\begin{itemize}

\item  Determining whether $DepLit(\Sigma) = L$ is \bh2-complete.

\begin{itemize}

\item Membership. 

$DepLit(\Sigma) = L$ \iff (i) $l \leadsto \Sigma$ holds for every $l \in L$ and
(ii) $l \not \leadsto \Sigma$ holds for every $l\in Lit(\Sigma)\setminus L$; 
the set of instances $\langle \Sigma, L \rangle$ such that (i) holds is the 
union of a linear number of problems in \np, thus it is in \np; similarly,
the set of instances $\langle \Sigma, L \rangle$ such that (ii) holds
is a problem in \conp. This proves the membership to \bh2 of the problem of
determining whether $DepLit(\Sigma) = L$.

\item Hardness.

Let $\langle\Phi, \Gamma\rangle$ be a pair of propositional formulas.
Without loss of generality, we assume that $\Phi$ and $\Gamma$ do not share any 
variable and that $X = Var(\Phi) = \{x_1, ..., x_n\}$, $Var(\Gamma) = \{z_1, ..., z_p\}$.
Furthermore we assume that $X \neq \emptyset$ (if it were not the case
it would then be sufficient then to replace $\Phi$ by $\Phi \wedge (t\vee \neg t)$
before performing the reduction). 
We prove that $\langle\Phi, \Gamma\rangle$ is a positive instance
of {\sc sat-unsat}, i.e., $\Phi$ is satisfiable and $\Gamma$ is unsatisfiable,
if and only if $DepLit(\Phi \wedge \neg \Gamma) = Lit(\Sigma(\Phi))$ where 
$\Sigma(\Phi)=(\Phi \vee \Phi[X/\neg X]) \wedge \bigwedge_{x_i \in X} x_i \Leftrightarrow y_i$
as in a previous proof (note that $\Sigma(\Phi)$ and $\Gamma$ do not share any 
variables).\\
(i)  if $\Phi$ is satisfiable and $\Gamma$ is unsatisfiable, 
then $\Sigma(\Phi)$ is Lit-simplified according to the previous proof
and thus $DepLit(\Sigma(\Phi)) = Lit(\Sigma(\Phi))$ whereas $DepLit(\neg \Gamma) = \emptyset$,
which together entail that $DepLit(\Sigma(\Phi)\wedge\neg \Gamma) = Lit(\Sigma(\Phi))$.\\
(ii) Assume that $\Phi$ is unsatisfiable and $DepLit(\Sigma(\Phi)\wedge\neg \Gamma) 
= Lit(\Sigma(\Phi))$.
Then $\Sigma(\Phi)$ is not simplified (recall that $Var(\Phi)$ is not empty and hence
so is $Lit(\Sigma(\Phi))$), thus  $DepLit(\Sigma(\Phi)) \subset Lit(\Sigma(\Phi))$. Now, 
$DepLit(\Sigma(\Phi)\wedge\neg \Gamma) = Lit(\Sigma(\Phi))$ implies 
$DepLit(\Sigma(\Phi)\wedge\neg \Gamma) \cap Lit(\Gamma) = \emptyset$, which is possible only
if $\Gamma$ is a tautology (because $\Sigma(\Phi)$ and $\Gamma$ do not share any variables);
but in this case, $\Sigma(\Phi)\wedge\neg \Gamma$ is inconsistent and thus
$DepLit(\Sigma(\Phi)\wedge\neg \Gamma) = \emptyset$, hence,  $Lit(\Sigma(\Phi)) = \emptyset$,
which is contradictory.\\
(iii) Assume that $\Gamma$ is satisfiable and  $DepLit(\Sigma(\Phi)\wedge\neg \Gamma) 
= Lit(\Sigma(\Phi))$.\\
The second condition can hold only if $\Sigma(\Phi)$ is unsatisfiable, hence 
not Lit-simplified (since $Lit(\Sigma(\Phi)) \neq \emptyset$), so $\Phi$ is unsatisfiable 
as well; this takes us back to the case (ii), which leads us to the
same contradiction again. 
\end{itemize}

\item Computing $DepLit(\Sigma)$ is in ${\sf F}\Delta_2^p$
since {\sc FL dependence} is in {\sf NP} and $DepLit(\Sigma) \subseteq Lit(\Sigma)$
(hence, it is sufficient to test for every $l \in Lit(\Sigma)$ whether or not
$\Sigma$ is Lit-independent from it).
It is also both \np-hard and \conp-hard.
\np-hardness is showed by the following polynomial reduction from
{\sc sat}: A CNF formula $F$ is satisfiable if and only if $F$ is valid or 
$DepLit(F) \neq \emptyset$; clearly enough, valid CNF formulas can be
recognized in polynomial time. Thus, {\sc sat} can be solved if we know how to compute  $DepLit(\Sigma)$
for any $\Sigma$, which shows that computing  $DepLit(\Sigma)$ is \np-hard.
The proof of \conp-hardness is similar ($F$ is unsatisfiable if and only
if $F$ is not valid and $DepLit(F) = \emptyset$). 

\item  Determining whether $DepVar(\Sigma) = V$ is \bh2-complete.
Membership follows easily from the membership of the corresponding problem
for $DepLit(\Sigma)$. Hardness is similar to the hardness proof
for $DepLit(\Sigma) = L$.

\item  Computing $DepVar(\Sigma)$ is in ${\sf F}\Delta_2^p$ and
is both \np-hard and \conp-hard.
Similar to the corresponding result for $DepLit(\Sigma)$.

\end{itemize}
\qed


\iffalse

\item Hardness. Let $G = \langle V, E\rangle$ be a graph. Let $\omega$ the mapping s.t.
$M(G)$ is the set of clauses containing:
\begin{itemize}
\item For every vertex $v_i$ of $V$, the four clauses $\neg v_i1 \vee \neg v_i2$,
$\neg v_i1 \vee \neg v_i3$, $\neg v_i2 \vee \neg v_i2$, $v_i1 \vee v_i2 \vee v_i3$.
\item For every edge $\{v_i, v_j\}$ of $E$, the 3 clauses $\neg v_i1 \vee \neg v_j1$,
$\neg v_i2 \vee \neg v_j2$, $\neg v_i3 \vee \neg v_j3$.
\end{itemize}
Clearly enough, $M(G)$ can be computed in time polynomial in $|G|$; to be more precise,
when $G$ contains $n$ vertices and $m$ edges, $M(G)$ contains $3*(n+m)$ binary clauses
plus $n$ ternary clauses.
Now, $\omega$ is a polynomial reduction from {\sc 3-colorability} to {\sc L-simplified formula},
i.e., $G$ is 3-colorable if and only if $M(G)$ is L-simplified. Indeed, the four clauses introduced per vertex
state that every vertex $v_i$ must be colored with exactly one of the three colors ($1$, $2$ or $3$),
and the three clauses introduced per edge state that no two adjacent vertices are colored with
the same color. 
If $G$ is not 3-colorable, then $M(G)$ is unsatisfiable, hence it is not L-simplified
(since it is not syntactically equal to the empty clause).
If $G$ is 3-colorable, then $M(G)$ is satisfiable (and a coloring of $G$ can be
directly extracted from a model of $M(G)$). Moreover, it is L-simplified.
Indeed, if it were not the case, then there would exist at least one literal $l_kc$ of
$Lit(M(G))$ s.t. $M(G) \models M(G)_{l_kc \leftarrow 0}$ holds (here $k$ stands for the
index of any variable of $V$ and $c$ for any color in $\{1, 2, 3\}$). 
There are two possibilities for $l_kc$: either $l_kc$ is a positive literal $v_kc$ or
it is a negated one $\neg v_kc$. In the first case, assigning $l_kc$ to $0$ in $M(G)$
amounts to assign $v_kc$ to $0$, while it amounts to assign $v_kc$ to $1$ in the remaining
case. Subsequently, in the first case, $c$ would be a forbidden color for 
the vertex $v_k$ of $V$, while it would be a mandatory color in the second case.
However, in {\sc 3-colorability}, the color names do not matter. Thus, if $I$ is a model
of $M(G)$ encoding a coloring of $G$ and $\tau$ is any permutation over $\{1, 2, 3\}$, 
then $\tau(I)$ also is a model of $M(G)$. Accordingly, as soon as $G$ is 3-colorable,
it cannot be the case that a vertex has a forbidden color or a mandatory color, contradiction.

\fi


% ------------------------------------------------------------------------
% Proofs FORGET
% ------------------------------------------------------------------------

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~ \ref{sema-lite-forg}~~ \em
The set of models of $ForgetLit(\Sigma,\{l\})$ can be expressed 
as:\eatpar

\begin{eqnarray*}
Mod(ForgetLit(\Sigma,\{l\})) 
&=&
Mod(\Sigma) \cup \{ Force(\omega,\neg l) ~|~ \omega \models \Sigma \} \\
&=&
\{ \omega ~|~ Force(\omega,l) \models \Sigma \}
\end{eqnarray*}
\rm

\noindent{\bf Proof:} The proof is obtained immediately from the definition.~\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~ \ref{sema-lits-forg}~~ \em
The set of models of $ForgetLit(\Sigma,L)$ can be expressed as:\eatpar
$$
Mod(ForgetLit(\Sigma,L)) =
\{ \omega ~|~ Force(\omega,L_1) \models \Sigma \mbox{ where } L_1 \subseteq L \}
$$
\rm

\noindent{\bf Proof:} By induction on $|L|$. The base
case in which $L$ is empty is trivial. Let now assume that the property 
holds for any $L$ composed of $k$ elements, and prove that it holds as
well for $L \cup \{l\}$.

By definition,\eatpar

\begin{eqnarray*}
\lefteqn{\omega \models ForgetLit(\Sigma,L \cup \{l\})} \\
& \mbox{ if and only if}&
\omega \models ForgetLit(ForgetLit(\Sigma, L), \{l\})) \\
&\mbox{if and only if}&
\omega \models ForgetLit(\Sigma,L) \mbox{ or } Force(\omega,l) \models ForgetLit(\Sigma,L) \\
&\mbox{if and only if}&
Force(\omega,L') \models ForgetLit(\Sigma,L) \mbox{ where } L' \subseteq \{l\}
\end{eqnarray*}

Using the induction hypothesis, we can express the set of models of
$ForgetLit(\Sigma,L)$ as the models $\omega'$ such that $Force(\omega',L_1) \models
\Sigma$, where $L_1$ is any subset of $L$. As a result,\eatpar

\begin{eqnarray*}
\lefteqn{\omega \models ForgetLit(\Sigma,L \cup \{l\})}\\
&\mbox{if and only if}&
Force(\omega,L')=\omega' \mbox{ and }
Force(\omega',L_1) \models \Sigma,
\mbox{ where } L' \subseteq \{l\} \mbox{ and } L_1 \subseteq L \\
&\mbox{if and only if}&
Force(\omega,L_1') \models \Sigma \mbox{ where } L_1' \subseteq L \cup \{l\}
\end{eqnarray*}

As a result, the models of $ForgetLit(\Sigma,L)$ are the models that can
be mapped into models of $\Sigma$ by forcing a subset of literals in $L$
to become true.~\qed

% ------------------------------------------------------------------------


\noindent{\bf Proposition} ~ \ref{keyforget}~~ \em Let $\Sigma$  be a formula
from $PROP_{PS}$ and $L \subseteq L_{PS}$.  $ForgetLit(\Sigma, L)$ is the
logically strongest consequence of $\Sigma$ that is Lit-independent from $L$
(up to logical equivalence).  \\ \rm

\noindent {\bf Proof:}
By induction on $|L|$. The base case $|L| = 0$ is trivial.
Let us now assume that the proposition holds for every $|L| \leq k$
and show that it remains true when $|L| = k+1$.
Let $L = L' \cup \{l\}$. By the induction hypothesis, we can assume that
$ForgetLit(\Sigma, L')$ is the most general consequence of $\Sigma$ that is
Lit-independent from $L'$. For the sake of simplicity, let $\Sigma'$ denote
this formula. It remains to show that $ForgetLit(\Sigma, L) =
ForgetLit(ForgetLit(\Sigma, L'), \{l\}) = ForgetLit(\Sigma', \{l\})$ is the most general
consequence of $\Sigma'$ that is Lit-independent from $l$. Two cases are to be
considered:\eatpar

\begin{itemize} 

\item $l = x$.
$ForgetLit(\Sigma', x)$ is Lit-independent from $x$ if and only if \\
$ForgetLit(\Sigma', x) \models ForgetLit(\Sigma', x)_{x \leftarrow 0}$ holds.
We have

\[
(\Sigma'_{x \leftarrow 1} \vee (\neg x \wedge \Sigma'))_{x \leftarrow 0}
\equiv (\Sigma'_{x \leftarrow 1} \vee \Sigma'_{x \leftarrow 0})
\]

This formula clearly is a logical consequence of $ForgetLit(\Sigma', \{x\})$. 
Hence $ForgetLit(\Sigma', x)$ is Lit-independent from $x$.
$ForgetLit(\Sigma', x)$ is a logical consequence of $\Sigma'$. Indeed,
for every $\Sigma' \in PROP_{PS}$, $x \in PS$, 
we have $\Sigma' \equiv (x \wedge \Sigma'_{x \leftarrow 1})
\vee (\neg x \wedge \Sigma'_{x \leftarrow 0})$. 
It remains to show that every logical consequence $\Phi$ of $\Sigma'$ that is Lit-independent
from $x$ is a logical consequence of $ForgetLit(\Sigma', x)$.
Let $\Phi$ any formula s.t. $\Sigma' \models \Phi$ holds and 
$\Phi \models \Phi_{x \leftarrow 0}$.
Since $\Sigma' \equiv (x \wedge \Sigma'_{x \leftarrow 1})
\vee (\neg x \wedge \Sigma'_{x \leftarrow 0})$ holds, we have $\Sigma' \models \Phi$ if and only if both
$(x \wedge \Sigma'_{x \leftarrow 1}) \models \Phi$ and
$(\neg x \wedge \Sigma'_{x \leftarrow 0}) \models \Phi$ hold. Thus, in order to show that
$ForgetLit(\Sigma', x) \models \Phi$ holds, it is sufficient to prove that $\Sigma'_{x \leftarrow
1} \models \Phi$ holds. Suppose that is not the case. Then, there exists an implicant $\gamma$ of
$\Sigma'_{x \leftarrow 1}$ that is not an implicant of $\Phi$. However, since 
$(x \wedge \Sigma'_{x \leftarrow 1}) \models \Phi$ holds, we know that $(x \wedge \gamma)$ is an
implicant of $\Phi$. Since $\Phi$ is equivalent to the conjunction of its prime implicates, there
necessarily exists a prime implicate $\pi$ of $\Phi$ s.t. $(x \wedge \gamma) \models \pi$ and
$\gamma \not \models \pi$ hold. This imposes that $x$ belongs to $\pi$ but no literal of $\gamma$
belongs to $\pi$. By construction, $\pi_{x \leftarrow 0}$ is an implicate of 
$\Phi_{x \leftarrow 0}$
and $\pi_{x \leftarrow 0}$ is strictly stronger than $\pi$. 
Since $\Phi \models \Phi_{x \leftarrow
0}$ holds, $\Phi \models \pi_{x \leftarrow 0}$ holds as well. 
This contradicts the fact that $\pi$ is a prime implicate of $\Phi$.

\item $l = \neg x$. The demonstration is similar, {\it mutatis mutandis}.

\end{itemize}\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{forget-or}~~ \em
Let $\Sigma$, $\Phi$  be two formulas from $PROP_{PS}$ and 
$L \subseteq L_{PS}$.
$$ForgetLit(\Sigma \vee \Phi,L) \equiv ForgetLit(\Sigma, L) \vee
ForgetLit(\Phi, L).$$\\ \rm

\noindent {\bf Proof:} The claim can be easily proved from
Proposition~\ref{sema-lits-forg}. Indeed, the models of $ForgetLit(\Sigma \vee
\Phi,L)$ are the models $\omega$ such that $Force(\omega,L_1) \models \Sigma \vee \Phi$,
where $L_1 \subseteq L$. Now, $Force(\omega,L_1) \models \Sigma \vee \Phi$ holds if
and only if $Force(\omega,L_1) \models \Sigma$ holds or $Force(\omega,L_1) \models
\Phi$ holds.

\noindent On the other hand, the models of $ForgetLit(\Sigma, L) \vee ForgetLit(\Phi, L)$
are those such that \\
$Force(\omega,L_1) \models \Sigma$ or $Force(\omega,L_1)
\models \Phi$ for some $L_1 \subseteq L$. This is equivalent to the above
condition.~\qed


\iffalse

\noindent {\em Proof:}
By induction on $|L|$. The base case where $|L| = 0$ is trivial.
Let us now assume that the proposition holds for every $|L| \leq k$
and show that it remains true when $|L| = k+1$.
Let $L = L' \cup \{l\}$. By induction hypothesis, we can assume that
$ForgetLit(\Sigma \vee \Phi, L') \equiv ForgetLit(\Sigma, L') \vee 
ForgetLit(\Phi, L')$.

Let us determine $ForgetLit(\Sigma \vee \Phi, L'\cup \{l\})$.
We have the following chain of equivalences:\eatpar

\begin{eqnarray*}
\lefteqn{ForgetLit(\Sigma \vee \Phi, L'\cup \{l\})} \\
&=& 
ForgetLit(ForgetLit(\Sigma \vee \Phi, L'), \{l\}) \\
&\equiv& 
ForgetLit(ForgetLit(\Sigma, L') \vee ForgetLit(\Phi, L'), \{l\}) \\
&\equiv&
\Big(ForgetLit(\Sigma, L') \vee ForgetLit(\Phi, L') \Big)_{l \leftarrow 1}
\vee
\Big(\neg l \wedge (ForgetLit(\Sigma, L') \vee ForgetLit(\Phi, L'))\Big) \\
&\equiv&
\Big(ForgetLit(\Sigma, L')_{l \leftarrow 1} \vee ForgetLit(\Phi, L')_{l \leftarrow 1}\Big)
\vee
\Big(\neg l \wedge (ForgetLit(\Sigma, L') \vee ForgetLit(\Phi, L'))\Big) \\
&\equiv&
\Big(ForgetLit(\Sigma, L')_{l \leftarrow 1} \vee (\neg l \wedge ForgetLit(\Sigma, L'))\Big)
\vee
\Big(ForgetLit(\Phi, L')_{l \leftarrow 1} \vee (\neg l \wedge ForgetLit(\Phi, L'))\Big) \\
&=&
ForgetLit(\Sigma, L' \cup \{l\}) \vee ForgetLit(\Phi, L' \cup \{l\})
\end{eqnarray*}

This proves the claim.\qed

\fi

\iffalse

Now, since $ForgetLit(\Sigma \vee \Phi, L'\cup \{l\}) = 
ForgetLit(ForgetLit(\Sigma \vee \Phi, L'), \{l\})$,
we have $ForgetLit(\Sigma \vee \Phi, L'\cup \{l\}) \equiv 
ForgetLit(ForgetLit(\Sigma, L') \vee ForgetLit(\Phi, L'), \{l\})$.
By definition, this formula is equivalent to 
$(ForgetLit(\Sigma, L') \vee ForgetLit(\Phi, L'))_{l \leftarrow 1}
\vee (\neg l \wedge (ForgetLit(\Sigma, L') \vee ForgetLit(\Phi, L'))_{l \leftarrow 0})$.
This is also equivalent to 
$(ForgetLit(\Sigma, L')_{l \leftarrow 1} \vee ForgetLit(\Phi, L')_{l \leftarrow 1})
\vee (\neg l \wedge (ForgetLit(\Sigma, L')_{l \leftarrow 0} \vee 
ForgetLit(\Phi, L')_{l \leftarrow 0}))$, which is equivalent to
$(ForgetLit(\Sigma, L')_{l \leftarrow 1} \vee (\neg l \wedge ForgetLit(\Sigma, L')_{l \leftarrow 0}))
\vee 
(ForgetLit(\Phi, L')_{l \leftarrow 1} \vee (\neg l \wedge ForgetLit(\Phi, L')_{l \leftarrow 0}))$.
Finally, this formula is equivalent to $ForgetLit(\Sigma, L' \cup \{l\}) \vee
ForgetLit(\Phi, L' \cup \{l\})$, Q.E.D.
\qed

\fi

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{forgetterms} ~~ \em
Let $\gamma$ be a consistent term from $PROP_{PS}$ and $L \subseteq L_{PS}$.\\
$ForgetLit(\gamma, L) \equiv \bigwedge_{l \in \gamma s.t. l \not \in L} l$.
\\ \rm

\noindent{\bf Proof}: We first prove the following lemma:

\begin{lemma}
For any consistent term $\gamma$,
we have $ForgetLit(\gamma,l) \equiv \gamma\setminus\{l\}$.
\end{lemma}

{\em Proof (lemma)}: 
\begin{description}
\item[case 1] $l \in \gamma$, {\em i.e.}, $\gamma = l \wedge
\gamma'$.\\
	$ForgetLit(\gamma,l) \equiv \gamma_{l\leftarrow 1}\vee (\neg l
\vee\gamma) \equiv \gamma' \equiv \gamma\setminus\{l\}$.
\item[case 2] $\neg l \in \gamma$, {\em i.e.}, $\gamma = 
\neg l \wedge \gamma'$.\\
	$ForgetLit(\gamma,l) \equiv \bot \vee \gamma \equiv
\gamma \equiv \gamma\setminus\{l\}$.
\item[case 3] $l \not \in \gamma$ and $\neg l \not \in \gamma$.\\
	$ForgetLit(\gamma,l) \equiv \gamma\vee(\neg l\vee\gamma)
\equiv \gamma \equiv \gamma\setminus\{l\}$.
\end{description} \qed

A straightforward induction on $L$ completes the proof. \qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{forget-IP}~~ \em
Let $\Sigma$  be a formula from $PROP_{PS}$ and $L \subseteq L_{PS}$.\\
$IP(ForgetLit(\Sigma, L)) = \{\delta \ | \ \delta \in IP(\Sigma)$ and
$Lit(\delta) \cap L = \emptyset\}$.
\\ \rm

\noindent {\bf Proof:}
\begin{itemize}
\item $\subseteq$: Let $\delta \in IP(ForgetLit(\Sigma, L))$. Since $\Sigma \models
ForgetLit(\Sigma, L)$ and $ForgetLit(\Sigma, L) \models \delta$ hold, $\delta$ is an implicate
of $\Sigma$. Hence, there exists a prime implicate $\delta'$ of $\Sigma$ s.t.
$\delta' \models \delta$ holds. Since $\delta$ does not contain any literal from $L$,
this is also the case for $\delta'$. Thus, $\delta'$ is a logical consequence of $\Sigma$
that is Lit-independent from $L$. As a consequence of Proposition \ref{keyforget},
it must be the case that $ForgetLit(\Sigma, L) \models \delta'$. Hence, there exists a prime
implicate $\delta''$ of $ForgetLit(\Sigma, L)$ s.t. $\delta'' \models \delta'$ holds.
This implies that $\delta'' \models \delta$ holds as well, and since both clauses are
prime implicates of the same formula, they are equivalent. But this implies that
$\delta \equiv \delta'$ holds, which completes the proof.
\item $\supseteq$: Let $\delta$ be a prime implicate of $\Sigma$ that does not contain
any literal from $L$. $\delta$ is Lit-independent from $L$. Since $\delta$ is an implicate
of $\Sigma$, it must also be an implicate of $ForgetLit(\Sigma, L)$.
Subsequently, there exists a prime implicate $\delta'$ of $ForgetLit(\Sigma, L)$
s.t. $\delta' \models \delta$ holds. Since $\Sigma \models ForgetLit(\Sigma, L)$ and
$ForgetLit(\Sigma, L) \models \delta'$ both hold, we have $\Sigma \models \delta'$ as well.
Hence, there exists a prime implicate $\delta''$ of $\Sigma$ s.t. $\delta'' \models \delta'$ holds.
Therefore, $\delta'' \models \delta$ holds and since both clauses are prime implicates of the
same formula, they are equivalent. But this implies that 
$\delta \equiv \delta'$ holds, which
completes the proof.
\end{itemize}
\qed

% ------------------------------------------------------------------------
\noindent {\bf Proposition}~\ref{forgetvar-forgetlit}~~ \em
Let $\Sigma$  be a formula from $PROP_{PS}$ and $V \subseteq PS$.
We have\eatpar

\[
ForgetVar(\Sigma, V) \equiv ForgetLit(\Sigma, L_V)
\]

\rm

\noindent {\bf Proof:}
By induction on $|V|$. The proposition trivially holds for $|V| = 0$.
Let us assume it is true whenever $|V| = k$. Let $V = \{v_1, ..., v_{k+1}\}$.
By definition, we have\eatpar

\[
ForgetVar(\Sigma, V) = ForgetVar(ForgetVar(\Sigma, \{v_1, ..., v_k\}),
\{v_{k+1}\})
\]

By the induction hypothesis, $ForgetVar(\Sigma, V)$ is equivalent to
$ForgetVar(\Phi,\{v_{k+1}\})$, where $\Phi$ is defined as:\eatpar

\iffalse
\[
ForgetVar(ForgetLit(\Sigma,
\{x ; x \in \{v_1,\ldots, v_k\}\} \cup \{\neg x ; x \in \{v_1,\ldots, v_k\}\}),
\{v_{k+1}\})
\]

For simplicity, let us define $\Phi$ as follows

\fi

\[
\Phi = ForgetLit(\Sigma, \{x ; x \in \{v_1,\ldots, v_k\}\} \cup \{\neg x ; x \in 
\{v_1,\ldots, v_k\}\})
\]


We have $ForgetVar(\Sigma, V) \equiv ForgetVar(\Phi, \{v_{k+1}\})$.
By definition,

\[
ForgetVar(\Phi, v_{k+1}) = \Phi_{v_{k+1} \leftarrow 0} \vee
\Phi_{v_{k+1} \leftarrow 1}.
\]

We also have\eatpar

\begin{eqnarray*}
\lefteqn{ForgetLit(\Phi, \{v_{k+1}, \neg v_{k+1}\})} \\
&=&
ForgetLit(ForgetLit(\Phi, \{v_{k+1}\}), \{\neg v_{k+1}\}) \\
&=&
ForgetLit((\neg v_{k+1} \wedge \Phi_{v_{k+1} \leftarrow 0}) \vee
                               \Phi_{v_{k+1} \leftarrow 1}, \{\neg v_{k+1}\}) \\
&=&
(v_{k+1} \wedge ((\neg v_{k+1} \wedge \Phi_{v_{k+1} \leftarrow 0}) \vee 
\Phi_{v_{k+1} \leftarrow 1})_{v_{k+1} \leftarrow 1}) \vee ((\neg v_{k+1} 
\wedge \Phi_{v_{k+1} \leftarrow 0}) \vee
\Phi_{v_{k+1} \leftarrow 1})_{v_{k+1} \leftarrow 0}.
\end{eqnarray*}

This simplifies to $(v_{k+1} \wedge \Phi_{v_{k+1} \leftarrow 1}) \vee
\Phi_{v_{k+1} \leftarrow 0} \vee \Phi_{v_{k+1} \leftarrow 1}$, which is also equivalent to
$\Phi_{v_{k+1} \leftarrow 0} \vee \Phi_{v_{k+1} \leftarrow 1}$, hence equivalent to
$ForgetVar(\Phi, \{v_{k+1}\})$. Consequently, we have\eatpar

\begin{eqnarray*}
\lefteqn{ForgetVar(\Sigma, V)} \\
&\equiv&
ForgetLit(ForgetLit(\Sigma, \{x ; x \in \{v_1,\ldots, v_k\}\} \cup \{\neg x ; x \in 
\{v_1,\ldots, v_k\}\}), \{v_{k+1}, \neg v_{k+1}\}) \\
&\equiv&
ForgetLit(\Sigma, V).
\end{eqnarray*}
\qed


% ------------------------------------------------------------------------
\noindent{\bf Proposition}~\ref{forg-and-ind}~~ \em
Let $\Sigma$, $\Phi$ be two formulas from $PROP_{PS}$, and
$V$ be a subset of $PS$. If $V \not \leadsto_{-}^{+} \Sigma$, then $ForgetVar(\Sigma \wedge
\Phi, V) \equiv \Sigma \wedge ForgetVar(\Phi, V)$.
\\ \rm

\noindent {\bf Proof:} Let us consider the case where $V = \{v\}$.
By definition, we have $ForgetVar(\Sigma \wedge \Phi, \{v\})
= (\Sigma \wedge \Phi)_{v \leftarrow 0} \vee (\Sigma \wedge \Phi)_{v \leftarrow 1}$.
Equivalently, $ForgetVar(\Sigma \wedge \Phi, \{v\}) \equiv
(\Sigma_{v \leftarrow 0} \wedge \Phi_{v \leftarrow 0}) \vee (\Sigma_{v \leftarrow 1} 
\wedge \Phi_{v \leftarrow 1})$. When $v \not \leadsto_{-}^{+} \Sigma$, we have
$\Sigma \equiv \Sigma_{v \leftarrow 0} \equiv \Sigma_{v \leftarrow 1}$.
Accordingly, $ForgetVar(\Sigma \wedge \Phi, \{v\}) \equiv
\Sigma \wedge (\Phi_{v \leftarrow 0} \vee \Phi_{v \leftarrow 1})
\equiv \Sigma \wedge Forget(\Phi, \{v\})$.
A straightforward induction completes the proof. \qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{circ}~~ \em
Let $\Sigma$, $\Phi$  be two formulas from $PROP_{PS}$, and $P$, $Q$, $Z$ be 
three disjoint sets of variables from $PS$ 
(such that $Var(\Sigma) \cup Var(\Phi) \subseteq P \cup Q \cup Z$).
It holds:\eatpar

\begin{enumerate}
\item If $\Phi$ does not contain any variable from $Z$

\begin{eqnarray*}
& CIRC(\Sigma, \langle P, Q, Z\rangle) \models \Phi & \\
& \mbox{ ~~ if and only if ~~ } & \\
& \Sigma \models ForgetLit(\Sigma \wedge \Phi, L_P^- \cup L_Z) &
\end{eqnarray*}

\item In the general case:

\begin{eqnarray*}
& CIRC(\Sigma, \langle P, Q, Z\rangle) \models \Phi & \\
& \mbox{ ~~ if and only if ~~ }& \\
& \Sigma \models ForgetLit(\Sigma \wedge \neg ForgetLit(\Sigma 
\wedge \neg \Phi, L_Z \cup L_P^{-}), L_Z \cup L_P^{-}) &
\end{eqnarray*}
\end{enumerate}

\noindent where $CIRC$ is circumscription as defined in \cite{McCarthy86}.
\\ \rm

\noindent {\bf Proof:}
\begin{enumerate}
\item This is a consequence of Theorem 2.5 from \cite{Przymusinski89}.
This theorem states that if $\Phi$ does not contain literals from $Z$, then $CIRC(\Sigma,
\langle P, Q, Z\rangle) \models \Phi$ holds if and only if there is no clause $\gamma$ s.t.
$\gamma$ does not contain any literal from $L_P^- \cup L_Z$ and
$\Sigma \models \neg \Phi \vee \gamma$ but $\Sigma \not \models \gamma$.
This is equivalent to state that, if $\Phi$ does not contain literals from $Z$, then $CIRC(\Sigma,
\langle P, Q, Z\rangle) \models \Phi$ holds if and only if, for every clause $\gamma$
containing only literals from $L_P^+ \cup L_Q$, we have $\Sigma \wedge \Phi \models \gamma$
if and only if $\Sigma \models \gamma$. It is easy to see that the equivalence is preserved would
any formula $\gamma$ Lit-independent from $L_P^- \cup L_Z$ be considered (any formula can be turned 
into an equivalent CNF formula). Thus, Theorem 2.5 can be rephrased in forgetting terms:
if $\Phi$ does not contain variables from $Z$, then $CIRC(\Sigma, \langle P, Q, Z\rangle) 
\models \Phi$ holds if and only if $\Sigma \wedge \Phi \equiv_{L_P^+ \cup L_Q} \Sigma$
if and only if $\Sigma \models ForgetLit(\Sigma \wedge \Phi, L_P^- \cup L_Z)$.

\item This is a consequence of Theorem 2.6 from \cite{Przymusinski89}.
This theorem states that $CIRC(\Sigma, \langle P, Q, Z\rangle) \models \Phi$ holds 
if and only if $\Sigma \models \Phi$ or there exists a formula $\Psi$ s.t. 
$\Psi$ does not contain any literal from $L_P^- \cup L_Z$, $\Sigma \models \Phi \vee \Psi$ holds
and $CIRC(\Sigma, \langle P, Q, Z\rangle) \models \neg \Psi$.
It is easy to see that such a formula $\Psi$ exists if and only if the conjunction $\alpha$ 
of all the formulas $\Psi$ such that $\Psi$ does not contain any literal from $L_P^- \cup L_Z$
and $\Sigma \models \Phi \vee \Psi$ holds is s.t. 
$CIRC(\Sigma, \langle P, Q, Z\rangle) \models \neg \alpha$.
Since $\Sigma \models \Phi \vee \Psi$ holds if and only if $\Sigma \wedge \neg \Phi
\models \Psi$ holds, $\alpha$ is equivalent to $ForgetLit(\Sigma \wedge \neg \Phi, L_P^- \cup L_Z)$.
Thus, $CIRC(\Sigma, \langle P, Q, Z\rangle) \models \Phi$ holds if and only if
$\Sigma \models \Phi$ holds or $CIRC(\Sigma, \langle P, Q, Z\rangle) \models \neg 
ForgetLit(\Sigma \wedge \neg \Phi, L_P^- \cup L_Z)$ holds. In the case where 
$\Sigma \models \Phi$ holds, $\Sigma \wedge \neg \Phi$ is inconsistent, so it is also
the case of $ForgetLit(\Sigma \wedge \neg \Phi, L_P^- \cup L_Z)$. Thus, if
$\Sigma \models \Phi$ holds, $CIRC(\Sigma, \langle P, Q, Z\rangle) \models \neg 
ForgetLit(\Sigma \wedge \neg \Phi, L_P^- \cup L_Z)$ holds as well.
Accordingly, $CIRC(\Sigma, \langle P, Q, Z\rangle) \models \Phi$ holds if and only if
$CIRC(\Sigma, \langle P, Q, Z\rangle) \models \neg  
ForgetLit(\Sigma \wedge \neg \Phi, L_P^- \cup L_Z)$ holds. Since
$ForgetLit(\Sigma \wedge \neg \Phi, L_P^- \cup L_Z)$ does not contain any literal from
$Z$, the point just above enables concluding the proof.
\end{enumerate} \qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{forget-not-polsize} ~~ \em
Let $\Sigma$ be a formula from $PROP_{PS}$ and
let $L$ be a subset of $L_{PS}$.
In the general case, there is no propositional formula $\Phi$
equivalent to $ForgetLit(\Sigma, L)$ s.t. the size of $\Phi$ is
polynomially bounded in $|\Sigma|+|L|$, unless {\sf NP} $\cap$ {\sf coNP}
$\subseteq$ {\sf P/poly}.\\ \rm

\noindent {\bf Proof:} The justification is twofold:

\noindent (1) $ForgetLit(\Sigma, L)$ is the logically strongest consequence of
$\Sigma$ that is Lit-independent from $L$. Consequently, for every formula
$\gamma \in PROP_{PS}$, we have $\Sigma \models \gamma$ if and only if $ForgetLit(\Sigma,
L) \models \gamma$, where $L = Lit(\Sigma) \setminus Lit(\gamma)$.  Because
$ForgetLit(\Sigma, L)$ depends only on literals of $Lit(\Sigma) \cap
Lit(\gamma)$, it is an {\em interpolant} of $\Sigma$ and $\gamma$, i.e., a formula
$\varphi$ s.t. $\Sigma \models \varphi$ and $\varphi \models \gamma$ hold; thus we have
$\Sigma \models ForgetLit(\Sigma, Lit(\Sigma) \setminus Lit(\gamma)) \models
\gamma$.

\noindent (2) the existence of a propositional formula, interpolant of $\Sigma$
and $\gamma$, and of size polynomially bounded in $|\Sigma|+|\gamma|$ would
imply that {\sf NP} $\cap$ {\sf coNP} $\subseteq$  {\sf P/poly}
\cite{BoppanaSipser90}, which is considered very unlikely in complexity theory.
\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{comp-LVequivalence}~~ \em
{\sc Lit-equivalence} and {\sc Var-equivalence} are $\Pi_2^p$-complete.
\\ \rm

\noindent {\bf Proof:}
\begin{itemize}

\item Var-equivalence.

\begin{itemize}

\item Membership: In order to check the membership to the complementary
problem, guessing a clause $\gamma$ built up from $V$, and checking that
($\Sigma \models \gamma$ and $\Phi \not \models \gamma$) or ($\Sigma \not
\models \gamma$ and $\Phi \models \gamma$) is sufficient. The check step can be
easily accomplished in polynomial time when an {\sf NP} oracle is available.
Hence, the complementary problem belongs to $\Sigma_2^p$.

\item Hardness: Let $M$ be the mapping that associates the triple
$\langle \Sigma, true, A\rangle$ to the 
quantified boolean formula $\forall A \exists B \Sigma$ 
(where $\{A, B\}$ is a partition of $Var(\Sigma)$). Clearly enough, $M$ is polytime.
Moreover, we have:\eatpar

\begin{eqnarray*}
\forall A \exists B \Sigma \mbox{ is valid}
& \mbox{if and only if} &
\models \exists B \ . \ \Sigma\\
& \mbox{if and only if} &
\models ForgetVar(\Sigma, B) \\
& \mbox{if and only if} &
\Sigma \equiv_A true
\end{eqnarray*}

Since the validity problem for \2qbfbarre formulas 
is $\Pi_2^p$-complete, this proves the $\Pi_2^p$-hardness of 
{\sc Var-equivalence}.

\end{itemize}

\item Lit-equivalence.

\begin{itemize}

\item Membership: See the membership proof above, replacing ``built up from $V$''by
``s.t. $Lit(\gamma) \subseteq L$''.

\item Hardness: Let $M$ be the mapping that associates $\langle \Sigma, \Phi, V\rangle$ to
$\langle \Sigma, \Phi, L_V\rangle$. Clearly
enough, $M(\langle \Sigma, \Phi, V\rangle)$ can be computed in time polynomial in
$|\langle \Sigma, \Phi, V\rangle|$. We have shown that $\Sigma$ and $\Phi$ are Var-equivalent given $V$
if and only if $\Sigma$ and $\Phi$ are Lit-equivalent given $L_V$.
Hence, $M$ is a polynomial many-one reduction from {\sc Var-equivalence} to {\sc Lit-equivalence}.
Since {\sc Var-equivalence} is $\Pi_2^p$-hard, this is also the case for {\sc Lit-equivalence}.

\end{itemize}
\end{itemize}
\qed

% ------------------------------------------------------------------------
% PROOFS OTHER 
% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{infl} ~~ \em
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is influenceable from $V$ if and only if $\Sigma$ is Var-dependent 
on $V$.
\\ \rm

\noindent {\bf Proof:}
Proposition 4 from \cite{Boutilier94} states that $\Sigma$ is influenceable 
from $V$ if and only if there exists 
a prime implicant of $\Sigma$ that contains a variable from $V$, where $V$ is 
the set of controllable variables. Proposition \ref{primev} completes the 
proof.
\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{rtsm} ~~ \em
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is relevant to $V$ if and only if $\Sigma$ is Var-dependent on $V$.
\\ \rm

\noindent {\bf Proof:} The proof is trivial from Proposition \ref{primev}.
\qed

% ------------------------------------------------------------------------

\noindent{\bf Proposition}~\ref{srsm1} ~~ \em
Let $\Sigma$ be a formula from $PROP_{PS}$ and $V$ a subset of $PS$.
$\Sigma$ is strictly relevant to $V$ if and only if 
$\Sigma$ is Var-dependent on $V$ and Var-independent from 
$Var(\Sigma) \setminus V$.
\\\ \rm

\noindent {\bf Proof:}
Easy from the definition of strict relevance, plus Proposition \ref{primev} ($\Sigma$ is Var-dependent
from every variable occurring in a prime implicate of $\Sigma$ and 
Var-independent from all the remaining variables).\qed

% ------------------------------------------------------------------------


\noindent{\bf Proposition}~\ref{comp-strict-rel}\\ \em
(1) {\sc strict relevance 
of a formula to a subject matter} \cite{Lakemeyer95} is $\Pi_2^p$-complete.\\
(2) {\sc strict relevance 
of a formula to a subject matter} \cite{Lakemeyer97} is \bh2-complete.
\\ \rm

\noindent {\bf Proof:} 

\begin{itemize}
\item {\bf strict relevance \cite{Lakemeyer95}} 

\begin{itemize}
\item Membership. Let us consider the complementary problem. Guess a clause
$\gamma$, check that it does not contain any variable from $V$ (this can be
achieved in time polynomial in $|\gamma|+|V|$, hence in time polynomial in
$|\Sigma|+|V|$ since no prime implicate of $\Sigma$ can include a variable that
does not occur in $\Sigma$). Then check that it is an implicate of $\Sigma$
(one call to an {\sf NP} oracle) and check that every subclause of $\gamma$
obtained by removing from it one of its k literals is not an implicate of
$\Sigma$ ($k$ calls to an {\sf NP} oracle). Since only $k+1$ calls to such an
oracle are required to check that $\gamma$ is a prime implicate of $\Sigma$,
the complementary problem of {\sc strict relevance} belongs to $\Sigma_2^p$.
Hence, {\sc strict relevance} belongs to $\Pi_2^p$.

\item Hardness. Let $\{A, B\}$ be a partition of $Var(\Sigma)$ (for any formula
$\Sigma$). $\forall A \exists B \Sigma$ is valid if and only if every
prime implicate of $\Sigma$ that contains a variable from $A$ also contains a
variable from $B$ if and only if every prime implicate of $\Sigma$ contains a variable
from $B$ (since $Var(\Sigma) = A \cup B$) if and only if $\Sigma$ is strictly relevant to
$B$.

\end{itemize}

\item {\bf strict relevance \cite{Lakemeyer97}}

\begin{itemize}
\item Membership: Straightforward from Propositions~\ref{srsm1} and
 ~\ref{cflfv}.
\item Hardness: By exhibiting a polynomial reduction from {\sc 
sat-unsat} to {\sc strict relevance of a formula to a subject matter}.
To any pair $\langle \phi, \psi \rangle$ of propositional formulas, 
let $rename(\psi)$ be a formula obtained from $\psi$ by
renaming its variables. Obviously,\\
(i) $rename(\psi)$ is satisfiable if and only if $\psi$ is.\\
Now, let $new$ be a new variable, let \\
\centerline{$\Sigma = \phi \wedge new \wedge \neg rename(\psi)$}
\noindent and $V = Var(\phi) \cup \{new\}$.
By Proposition 8, $\Sigma$ is Var-dependent on $V$ if and only if there is a
prime implicant of $\Sigma$ mentioning a variable from $V$, i.e.,
if and only if $\phi \wedge \neg rename(\psi)$ is satisfiable, thus, using (i):\\
(ii) $\Sigma$ is Var-dependent on $V$ if and only if both $\phi$ and $\neg \psi$ 
are satisfiable.\\
Then, again after Proposition 8, $\Sigma$ is Var-independent from
$Var(\Sigma) \setminus V = Var(rename(\psi))$ if and only if no prime implicant of 
$\Sigma$ mentions a variable from $Var(rename(\psi))$, i.e., if and only if $rename(\psi)$ is 
unsatisfiable, thus, using (i):\\ 
(iii) $\Sigma$ is Var-independent from $Var(\Sigma) \setminus V$ if and only if 
$\psi$ is satisfiable.

Thus, from Proposition~\ref{srsm1}, (ii) and (iii), we get that $\Sigma$ is 
strictly relevant to $V$ if and only if $\phi$ is satisfiable and $rename(\psi)$ is not.
\end{itemize}
\end{itemize}
\qed

% ------------------------------------------------------------------------

\newpage

\section*{Appendix B: Glossary}

Here is a small glossary of useful terms with the place where their
definition can be found.\\

\begin{tabular}{lll}
$PROP_{V}$ & propositional language generated by $V$ & Section \ref{prelipl}\\
$L_{V}$ & set of literals built up from $V$ & Section \ref{prelipl}\\
$L_V^+$ & set of positive literals built up from $V$ & Section \ref{prelipl}\\
$L_V^-$ & set of negative literals built up from $V$ & 
Section \ref{prelipl}\\
$Var(\Sigma)$ & set of propositional variables appearing in
$\Sigma$ & Section \ref{prelipl}\\
NNF & negation normal form & Section \ref{prelipl}\\
$Lit(\Sigma)$ & set of literals occurring in the NNF of $\Sigma$ & 
Section \ref{prelipl}\\
$\omega_V$ & a $V$-world (instantiations of all variables of $V$) & 
Section \ref{prelipl}\\
$\Omega_V$ & set of all $V$-worlds & Section \ref{prelipl}\\
$\omega$ & world (full instanciation) & Section \ref{prelipl}\\
$Mod(\Sigma)$ & set of models of $\Sigma$ & Section \ref{prelipl}\\
$for(S)$ & formula such that $Mod(\Sigma) = S$ & Section \ref{prelipl}\\
$\Sigma_{x \leftarrow 0}$ &  & Section \ref{prelipl}\\
$\Sigma_{x \leftarrow 1}$ &  & Section \ref{prelipl}\\
$\Sigma_{l \leftarrow 1}$ &  & Section \ref{prelipl}\\
$Force(\omega,l)$ & & Section \ref{prelipl}\\
$IP(\Sigma)$ & set of prime implicates of $\Sigma$ &
Section \ref{prelipl}\\
$PI(\Sigma)$ & set of prime implicants of $\Sigma$ &
Section \ref{prelipl}\\
$\mbox{{\sf BH}}_2$, $\mbox{{\sf coBH}}_2$ & & Section \ref{prelicc}\\
$\Delta_2^p$, $\Sigma_2^p$, $\Pi_2^p$ & & Section \ref{prelicc}\\
& syntactical Lit-dependence & Definition \ref{defsfl}\\
& syntactical Var-dependence & Definition \ref{defsfv}\\
$l \leadsto \Sigma$ & (semantical) Lit-dependence & Definition 
\ref{semflindep}\\
$DepLit(\Sigma)$ &  literals  such that $l \leadsto \Sigma$ &
Definition \ref{semflindep}\\
$v \leadsto_{-}^{+}\Sigma$ & (semantical) Var-dependence & Definition
\ref{semfvindep}\\
$DepLit(\Sigma)$ & variables such that $l \leadsto \Sigma$ &
Definition \ref{semfvindep}\\
{\em Lit-simplified} & &  Definition \ref{defsimplified}\\
{\em Var-simplified} & &  Definition \ref{defsimplified}\\
$ForgetLit(\Sigma, L)$ & literal forgetting &  Definition \ref{deflf}\\
$ForgetVar(\Sigma, L)$ & variable forgetting  &  Definition \ref{defvf}\\
$\Sigma \equiv_L \Phi$ & Lit-equivalence & Definition \ref{defequiv}\\
$\Sigma \equiv_V \Phi$ & Var-equivalence & Definition \ref{defequiv}\\
& influenceability & Definition \ref{definflu}\\
& relevance to a subject matter & Definition \ref{defrsm}\\
& strict relevance to a subject matter & Definition \ref{defsrsm}
\end{tabular}

\newpage
\bibliographystyle{theapa}
\bibliography{long-string,local}

%%%%%%%%%%%%%%%%
\end{document}
%%%%%%%%%%%%%%%%


