11institutetext: Pontifica Universidad Catolica de Chile, Chile.
11email<EMAIL_ADDRESS>22institutetext: Department of Computer
Science and Engineering, IIT Ropar, India.
22email<EMAIL_ADDRESS>
# Extending Prolog for Quantified Boolean Horn Formulas

Anish Mallick 11 Anil Shukla 22

###### Abstract

Prolog is a well known declarative programming language based on propositional
Horn formulas. It is useful in various areas, including artificial
intelligence, automated theorem proving, mathematical logic and so on. An
active research area for many years is to extend Prolog to larger classes of
logic. Some important extensions of it includes the constraint logic
programming, and the object oriented logic programming. However, it cannot
solve problems having arbitrary quantified Horn formulas.

To be precise, the facts, rules and queries in Prolog are not allowed to have
arbitrary quantified variables. The paper overcomes this major limitations of
Prolog by extending it for the quantified Boolean Horn formulas. We achieved
this by extending the SLD-resolution (SLD-Res) proof system for quantified
Boolean Horn formulas, followed by proposing an efficient model for
implementation. The paper shows that the proposed implementation also supports
the first-order predicate Horn logic with arbitrary quantified variables.

The paper also introduces for the first time, a declarative programming for
the quantified Boolean Horn formulas.

##  1 Introduction

Prolog is a declarative programming language developed by Alain Colmerauer,
Bob Pasero and Philippe Roussel in 1972 [31, 8]. It was first designed for
solving problems related to natural language processing. Very soon, arithmetic
aspects of logic was added to it, using the ideas from Robert Kowalski SL-
resolution prover [24]. Today, Prolog is useful not only in the areas of
language processing and automated theorem proving, but also in the areas of
artificial intelligence, relational database, and design automation to name a
few.

Prolog is, in a way an interactive system, which supports a kind of man-
machine conversation. That is, a user is allowed to specify some relevant
knowledge and subsequently ask it valid questions regarding the same. For
example, one may specify several facts about a family, say family members and
their relationships, along with some specific rules, for example a rule about
siblings. Then one may ask if two elements in the space are siblings?

In Prolog, facts and rules are defined first then query follows. Though all
facts and rules have to be predicate horn formulas with quantifiers, any rules
defined have to be univerally quantified. For example,

$\displaystyle\forall x,y~{}female(x)\wedge parent(x,y)\rightarrow
mother(x,y)$

is a valid rule but

$\displaystyle\forall x,y\exists z~{}parent(z,x)\wedge parent(z,y)\rightarrow
sibling(z,y)$

is not.
On the other hand for queries we are allowed logical Horn clauses with
existential quantifiers only. For example,

$\displaystyle\hskip 17.07164pt\exists x.parent(x,bob)$

is a valid query but

$\displaystyle\hskip 17.07164pt\exists x\forall y.ancestor(x,y)$

is not. The primary focus of this work is to remove these limitations (see,
[33, Chapter 14] for reference) and extend the scope of Prolog to handle
larger class of problems. We also propose an efficient algorithm to the
problem

$\displaystyle\hskip 17.07164pt\text{Is
}\mathcal{F}=\Pi.\phi\implies\Pi.(\phi\wedge C)?,$

where, $\mathcal{F}$ is a first-order predicate Horn formula, and $C$ a first-
order predicate Horn clause. Note that the above problem is in general
undecidable [15, 37]. The efficiency lies in the fact that the algorithm will
detect loop or infinite braching in linear time and stop. It should be clear
that we are not claiming that any SLD-Q-resolution (Definition 3) will not
halt if this algorithm outputs loop, just that it will determine possiblity of
not halting following the current course of action. So this should not be
viewed as an attempt towards halting problem but a contigency. These are
explained further in the following section.

###  1.1 Our Contributions

In this section we summarize the contribution of this article.

  1. 1.

Extending Prolog for quantified Boolean Horn formulas. A Prolog algorithm can
be expressed as logical part plus control part. Logical part is expressed as
facts and rules. The facts and rules are represented as (propositional) Horn
formulas (Section 2.5.2). The control part is based on the SLD-Res proof
system (Definition 1). In particular, once a query clause $C$ is presented by
the user, Prolog control tries to find an SLD-Res refutation of $\neg C$, and
accordingly return the answer.

The article extended the SLD-Res proof systems for the quantified Boolean Horn
formulas and defined the SLD-Q-Res proof system (Section 3). Quantifed Boolean
Horn formulas are all QBFs in closed prenix form with CNFs in which every
clause has at most one positive literal (Definition 2). The article shows that
SLD-Q-Res is sound and complete for the quantified Boolean Horn formulas and
also proposes an efficient implementation for the same. That is, given a
quantified Boolean Horn formula $\mathcal{F}=\Pi.\phi$ as facts and rules, and
a quantified Horn query clause $C$, the paper proposes an efficient algorithm
(Algorithm 2) to answer the following:

$\displaystyle\text{Is }\mathcal{F}=\Pi.\phi\implies\Pi.(\phi\wedge C)?$

Obviuosly, one may encode verification problems as a quantified Boolean Horn
formulas [2, 5, 30], which in general is undecidable. Our proposed algorithm
is efficient in the sense that it can detect a possible loop during evaluation
efficiently.

As a result, the article allows us to specify facts and rules as a quantified
Boolean Horn formulas with quantified query clause. Refer Section 6.1 for an
application.

The article shows how our efficient algorithm (Algorithm 2) handles the first-
order predicate Horn logic as well. To be precise, the article shows that
given facts, rules and queries as first-order predicate Horn clauses,
Algorithm 2 solves efficiently the above implication problem.

  2. 2.

Overcomes the weaknesses of existing Prolog. As already discussed, Prolog does
not allow arbitrary quantified variables in facts, rules and queries. All
variables appearing in facts and rules are universally quantified and all
variables appearing in the query are existentially quantified. These
limitations arise due the Prolog control (engine) part, which is based on SLD-
Res proof systems for Horn formulas.

This article overcomes the limitations of the existing Prolog by allowing
arbitrary quantified variables in facts, rules and queries. As a result
several problems which were impossible to be solved via existing Prolog can
now be attempted. We present few examples below after few comments.

The encoding of the problem statement of the Example 1 and Example 2 (below)
uses only universally quantified variables and can be specified in the
existing Prolog. However, the query of the corresponding problem cannot be
specified in the existing Prolog as it requires universally quantified
variables.

The encoding of the problem statement and the query of the Example 3 (below)
uses both the existentially and universally quantified variables, and so
cannot be specified in the existing Prolog. However, the problem is easily
handled by the extended Prolog (QBF-Prolog, Section 4) of this article.

######  Example 1.

Tree-bipartite-problem: Consider the problem related to trees and bipartite
graphs. Recall, a graph $G=(V,E)$ is said to be bipartite iff its vertex set
$V$ can be partitioned into two parts $U$ and $W$ such that every edge in $E$
connects a vetex in $U$ to a vertex in $W$. Consider the following: undirected
graphs without cycle are bipartite, and trees are acyclic. These facts can be
encoded as rules in the existing Prolog. However, consider the following
query: are trees bipartite?

The query required universal variables, and hence cannot be handled by the
existing Prolog. However, the extended Prolog of the paper is capable to
handle the problem. For the detailed encoding and solution of the problem,
refer Section 6.2.

######  Example 2.

Bipartite problem: Consider a Prolog program which specifies the set of all
bipartite graphs $G$. One can easily encode bipartite graphs in first-order
predicate Horn logic using only universally quantified variables. Hence, this
can be encoded in the existing Prolog. But, consider the following query
regarding a bipartite graph $G=(\\{U,W\\},E)$: pick a vertex $x$ belonging to
$U$ and move to some vertex $y$ using an edge $\\{x,y\\}$ and from $y$ again
move to a vertex $z$ using the edge $\\{y,z\\}$. Is the vertex $z\in U$?

Obviously, the above query is valid and needed universal variables in the
encoding. Hence, the existing Prolog does not supports such queries. However,
the present paper extend Prolog to handle such queries as well. For the
detailed encoding of the bipartite problem, refer Section 6.3.

######  Example 3.

Simple relations: The problem uses the following predicates:

$\displaystyle P(h,k)~{}~{}\text{/* the predicate is 1 iff }k=2h*/$
$\displaystyle R(h,k)~{}~{}\text{/* the predicate is 1 iff }h<k*/$

We may give several interpretations to these predicates. For example, if $k$
and $h$ represent graphs, then the predicate $R(k,h)$ is $1$ iff the graph $h$
is a subgraph of the graph $k$. The predicate $P(k,h)$ is $1$ iff the graph
$k$ is a superset of the graph $h$. That is, the graph $k$ is constructed from
$h$ by say adding a vertex.

Let us now consider the following rules:

$\displaystyle\forall h,k.P(h,k)\rightarrow R(h,k)~{}~{}\text{/* rule 1 */}$
$\displaystyle\forall h_{1},h_{2},h_{3}.[R(h_{1},h_{2})\wedge
R(h_{2},h_{3})]\rightarrow R(h_{1},h_{3})~{}~{}\text{ /* rule 2 */}$

Now consider the following query:

$\displaystyle\forall h\exists g,k.[P(h,g)\wedge P(g,k)]\rightarrow
R(h,k)~{}~{}\text{ /* query */}$

Clearly the query is correct according to our interpretation. We show that
this problem can be easily solved by the QBF-Prolog of this article. For the
detailed encoding and solution of the problem, refer Section 6.4.

Finally, we show an example (Example 4) which cannot be handled by the
existing Prolog, but also cannot be solved via the extended Prolog. The proofs
of such problems are induction based, however, our algorithm is unable to
mimic the inductive proof and just return a loop as the output. This is not
surprising, even the pigeonhole principle has a short inductive proof, but is
hard for resolution [14]. Consider the example below.

######  Example 4.

Consider a Prolog program which specifies the set of all trees, with a unique
root and such that every child has a unique parent. Consider the following
query: is the tree connected? Existing prolog unables to handle such programs.
QBF-Prolog, proposed in this article just return a loop for this problem. For
the detailed encoding of the tree and query, refer Section 6.5.

  3. 3.

An interactive QBF-solver for the quantified Boolean Horn formulas (QBF-
Prolog, Section 4). There exists several QBF-solver in the literature (Section
2.2), then why QBF-Prolog?

First of all, QBF-Prolog, deals with the quantified Horn formulas. It is well
known that several problems of practical importance, such as program
verifications [2, 5, 30], can be encoded as quantified Horn formulas. It is
important to design an efficient QBF solver for the same. QBF-Prolog is such a
solver. It uses the structure of the quantified Boolean Horn formulas and
solves the satisfiability problem in linear time. (Of course, the QBF-Prolog
may return a loop as well, but it detects the same in linear time).

QBF-Prolog can also be used for the quantified renamable Horn formulas. We say
that a QBF $\mathcal{F}$ is a quantified renamable Horn formula, if
$\mathcal{F}$ can be transformed into a quantified Horn formula by negating
every instance of one or more of its variables. For example, the QBF $\exists
x_{1}\forall x_{2}\exists x_{3}.(x_{1}\vee x_{2}\vee x_{3})\wedge(\neg
x_{1}\vee x_{2}\vee\neg x_{3})$ is a quantified renamable Horn formula, since
by complementing $x_{1}$ and $x_{2}$ we get the following quantified Boolean
Horn formula: $\exists x_{1}\forall x_{2}\exists x_{3}.(\neg x_{1}\vee\neg
x_{2}\vee x_{3})\wedge(x_{1}\vee\neg x_{2}\vee\neg x_{3})$. This operation of
choosing a subset of variables and replacing each positive literal of such a
variable by the corresponding negative literal and vice versa, is called
renaming. It is easy to observe that renaming preserves satisfiability. That
is, a QBF $\mathcal{F}$ is satisfiable if and only if the QBF
$\mathcal{F}^{\prime}$ obtained via renaming is satisfiable.

Given a QBF formula $\mathcal{F}$ it is possible to determine in linear time
whether $\mathcal{F}$ is quantified renamable Horn formula [16]. The algorithm
also gives the set of variables which needs to be complemented in order to get
a quantified Horn formula. Thus, using the algorithm from [16], and via the
QBF-Prolog, one can solve the satisfiable problem for a quantified renamable
Horn formula efficiently. Note that, [16] solves the problem for the
propositional case, however, the same algorithm works for the quantified
formulas as well, we just need to ignore the quantifiers.

Another advantage of QBF-Prolog is it’s interactive nature: As it is based on
Prolog, it supports man-machine conversation. To the best of our knowledge,
all existing QBF solvers are imperative in nature. Also, QBF satisfiability
problem is well suited to be solve via backtracking and hence is very natural
to pick Prolog and extend it for the QBFs.

###  1.2 Organisation of the paper

The remainder of the paper is organized as follows. We review the basic
notations and preliminaries in Section 2. In Section 3, we extend the SLD-Res
proof systems for the quantified Boolean Horn formulas and proof the
completeness and soundness of the new proof systems for the same. We extend
Prolog for the quantified Boolean formulas, with the restrictions that the
query clause contains no new variables, in Section 4, and also propose an
efficient implementation model for the same. We extend Prolog for quantified
Boolean Horn formulas without any restriction and for first-order predicate
Horn formulas in Section 5. In Section 6, we present some applications of the
QBF-Prolog. Finally, we present conclusions in Section 7.

##  2 Notations and Preliminaries

Quantified Boolean formulas (QBFs) are extensions of propostional formulas, in
which each variable is quantified by universal or existential quantifiers. QBF
does not increase the expressive power of propositional logic, it simply
offers an exponentially more succinct encoding of problems. As a result,
problems from various important industrial fields, such as formal verification
and model checking can be encoded succintly as QBFs. This leads to the desire
of building efficient QBF-SAT solvers. Let us define now QBFs more formally.

Quantified Boolean Formulas (QBFs): It extend propositional logic with Boolean
quantifiers with the standard semantics that $\forall x.F$ is satisfied by the
same truth assignments as $F|_{x=0}\wedge F|_{x=1}$ and $\exists x.F$ as
$F|_{x=0}\vee F|_{x=1}$.

We say that a QBF is in _closed prenex form_ with a CNF (Conjunctive Normal
Form) matrix, if the QBF instance is of the form $\Pi.\phi$, where
$\Pi=\mathcal{Q}_{1}X_{1}\mathcal{Q}_{2}X_{2}\dots\mathcal{Q}_{n}X_{n}$ is
called the quantifier prefix, with $\mathcal{Q}_{i}\in\\{\exists,\forall\\}$,
and $\phi$ is a quantifier-free CNF formula in the variables
$X_{1}\cup\ldots\cup X_{n}$. We have $X_{i}\cap X_{j}=\emptyset$,
$\mathcal{Q}_{i}\neq\mathcal{Q}_{i+1}$, and
$\mathcal{Q}_{1},\mathcal{Q}_{n}=\exists$.

A literal is either a variable or its complement. For a clause $C$, $var(C)$
is a set containing all the variables of $C$. For a QBF $\mathcal{F}$,
$var(\mathcal{F})$ is a set containing all the variables of $\mathcal{F}$
(i.e., $var(\mathcal{F})=\cup_{C\in\mathcal{F}}\\{var(C)\\}$). A quantifier
$Q(\Pi,\ell)$ of a literal $\ell$ is $\mathcal{Q}_{i}$ if the variable
$var(\ell)$ of $\ell$ is in $X_{i}$. A literal $\ell$ is existential if
$Q(\Pi,\ell)=\exists$ and universal if $Q(\Pi,\ell)=\forall$. For literals
$\ell$ and $k$, with $Q(\Pi,\ell)=\mathcal{Q}_{i}$ and
$Q(\Pi,k)=\mathcal{Q}_{j}$, we say that the literal $\ell$ is on the left of
literal $k$ ($\ell\leq_{\Pi}k$) if and only if $i\leq j$. Within a clause, we
order literals according to their ordering in the quantifier prefix. We assume
that QBF is in this form, unless noted otherwise. The order $\leq_{\Pi}$ is
arbitrary extended to variables withing each block $X_{i}$. For a literal
$\ell$, $level(\Pi,\ell)=i$ if $var(\ell)\in X_{i}$.

A QBF ${\mathcal{Q}_{1}x_{1}\cdots\mathcal{Q}_{k}x_{k}}\,\text{.}\,{\phi}$ can
be seen as a game between two players: universal $(\forall)$ and existential
$(\exists)$. In the $i^{th}$ step of the game, the player ${\cal Q}_{i}$
assigns a value to the variable $x_{i}$. The existential player wins if $\phi$
evaluates to $1$ under the assignment constructed in the game. The universal
player wins if $\phi$ evaluates to $0$.

An assignement tree [17] $T$ of a QBF $\mathcal{F}$ is a complete binary tree
of depth $|var(\mathcal{F})|+1$. Internal nodes corresponds to the variables
of $\mathcal{F}$. The order of the variables in $T$ respect the orders in the
prefix in $\mathcal{F}$. Internal nodes which corresponds to an existential
variables act as an OR-nodes, whereas universal nodes corresponds to an AND-
nodes. Every internal nodes $x$ has two children, one for literal $x$ (true)
and one for literal $\neg x$ (false). An existential node is labelled with
$\top$ (true) if at least one of its children is labelled with $\top$ (true).
A universal node is labelled with $\top$ if both of its children are labelled
with $\top$. A path in $T$ is a sequence of literals. A path $\tau$ from root
to a leave in $T$ is a complete assignement and the leave is labelled with the
value of QBF under $\tau$. The QBF $\mathcal{F}$ is true if the root of $T$ is
labelled with $\top$, and $\mathcal{F}$ is false if the root is labelled with
$\perp$.

A subtree $T^{\prime}$ of the asignment tree $T$ is a pre-model [17] of the
QBF $\mathcal{F}$ if the root of $T$ is also the root of $T^{\prime}$, both
children of every universal node must be present in $T^{\prime}$, and exactly
one child of every existential node are in $T^{\prime}$. We say that a pre-
model $T^{\prime}$ of a QBF $\mathcal{F}$ is a model of $\mathcal{F}$, denoted
$T^{\prime}\models\mathcal{F}$ if every node in $T^{\prime}$ is labelled with
$\top$. Similarly, a false QBF has countermodels which can be defined dually.

A QBF $\mathcal{F}$ is satisfiable if it has at least one model. For QBFs
$\mathcal{F}$ and $\mathcal{H}$, we say that $\mathcal{H}$ is implied by
$\mathcal{F}$, denoted $\mathcal{F}\models\mathcal{H}$ if, for all $T$, if
$T\models\mathcal{F}$ then $T\models\mathcal{H}$.

We say that two QBFs $\mathcal{F}$ and $\mathcal{H}$ are (logically)
equivalent denoted $(\mathcal{F}\equiv\mathcal{H})$ iff
$\mathcal{F}\models\mathcal{H}$ and $\mathcal{H}\models\mathcal{F}$, and
satisifability equivalent, denoted $\mathcal{F}\equiv_{sat}\mathcal{H}$, iff
$\mathcal{F}$ is satisifable whenever $\mathcal{H}$ is satisfiable.

###  2.1 QBF proof complexity

Since past few decades, QBFs solving is an active area of research. As a
result, several proof systems for QBFs have been developed. For example,
Kleine Büning et al. in [21] introduced Q-resolution (Q-Res), which is an
extension of the propositional resolution proof system for QBFs. Before
defining Q-Res, let us quickly define the Resolution (Res) proof system.

Resolution: (Res) is well studied propositional proof system introduced by
Blake in [6] and proposed by Robinson in [32] as automated theorem proving.
The lines in the resolution proofs are clauses. Given a CNF formula $F$, Res
can infer new clauses according to the following inference (resolution) rule :

$\frac{C\vee x\hskip 14.22636ptD\vee\neg x}{C\vee D},$

where $C$ and $D$ are clauses and $x$ is a variable being resolved, called as
pivot variable. The clause $C\vee D$ is called the resolvent. Let $F$ be an
unsatisfiable CNF formula. A resolution proof (refutation) $\pi$ of $F$ is a
sequence of clauses $D_{1},\dots,D_{l}$ with $D_{l}=\Box$ and each clause in
the sequence is either from $F$ or is derived from previous clauses in the
sequence using the above resolution rule.

We can also view $\pi$ as a directed acyclic graph $G_{\pi}$, where the source
nodes are the clauses from $F$, internal nodes are the derived clauses and the
empty node is the unique sink. Edges in $G_{\pi}$ are from the hypotheses to
the conclusion for each resolution step. In $G_{\pi}$, we say that a clause
$C$ is descendant to a clause $D$ if there is a directed path from $C$ to $D$.

Q-resolution: Q-Res uses the resolution rule, but with a side condition that
the pivot variable must be existential, and the resolvent does not have
simultaneously a $z$ and $\neg z$. In addition, Q-Res has a universal
reduction rule ($\forall$-Red) which allows dropping a universal literal $u$
from a clause provided the clause has no existential literal $\ell$ with
$u\leq_{\Pi}\ell$. That is, there exists no existential literal to the right
of the reduced literal $u$. We say in this case, that $u$ is not blocked.

QU-resolution [12], removes the restriction from Q-Res that the resolved
variable must be existential variable and allows resolution on universal
variables as well. Thus QU-resolution (QU-Res) is classical resolution
augmented with a $\forall$-Red rule. Interested readers are referred to [35],
for more details on QBF proof complexity.

###  2.2 QBFs solvers

Since, the propositional satisfiablity (SAT) problem is NP-complete, and the
QBF-SAT problem is PSPACE-complete [1], only algorithms with exponential
worst-case time complexity are known for these problems. Despite of this,
several efficient SAT solvers, capable of solving the satisfiability instances
with thousands of variables and clauses, have been designed. For example, the
GRASP search algorithm for the satisfiability problem [36], implemented by
Marques-Silva and Sakallah. GRASP is based on conflict-driven clause learning
(CDCL) algorithms [34].

Motivated by the success of propositional SAT solvers, many QBF solvers have
also been developed. We would like to mention some important ones:

DepQBF: DepQBF, developed by Lonsing and Egly [26], is based on QCDCL [40],
which is an extension of CDCL for QBFs. DepQBF, implements a variant of QCDCL,
which is based on a generalization of Q-Res. This generalization is due to
some additional axioms. Q-Res proofs can be extracted from instances of the
QCDCL algorithm. This generalization, in DepQBF implementation, helps to
produce exponential shorter refutation, than the traditional QCDCL-based
solvers.

RAReQS: Recursive Abstraction Refinement QBF Solver [18], is a recursive
algorithm for QBF solving, based on the Counter-example Guided Abstraction
Refinement (CEGAR) technique [7]. Initially, CEGAR was used to solve QBFs with
two level of quantifiers [19]. RAReQS, extends the technique to QBFs with an
arbitrary number of quantifiers using recursion.

CEGAR technique was designed to tackle problems whose implicit representation
is infeasible to solve, and an abstract instance is tackled instead. Thus, in
CEGAR-based algorithm, we have a concrete (an original) representation, and an
abstract representation of a problem. Both the representations are connected
as follows: if the abstract problem has no solution, then concrete problem
also does not have a solution. If a solution to the abstract problem is not a
solution to the concrete problem, then a counterexample can be constructed for
this fact. And finally, if there are no counterexamples for a solution to the
abstract problem, then the solution, is also a solution to the concrete
problem.

Based on the above properties one can compute a solution to the original
problem as follows: compute a solution to the abstract problem, if no such
solution exists, return: no solution to the original problem. Otherwise, check
if it is also a solution to the original problem: if no counterexample exists,
return: the same solution is a solution to the original problem. Otherwise,
use the counterexample to refine the abstract representation and repeat. This
gives the name: CounterExample Guided Abstract Refinement technique.

GhostQ: GhostQ solver [23] is originally implemented to support the QBF
solving for instances which are not in prenex from. GhostQ is a DPLL-based QBF
solver which uses ghost variables. Ghost literal, first introduced in [13], is
a powerful propogation technique for QBFs. Interested readers are referred to
[23].

###  2.3 First-order predicate logic

First-order predicate logic extends the propositiona logic by adding both the
predicates and the quantification. A Predicate $P(x_{1},x_{2},\dots,x_{n})$ is
an $n$-ary function whose range is only $0$ (false) or $1$ (true). Unlike
propositiona logic, where variable can take only $0$-$1$ values, in predicate
logic variables can take any values from some universal set $U$. Predicates
with arity $0$ are just the propositional variables. Some examples of
predicates are as follows. Assume the set of all humans as the universal
domain set $U$ for the below examples.

######  Example 5.

“$x$ is a male $\equiv$ male($x$)”: here variable $x$ ranges over the
universal set $U$. The predicate male($x$) is true iff $x$ is male.

######  Example 6.

“$x$ is the mother of $y$ $\equiv$ mother($x$, $y$)”: again $x,y$ ranges over
the universal set $U$, and the predicate mother($x,y$) is true iff the
variables $x$ and $y$ are initialized with some values $a,b\in U$
respectively, such that $a$ is the mother of $b$.

Clearly, as compared to the propositional logic, in the first-order predicate
logic, it is possible to express knowledge much easier, for example the
statement “for every $x$, if $x$ is an indian then $x$ is a human” can be
expressed as:

$\forall x~{}~{}indian(x)\rightarrow human(x).$

As another example, consider the following statement: If $x$ is a female, and
parents of $x$ and $y$ are same, then $x$ is a sister of $y$. This statement
can be expressed as:

$\forall x,y,m,f~{}~{}Female(x)\wedge Parent(x,m,f)\wedge
Parent(y,m,f)\rightarrow Sister(x,y).$

Obseve that the above example is equivalent to the following:

$\forall
x,y,m,f~{}\Big{(}\neg\text{Female}(x)\vee\neg\text{Parent}(x,m,f)\vee\neg\text{Parent}(y,m,f)\vee\text{Sister}(x,y)\Big{)}.$

This rule has just one positive predicate, and hence is a Horn clause. A
first-order predicate Horn logic consists of Horn clauses only. However, each
literal on a clause can be replaced by an arbitrary predicates of any arity.
Also, the variables can be quantified arbitrary.

We skip the definition of first-order predicate logic more formally here.
Interested readers are referred to the book by Robert S. Wolf [38].

Substitution and Unification: Given a first-order predicate formula
$F(x_{1},\dots,x_{n})$, over distinct variables, $x_{1},\dots,x_{n},$ a
substitution is a process of binding each variable $x_{i}$ with a predicate
$P_{i}$ (denoted, $x_{i}/P_{i}$). The arity of $P_{i}$ is allowed to be zero.

Recall, in Res, the resolution rules are performed over clauses with
complementary literals $x$ and $\neg x$. Consider two literals $P(a)$ and
$\neg P(x)$ appearing in two distinct clauses in a first-order predicate
logic. The literals are almost complementary: the first contains a constant,
whereas the second contains a variables. The subsitution can be applied here
two make the literals complementary: substitute $x/a$ in the second. Thus, the
literal $P(a)$ and $\neg P(x)$ becomes complementary after the substitution.
One may now perform resolution step on the same. Thus substitution can be
applied to make two first-order predicate formulas syntactically equal.

The unification algorithm is a general method for comparing first-order
predicate formulas. The algorithms also computes the substitution which is
needed to make the formulas syntatically equal. Interested readers are
referred to [29].

###  2.4 Prolog

Prolog stands for PROgramming in LOGic. Prolog is a declarative programming
language. Unlike, the procedural programming languages, where we have to tell
the computer what to do when, and how to achieve a certain goal, in Prolog on
the other hand, we only need to tell what is true, and then quering it to draw
conclusions. To be precise, in Prolog the description of a problem and the
procedure for solving it are separated from each other. According to Robert
Kowalski, a Prolog algorithm can be expressed as:

$\text{algorithm = logic }+\text{ control}$

In the above equation, the logic part gives the description of the problem,
that is, what the algorithm should do, and the control part indicates how it
should be done. In particular, the program logic is expressed as facts and
rules, and a computation is initiated by running a query over these facts and
rules.

The facts and rules are represented as Horn formulas. Horn formulas are a
special case of CNF formulas, where each clause is allowed to have at most one
positive literals.

Once a query as a goal clause is provided, Prolog tries to find a resolution
refutation of the negated query. If the refutation is found, the query is said
to be sucessful. This part constitute the control part.

To be precise, the Prolog control part is based on SLD-resolution, which is an
important refinement of Linear Resolution [9]. A linear resolution derivation
of a clause $C$ from a CNF formula $F$ is a sequence of clauses
$C_{1},C_{2},\dots,C_{m}$, such that $C_{1}\in F$, $C_{m}=C$, and for every
$i<m$, $C_{i+1}$ is the resolvent of $C_{i}$ either with a clause $D\in F$ or
with a clause $C_{k}$ for $k<i$. In order to define the basic principle used
in processing a logic program in Prolog, we need to first define the SLD-
resolution (Definition 1).

###  2.5 Proof system for Prolog: SLD-Res

In order to cut down the search space for SAT solvers, several refinements of
resolution proof system have been introduced. One of the most important
refinement is the linear resolution. Linear resolution is known to be complete
and sound for unsatisfiable CNF formulas [20]. To even cut down the search
space, several refinements of linear resolution have been proposed, for
example, s-linear Res [28, 39], t-linear Res [24], SL-res [24], and SLD-Res
[25]. All the above mentioned refinements are known to be complete and sound
for unsatisfiable CNF formulas, except the SLD-Res. As Prolog is based on SLD-
Res we define it next.

####  2.5.1 SLD-Res

SLD-Res, a refinement of linear resolution, was introduced by Robert Kowalski
[25]. The name SLD-Resolution stands for SL resolution with definite clauses.
SLD-Res is complete and sound for propositional Horn formulas. Before
introducing SLD-Res, let us quickly re-visit propositional Horn formulas in
detail.

####  2.5.2 Propositional Horn Formulas

Horn formulas are a special case of CNF formulas, named after the logician
Alfred Horn. A clause $C$ is a Horn clause if and only if $C$ contains at most
$1$ positive literal. A Horn formula is a conjunction of Horn clauses. A
definite Horn clause is a clause with exactly one positive literal and zero or
more negative literals. A conjunction of definite Horn clauses is called a
definite Horn formula. We usually denote a definite Horn clause $(x\vee\neg
x_{1}\vee\dots\vee\neg x_{k})$ as $x\leftarrow x_{1},\dots,x_{k}$, which is
equivalent to the following:

$\text{IF }x_{1}\wedge x_{2}\wedge\dots\wedge x_{k}\text{ then }x$

Here, $x,x_{1},\dots,x_{k}$ are variables. The variable $x$ is called the head
of the clause, and $x_{1},\dots,x_{k}$ is called the body of the clause. We
denote the head of a Horn clause $C$ by $C^{+}$ (or $head(C)$) and the body by
$C^{-}$. A clause with only negative literals are referred as negative clause.
Clearly a negative clause is also a Horn clause. We usually refer a negative
Horn clause as a goal clause. We denote a goal clause $(\neg x_{1}\vee\neg
x_{2}\vee\dots\vee\neg x_{k})$ as $\leftarrow x_{1},x_{2},\dots,x_{k}$. The
empty clause $\Box$ is also considered as a goal clause. We quickly list some
important facts about Horn formulas.

######  Lemma 1.

[22] For any Horn formula (other than the empty clause), the following holds:

  1. 1.

A definite Horn formula is satisfiable.

  2. 2.

A Horn formula $F$ is satisfiable if $F$ contains no positive unit clause
(clauses with only one literal are called unit clauses).

###### Proof.

Every clause in a definite Horn formula has exactly one positive literal. Thus
the assignment which assigns each variable the value true, satisifies the
formula.

If the Horn formula has no positive unit clause, then each clause contains at
least one negative literals. Again the assignment which assigns each variable
the value false, satisfies the formula. ∎

Therefore, for a Horn formula to be unsatisfiable, it must contain at least
one negative clause. In fact the following also holds:

######  Lemma 2.

[22] Let $F=F_{1}\cup F_{2}$ be an unsatisfiable Horn formula, where $F_{1}$
contains only definite Horn clauses and $F_{2}$ contains only negative
clauses. Then

$F\text{ is unsatisfiable }\iff\exists C\in F_{2}:F_{1}\cup\\{C\\}\text{ is
unsatisfiable}$

###### Proof.

Suppose not. That is, let $F$ be unsatisfiable and for all $C\in F_{2}$,
$F_{1}\cup\\{C\\}$ is satisfiable. Assuming this we show that $F$ is
satisfiable as well, which is clearly a contradiction.

Let variables $x_{1},x_{2},\dots x_{m}$ are consequences of $F_{1}$, that is
$F_{1}\implies x_{i}$ for $i\in[m]$. Clearly,
$var(C)\nsubseteq\\{x_{1},\dots,x_{m}\\}$ for every $C\in F_{2}$, otherwise
$F$ would have been satisfiable: $F_{1}$ is satisfiable from Lemma 1, and if
$var(C)\in\\{x_{1}\dots,x_{m}\\}$ for all $C$ in $F_{2}$, then $F_{2}$ is also
satisfiable.

Let $\mathcal{I}$ be the following assignment: $\mathcal{I}(x_{j})=1$ for
$j\in[m]$, and $\mathcal{I}(y)=0$ for all other variables $y$. Clearly,
$\mathcal{I}(C)=1$ for all $C\in F_{2}$: as $C$ is negative clause and at
least one variable $y$ must belong to $C$. Therefore we have
$\mathcal{I}(F_{2})=1$.

On the other hand, observe that $\mathcal{I}(F_{1})=1$ as well: since
$\mathcal{I}(x_{j})=1$ and $F_{1}\implies x_{j}$, for $j\in[m]$, therefore
$\mathcal{I}(F_{1})$ must be $1$.

∎

Since we are discussing Horn formulas, we quickly introduce an important
refinement of resolution proof system which is incomplete for CNF formulas but
complete for Horn formulas: unit resolution (unit-Res). A resolution proof
system is called a unit resolution proof systems iff for every resolution step
one of its parent clause is a unit-clause. We have the following:

######  Lemma 3.

[22] Let $F$ be a Horn formula, then

$F\text{ is unsatisfiable }\iff
F{\scriptsize\mathrel{\leavevmode\hbox{\set@color\raisebox{2.41112pt}{$\rule[-4.52083pt]{0.33452pt}{9.04166pt}\rule[-0.16725pt]{20.86191pt}{0.33452pt}\raisebox{-4.7211pt}{\makebox[20.86191pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{unit-
Res}}$}}}\raisebox{1.37277pt}{\makebox[20.86191pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}}~{}\Box$

###### Proof.

Since Res simulates unit-Res and Res is sound, we only need to prove that
unit-Res is complete. We prove this by induction on the number of variables in
$F$. For $n=1$ clearly $F\equiv x\wedge\neg x$, and the Lemma follows.

Assume that $n>1$. As $F$ is unsatisfiable Horn formula, it must have a
positive unit clause $x$. Resolve $x$ with all the clauses having $\neg x$.
Clearly the resulting formula $F^{\prime}$ is indeed Horn. Also observe that
$F^{\prime}$ is unsatisfiable (the proof is exactly as in the completeness
proof of resolution). Clearly, $F^{\prime}$ is an unsatisfiable Horn formula
over $n-1$ variables. The refutation follows from the induction hypothesis. ∎

######  Definition 1 (SLD-resolution).

[11] Let $F$ be a Horn formula. Let $D,G\subseteq F$ be disjoint subsets of
clauses from $F$ such that $D$ is the set of all definite Horn clauses, and
$G=\\{G_{1},\dots,G_{q}\\}$ be the set of all goal (negative) clauses. Let $C$
be a goal clause. An SLD-Res derivation of $C$ from $F$ is a sequence of
negative clauses $\pi=N_{0},N_{1},\dots,N_{m}$ such that:

  1. 1.

$N_{0}=G_{j}$, where $G_{j}$ is some goal from $F$.

  2. 2.

Each $N_{i}$ is a resolvent of $N_{i-1}$ and a definite input clause $C_{i}\in
D$, resolved over the head $x$ of $C_{i}$. The variable $x$ (i.e., the literal
$\neg x$) of $N_{i-1}$ is the selected variable in the body of $N_{i-1}$. We
call, the clause $N_{i-1}$ a centre clause, and the clause $C_{i}$, a side
clause.

  3. 3.

$N_{m}=C$.

$N_{0}$ is the top clause, and the $C_{i}$ are the input clauses of this SLD-
Res derivation. If an SLD-Res derivation of $C$ from $F$ exists, we write
$F~{}{\scriptsize\mathrel{\leavevmode\hbox{\set@color\raisebox{2.41112pt}{$\rule[-4.52083pt]{0.33452pt}{9.04166pt}\rule[-0.16725pt]{21.67857pt}{0.33452pt}\raisebox{-4.7211pt}{\makebox[21.67857pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{SLD-
Res}}$}}}\raisebox{1.37277pt}{\makebox[21.67857pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}}~{}C$.
If $N_{m}=\Box$, we call $\pi$ an SLD-Res refutation of the Horn formula $F$.

Observe that, an SLD-Res refutation is not just a linear resolution but also
an input and a negative resolution (every resolution step has at least one
negative clause as parent). In fact, all the clauses $N_{i}$ is the SLD-Res
derivation are goal clauses. This is because the top clause $N_{0}$ is a goal
clause. If we pick $N_{0}$ to be a definite clause from $F$, then all clauses
in the SLD-Res derivation will be definite clauses. Note that the input
clauses of any SLD-Res derivations are always the definite clauses.

We know that SLD-Res proof system is sound and complete for Horn formulas.

######  Theorem 2.1.

[10] SLD-Res proof system is sound and complete for Horn formulas.

Prolog treats clauses as multisets of literals (it retains all the repeated
literals in a resolvent). For Prolog not only the order of literals within a
clause matters, but also the order of clauses within a Horn formula matters.
The Horn formulas in which both the clauses and the literals within the
clauses are given a fixed ordering are called a Prolog program. Given a Prolog
program $\pi$ and a query $\gamma$ one can easily define the Prolog mechanism
via a recursive algorithm. Interested readers are referred to [22].

##  3 SLD-resolution for QBFs (SLD-Q-Res)

If we allow universal variables, along with existential variables, to be used
as a pivot variable, for the resolution step (as in QU-Res), then SLD-Res can
be easily extended for QBFs: just add the $\forall$-Red rules as in [3]. This
proof system is interesting, and we plan to study this in future. However, as
per our knowledge, there exists no QBF solver based on QU-Res. Therefore,
extending SLD-Res to QBFs with a restriction that only existential variables
are allowed, as a pivot variable in the resolution step (as in Q-resolution),
is more important. We work on this direction now. As, SLD-Res proof system is
complete only for Horn formulas, let us define quantified Horn formulas first:

######  Definition 2.

[22] A quantified Boolean formula
$\mathcal{F}\equiv\mathcal{Q}_{1}X_{1}\mathcal{Q}_{2}X_{2}\dots\mathcal{Q}_{n}X_{n}(C_{1}\wedge\dots\wedge
C_{m})$ is a quantified Horn formula iff each clause $C_{i}$ in the matrix has
at most one positive literals (existential or universal). We use notations as
in the propositional case.

It is well known that the satisfiability problem for the quantified Horn
formula can be solvable in polynomial time [22], however the equivalence
problem for them are coNP complete [22].

It is clear that every clause in any quantified Horn formula $\mathcal{F}$
belongs to one of the following set:

  * •

$F_{\exists}$: set of all clauses $C$ with exactly one positive existential
literal $\ell$.

  * •

$F_{\forall}$: set of all clauses with exactly one positive universal literal.

  * •

$F_{\text{goal}}$: set of all goal clauses with only negative (existential or
universal) literals.

######  Observation 1.

[22] A quantified Horn formula $\mathcal{F}$ is false if and only if there
exists a clause $C^{\prime}\in F_{\forall}\cup F_{\text{goal}}$ such that
$\mathcal{Q}_{1}X_{1}\mathcal{Q}_{2}X_{2}\dots\mathcal{Q}_{n}X_{n}.(F_{\exists}\wedge
C^{\prime})$ is false.

######  Observation 2.

Let $\mathcal{F}$ be a false quantified Horn formula. Let us assume, that in
Observation 1, we have $C^{\prime}\in F_{\text{goal}}$. That is, assume
$C^{\prime}\in F_{\text{goal}}$, and
$\mathcal{Q}_{1}X_{1}\mathcal{Q}_{2}X_{2}\dots\mathcal{Q}_{n}X_{n}.(F_{\exists}\wedge
C^{\prime})$ is false. Then for every negated existential literal $q$ in
$C^{\prime}$ (i.e, $\neg q\in C^{\prime}$), we have a clause $C\in
F_{\exists}$, with the variable $q$ (i.e., literal $q$) as its head.

###### Proof.

We know that the initial QBF $\mathcal{F}$ is false. Therefore, there does not
exists any winning strategy for the existential player.

Consider the following strategy of the existential player: assign $1$ to all
the heads of the clauses from $F_{\exists}$. Let us call this assignment
$\alpha$. For sure, $\alpha$ satisfies all the clauses of $F_{\exists}$.
However, as the original formula is false, this assignment does not satisfy
the clause $C^{\prime}$. In fact $C^{\prime}|{\alpha}$ is either $0$, or is
left with a bunch of negated universal literals. Otherwise, $\alpha$ can be
extended as a winning strategy for the existential player.

This tells us that, every negated existential literal $(\neg\ell)$ of
$C^{\prime}$ has a corresponding head $\ell$ in some clause of $F_{\exists}$.
If not, one can extend $\alpha$ to winning startegy for the existential
player. ∎

######  Observation 3.

Let us assume, that in Observation 1, we have $C^{\prime}\in F_{\forall}$.
Then, for every negated existential literal $q$ in $C^{\prime}$ (i.e, $\neg
q\in C^{\prime}$), we have a clause $C\in F_{\exists}$, with the variable $q$
(i.e., literal $q$) as its head.

###### Proof.

The proof is exactly as in Observation 2. ∎

Let us define SLD-Res for QBFs (SLD-Q-Res). An SLD-Q-Res derivation of a
clause $C$ from a quantified Horn formula $\mathcal{F}$ is exactly as in the
propositional case, except that a clause $N_{i}$ in the sequence may also be
derived via a $\forall$-Red rule from $N_{i-1}$. That is, by deleting a
universal variable of $N_{i-1}$ which has not been blocked in $N_{i-1}$. To be
precise,

######  Definition 3 (SLD-Q-Res).

Let $\mathcal{F}$ be a false quantified Horn formula. Let $C$ be a goal
clause. An SLD-Q-Res derivation of $C$ from $\mathcal{F}$ is a sequence of
negative clauses $\pi=N_{0},N_{1},\dots,N_{m}$ such that:

  1. 1.

$N_{0}\in\mathcal{F}$, is an initial goal clause.

  2. 2.

Each $N_{i}$ is a resolvent of $N_{i-1}$ and a definite input clause $C_{i}$,
resolved over the head $x$ of $C_{i}$. The variable $x$ (i.e., the literal
$\neg x$) of $N_{i-1}$ is the selected variable in the body of $N_{i-1}$.
(Observe that $x$ is an existential literal by definition). Resolution is only
allowed on existential variables.

  3. 3.

Each $N_{i}$ is derived from $N_{i-1}$ via a $\forall$-Red step. That is, by
deleting a universal variable $u$ from $N_{i-1}$ such that $u$ is not blocked
in $N_{i-1}$.

  4. 4.

$N_{m}=C$.

If $N_{m}=\Box$ then $\pi$ is an SLD-Q-Res refutation of the quantified Horn
formula $\mathcal{F}$. We denote by
$\mathcal{F}~{}{\scriptsize\mathrel{\leavevmode\hbox{\set@color\raisebox{2.41112pt}{$\rule[-4.52083pt]{0.33452pt}{9.04166pt}\rule[-0.16725pt]{27.12302pt}{0.33452pt}\raisebox{-4.7211pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{SLD-
Q-
Res}}$}}}\raisebox{1.37277pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}}~{}\Box$
the fact that $\mathcal{F}$ has an SLD-Q-Res refutation.

######  Theorem 3.1.

SLD-Q-Res is sound and complete for false quantified Horn formulas.

###### Proof.

As Q-Res is sound and can simulate SLD-Q-Res, we only need to prove
completeness. Let $\mathcal{F}$ is a false quantified Horn formula. Then, by
Observation 1, $\exists C^{\prime}\in F_{\text{goal}}\cup F_{\forall}$ such
that
$\mathcal{Q}_{1}X_{1}\mathcal{Q}_{2}X_{2}\dots\mathcal{Q}_{n}X_{n}(F_{\exists}\wedge
C^{\prime})$ is false. So we have two cases:
Case 1: When $C^{\prime}\in F_{\text{goal}}$: If $C^{\prime}$ has only negated
universal literals, just apply the $\forall$-Red rules and derive the empty
clause. Clearly, this is an SLD-Q-Res refutation. Otherwise, let $C^{\prime}$
has the following existential negated literals (with some negated universal
literals as well): $\neg x_{1},\neg x_{2},\dots,\neg x_{k}$. Let $C_{i}\in
F_{\exists}$ be the clause with head $x_{i}$. By Observation 2, we must have a
$C_{i}\in F_{\exists}$ for every $x_{i}$.

We start constructing an SLD-Q-Res refutation with the top clause $C^{\prime}$
as follow: resolve $C^{\prime}$ and the clause $C_{1}$ with pivot $x_{1}$. Let
the resolvent is $C^{\prime}_{1}$. Resolve $C^{\prime}_{1}$ with the clause
$C_{2}$ with pivot $x_{2}$. and so on. Call the resolvent after $k$ step as
$C^{\prime}_{k}$.

We claim that $C^{\prime}_{k}$ is either an empty clause, or consists of only
negated universal literal. If this claim is true, we are done. We have an SLD-
Q-Res refutation of $\mathcal{F}$.

Suppose not. Then, $C^{\prime}_{k}$ has an existential variable say $q$.
Clearly, $q$ is a negated literal. Because, each $C^{\prime}_{i}$ is in fact a
negated clause only. Observe that $\neg q\notin C^{\prime}$, otherwise, it
would have been resolved via an input clause containing $q$ as head. So, it
must be the case, that $\neg q$ belongs to some $C_{i-1}\in F_{\exists}$ and
introduced in the resolvent $C^{\prime}_{i}$.

Assuming this, we now give a winning strategy for the existential player for
the QBF $\mathcal{F}$: assign $1$ to all the heads of the clauses from
$F_{\exists}$, except the clause $C_{i-1}$. In $C_{i-1}$ assign $0$ to the
head $x_{i-1}$ and a $0$ to the negated literal $q$. Clearly, the assignement
satisfies all clauses from $F_{\exists}$. Also, it satisfies the clause
$C^{\prime}$: as $\neg x_{i-1}\in C^{\prime}$ and $x_{i-1}=0$. Note that $\neg
x_{i-1}$ surely is present in $C^{\prime}$, that is why we resolved
$C^{\prime}_{i-1}$ with $C_{i-1}$. This proves our claim.

Note: as $\mathcal{F}$ is a QBF Horn formula, we do not have any universal
variables $u$ and $\neg u$ together in any resolvent $C^{\prime}_{i}$.
Case 2: When $C^{\prime}\in F_{\forall}$: This case is similar to the Case 1.
Again, begin with clause $C^{\prime}$ and start resolving the negated
existential literals of $C^{\prime}$ with the corresponding definite clauses.
This is possible by Observation 2. At the end, we are left with the empty
clause or with only negated universal literals. ∎

##  4 Extending Prolog to QBFs (QBF-Prolog)

In this Section, we develop theory for the QBF-Prolog. We follow the ideas
from [22, 27]. Given facts and rules as a quantified Horn formulas
$\mathcal{F}=\Pi.~{}\phi$, and a query Horn clause $C\equiv x\leftarrow
x_{1},x_{2},\dots,x_{n}$. We need to answer whether

$\Pi.\phi\models\Pi.(\phi\wedge\\{C\\})?$

We note that $C$ may have new variables as well, and there are no restrictions
on how these variables are quantified and where they are put within the
prefix.

Let us first develop theory for the case when the query clause $C$ has no new
variables. We show that the other case is trivial. That is, we show that the
case in which the query clause contains new literals have a straightforward
answer: if the new literal in the query clause is existential, then the answer
is yes. If the new literal $u$ is universal, then one may drop $u$ from the
query clause without effecting the answer.

###  4.1 Theory for QBF-Prolog when the query Horn clause has no new variables

Let $\mathcal{F}=\Pi.\phi$ be a quantified Boolean Horn formula. Let $C$ be a
Horn clause, such that $var(C)\subseteq var(\mathcal{F})$. We need to answer
whether

$\Pi.\phi\models\Pi.(\phi\wedge\\{C\\})?$

We use the ideas from [27].

Abstractions: Given a QBF $\mathcal{F}=\Pi.\phi$ with prefix
$\Pi=\mathcal{Q}_{1}X_{1}\dots\mathcal{Q}_{i}X_{i}\mathcal{Q}_{i+1}X_{i+1}\dots\mathcal{Q}_{n}X_{n}$,
and an $i$ with $0\leq i\leq n$. An abstraction QBF is defined as
$\mathcal{F}_{i}=\Pi_{i}.\phi$ where

$\Pi_{i}=\exists(X_{1}\cup\dots\cup
X_{i})\mathcal{Q}_{i+1}X_{i+1}\dots\mathcal{Q}_{n}X_{n}$

Note that $\mathcal{F}_{0}\equiv\mathcal{F}$ and $\mathcal{F}_{n}$ is just the
CNF formula $\phi$ over all existential variables $X_{1}\cup\dots\cup X_{n}$.
We state the following Lemma from [27] regarding abstractions without proof:

######  Lemma 4 ( [27]).

Let $\mathcal{F}=\Pi.\phi$ and $\mathcal{F}^{\prime}=\Pi.\phi^{\prime}$ be two
QBFs with same prefix. Then for all $i$, if
$\Pi_{i}.\phi\equiv\Pi_{i}.\phi^{\prime}$ then
$\mathcal{F}\equiv\mathcal{F}^{\prime}$.

Let $i=max_{\ell\in C}\\{level(\Pi,\ell)\\}$, that is, $i$ be the maximum
level of literals in the query Horn clause $C$. For a clause $C$ (say,
$(\ell_{1}\vee\dots\vee\ell_{k})$), we define $\overline{C}$ as the complement
of $C$, that is, conjunction of all the negated literals of $C$ (that is,
$(\neg\ell_{1}\wedge\dots\wedge\neg\ell_{k})$). We have the following:

######  Lemma 5 ([27]).

Let $\mathcal{F}=\Pi.\phi$ be a Horn QBF, $C$ be a Horn clause with
$var(C)\subseteq var(\mathcal{F})$ and $i=max_{\ell\in
C}\\{level(\Pi,\ell)\\}$. If
$\Pi_{i}.(\phi\wedge\overline{C})~{}{\scriptsize\mathrel{\leavevmode\hbox{\set@color\raisebox{2.41112pt}{$\rule[-4.52083pt]{0.33452pt}{9.04166pt}\rule[-0.16725pt]{27.12302pt}{0.33452pt}\raisebox{-4.7211pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{SLD-
Q-
Res}}$}}}\raisebox{1.37277pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}}~{}\Box$
then $\Pi.\phi\equiv\Pi.(\phi\wedge C)$

Note that in [27], they proved the result via quantified unit propagation [27,
Definition 9]. However, here we show that the result is valid for SLD-Q-Res as
well.

Lemma 5 follows from Lemma 4, and Lemma 7 below.

######  Lemma 6 ([27]).

Let $\Pi.\phi$ be a Horn QBF, with
$\Pi=\mathcal{Q}_{1}X_{1}\dots\mathcal{Q}_{n}X_{n}$ and $C$ be a Horn query
clause with $var(C)\subseteq X_{1}$, and $i=max_{\ell\in
C}\\{level(\Pi,\ell)\\}=1$. If
$\Pi_{1}.(\phi\wedge\overline{C})~{}{\scriptsize\mathrel{\leavevmode\hbox{\set@color\raisebox{2.41112pt}{$\rule[-4.52083pt]{0.33452pt}{9.04166pt}\rule[-0.16725pt]{27.12302pt}{0.33452pt}\raisebox{-4.7211pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{SLD-
Q-
Res}}$}}}\raisebox{1.37277pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}}~{}\Box$
then $\Pi_{1}.\phi\equiv\Pi_{1}.(\phi\wedge C)$.

As $\Pi_{1}.\phi$ is equal to $\Pi.\phi$. We have that if
$\Pi.(\phi\wedge\overline{C})~{}{\scriptsize\mathrel{\leavevmode\hbox{\set@color\raisebox{2.41112pt}{$\rule[-4.52083pt]{0.33452pt}{9.04166pt}\rule[-0.16725pt]{27.12302pt}{0.33452pt}\raisebox{-4.7211pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{SLD-
Q-
Res}}$}}}\raisebox{1.37277pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}}~{}\Box$
then $\Pi.\phi\equiv\Pi.(\phi\wedge C)$.

###### Proof.

Suppose not, and there exists a $T$ (assignment tree) with $T\models\Pi.\phi$
but $T\not\models\Pi.(\phi\wedge C)$. It follows that there exists a path
$\tau$ in $T$ with $\tau(C)=\perp$. As
$\Pi_{1}.(\phi\wedge\overline{C})~{}{\scriptsize\mathrel{\leavevmode\hbox{\set@color\raisebox{2.41112pt}{$\rule[-4.52083pt]{0.33452pt}{9.04166pt}\rule[-0.16725pt]{27.12302pt}{0.33452pt}\raisebox{-4.7211pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{SLD-
Q-
Res}}$}}}\raisebox{1.37277pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}}~{}\Box$,
the Horn QBF $\Pi.(\phi\wedge\overline{C})$ is unsatisfiable, and so
$T\not\models\Pi.(\phi\wedge\overline{C})$. Since $\tau(C)=\perp$, we have
$\tau(\overline{C})=\top$ and hence $T\models\Pi.(\phi\wedge\overline{C})$, a
contradiction. ∎

######  Lemma 7 ([27]).

Let $\Pi.\phi$ be a Horn QBF, $C$ be a Horn query clause and $i=max_{\ell\in
C}\\{level(\Pi,\ell)\\}$. If
$\Pi_{i}.(\phi\wedge\overline{C})~{}{\scriptsize\mathrel{\leavevmode\hbox{\set@color\raisebox{2.41112pt}{$\rule[-4.52083pt]{0.33452pt}{9.04166pt}\rule[-0.16725pt]{27.12302pt}{0.33452pt}\raisebox{-4.7211pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{SLD-
Q-
Res}}$}}}\raisebox{1.37277pt}{\makebox[27.12302pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}}~{}\Box$
then $\Pi_{i}.\phi\equiv\Pi_{i}.(\phi\wedge C)$.

###### Proof.

Since all variables from $C$ are existentially quantified in the abstraction
$\Pi_{i}.(\phi\wedge\overline{C})$, they all belongs to the first quantifier
block and the Lemma follows from Lemma 6. ∎

Using the ideas from [22] and Lemma 5, we next develop an efficient
implementation model. We start by presenting an exponential time algorithm for
the same.

###  4.2 Exponential time algorithm for QBF-Prolog when the query clause has
no new variables

In this Section we develop an efficient implementation for the QBF-Prolog when
the query clause has no new variables. In particular, we need to develop an
efficient implementation details for the Lemma 5. However, Prolog does not
work with clauses, but with multi-clauses as a lists. Therefore, we need to do
more.

As in the propositional case, QBF-Prolog treats clauses as multisets, let us
call this proof system as $\text{SLD-Q}_{\text{multi}}$-resolution. That is,
$\text{SLD-Q}_{\text{multi}}$-resolution proof system is just an SLD-Q-Res
proof system which retains every multiple copies of any literals within a
resolvent clause. For example: ($\leftarrow x,y),(y\leftarrow
x,z)~{}\,\scalebox{0.8}[0.8]{$\mathrel{\leavevmode\hbox{\set@color\raisebox{3.44444pt}{$\rule[-6.45831pt]{0.47787pt}{12.91663pt}\rule[-0.23894pt]{47.96942pt}{0.47787pt}\raisebox{-6.74445pt}{\makebox[47.96942pt]{\leavevmode\hbox{\set@color$\scriptstyle{\textsf{SLD-Q}_{\textsf{multi}}\textsf{-Res}}$}}}\raisebox{1.96112pt}{\makebox[47.96942pt]{\leavevmode\hbox{\set@color$\scriptstyle{}$}}}$}}}$}\,~{}\leftarrow
x,x,z$, and not $\leftarrow x,z$. Also, QBF-Prolog treats clauses as list of
literals. Therefore, the order of literals in any clause matters for QBF-
Prolog. To make it clear, let us define the proof system precisely for QBF-
Prolog.

######  Definition 4 ($\text{SLD-Q}_{\text{Prolog}}$-resolution).

[22, Chapter 5] An $\text{SLD-Q}_{\text{Prolog}}$-resolution derivation of a
quantified Horn formula is an $\text{SLD}_{\text{multi}}$-resolution
derivation in which clauses are regarded and processed as lists. In every
resolution step, the pivot variable $x$ which is resolved upon must occur as a
negative literal at the start of the list for the centre clause ($\neg x,\neg
y_{1},\neg y_{2},\dots\neg y_{r}$) and as a positive literal at the start of
the list for the side clause ($x,\neg s_{1},\neg s_{2},\dots,\neg s_{p}$). The
resolvent list is formed by concatenating the remainder of the centre clause
to the remainder of the side clause ($\neg s_{1},s_{2},\dots,\neg s_{p},\neg
y_{1},\neg y_{2},\dots,\neg y_{r}$). There are no additional constraints for
the $\forall$-Red rules.

In QBF-Prolog, not only the order of literals within a clause matters, but
also the order of clauses within a quantified Horn formula matters. A QBF-
Prolog program $P$ is a quantified Horn formula in which both the clauses and
the literals within the clauses are given a fixed ordering. Positive literals
always appear in the front of the lists for any definite clause.

Now, let us restate the problems mentioned at the begining of Section 4.1,
with the above discussed modifications.

Instead of a quantified definite Horn formula $\mathcal{F}=\Pi.\phi$, we have
a QBF-Prolog program $P=\Pi.\phi$ in which both the clauses and the literals
within a clause have fixed ordering. In addition, clauses in $\phi$ are given
as a list, with the positive literal in the front. We also have given the
query definite Horn clause $C=(x\vee\neg x_{1}\vee\neg x_{2}\vee\dots\vee\neg
x_{n})$ as a list of literals, with $var(C)\subseteq var(P)$. We need to
answer whether $P=\Pi.\phi\models\Pi.(\phi\wedge C)$?

Let $i=max_{\ell\in C}\\{level(\Pi,\ell)\\}$. Lemma 5 says that our Prolog
Algorithm should return a yes, for the above problem, if we can search an SLD-
Q-Res refutation of the following QBF-Prolog program:

$\displaystyle P^{\prime}=\Pi_{i}.(\neg x\wedge x_{1}\wedge x_{2}\dots\wedge
x_{n}\wedge\phi)$ (1)

Note that all the literals of $C$ becomes existential literals in the above
QBF-Prolog program. To be precise, we need to search an
$\text{SLD-Q}_{\text{Prolog}}$-resolution refutation. We first present an
exponential time recursive algorithm (Algorithm 1) to search a required
$\text{SLD-Q}_{\text{Prolog}}$-resolution refutation. The Algorithm search a
refutation with $\neg x$ as the top clause. That is, it start searching the
refutation with negation of the head of the query clause $C$. We call the
Algorithm 1 with the following input parameters: the QBF-Prolog program
$P^{\prime}$, and $\neg x$ ($\neg x$ will copy in the list $\gamma$).

_QBF-Prolog-Recursive-Algo(_quantified cnf-formula * $P$, list of quantified
cnf-variables * $\gamma$_)_

Input: QBF-Prolog program $P$ as a list of definite quantified Horn clauses,
and a goal list $\gamma$ as a list of quantified (negated) literals. For our
problem, $\gamma$ is the negation of the head of the query definite clause $C$
and $P$ is equalt to $P^{\prime}$ (Refer Equation 1).

Output: true; if the literals of the goal list are derivable from $P$ using
the prolog procedure, false (or possibly a loop); otherwise

if  _is-empty($\gamma$)_ then

return true

else

foreach  _clause $C\in P$_ do

if  _first-pos-lit($C$)==first($\gamma$)_ then

/* first-pos-lit($C$) returns the only positive literal of $C$, similarly,
first($\gamma$) returns the first existential literal of $\gamma$. If they are
same, call recursively the main program with $P$ as the first argument and the
goal list $\gamma^{\prime}$ as the second argument. $\gamma^{\prime}$ is
obtained as follows: Let rest($C$) outputs exactly the same list except the
first positive existential literal. Similarly, we have rest($\gamma$) returns
the same list except the first existential literal of $\gamma$. And
$\gamma^{\prime}=$ append(rest($C$), rest($\gamma$)), where append
concatenates the rest of $\gamma$ list to the rest of $C$ and then removes all
the universe literals which are not blocked in the concatenated sequence. */

if  _QBF-Prolog-Recursive-Algo $(P$, $\gamma^{\prime})$_ then

/* When the recursive call return sucess, we return success */

return true

end foreach

/* For $\gamma$, we considered each clause from $P$ in sequence, but unable to
proccess $\gamma$ completely, so return a failure */

return false

end if

End Function

Algorithm 1 Recursive algorithm for Prolog search mechanism for QBFs inspired
from [22].

QBF-Prolog-Recursive-Algo, uses $\text{SLD-Q}_{\text{Prolog}}$-resolution with
a combination of depth first search from left to right with backtracking.
Observe that Algorithm 1, may enters an infinite loop, even for the
propositional Prolog program.

Infact, due to the deterministic approach, the completeness of the
$\text{SLD-Q}_{\text{Prolog}}$-resolution has lost.

The above QBF-Prolog mechanism can be well explained with the concept of a
refutation tree [22]. Let $P$ be a QBF-Prolog program and $\gamma$ be the qoal
query. The refutation tree $T_{P}(\gamma)$ is a tree such that its root is
labelled with the query clause $\gamma$. Every node labelled with a goal
clause $\leftarrow x_{1},x_{2},\dots,x_{n}$ has a successor corresponding to
every definite Horn clause $x_{1}\leftarrow y_{1},\dots,y_{k}\in P$. The
successors are labelled with the $\text{SLD-Q}_{\text{Prolog}}$-resolution
resolvent $\leftarrow y_{1}\dots y_{k},x_{2}\dots x_{n}$ in this order.

For example, Figure 1 shows a refutation tree for the QBF-Prolog program

$P=\exists a,b,c,d,e\forall f\exists g.(a\leftarrow e,c,g)\wedge(a\leftarrow
d,b)\wedge(d\leftarrow b,f)\wedge(e\leftarrow f)\wedge(b)\wedge(g)$

and a query clause $\leftarrow a$.

$\hskip 2.84526pt\Box\hskip 2.84526pt$$\leftarrow f$$\leftarrow
f,b$$\leftarrow b,f,b$$\leftarrow d,b$$\leftarrow a$$\leftarrow
e,c,g$$\leftarrow f,c,g$$\leftarrow f,c$$\forall$-Red steps Figure 1:
Refutation tree for QBF-Prolog program $P$ and query $\leftarrow a$

While searching for a refutation, given a goal query $\gamma$ and $P$, three
outcomes are possible:

  * •

Empty clause $\Box$ is found. We say that the algorithm found the refutation.
The result is a yes.

  * •

The entire tree is searched without finding a node with $\Box$. The result is
a no, which means that the derivation of the empty clause is not possible.

  * •

During the search algorithm follow an infinite branch in the refutation tree.
The result is a loop.

For a QBF-Prolog program $P$ and a Horn query clause $C$, let us define the
following function:

$\text{output}(P,C)=\left\\{\begin{array}[]{l l}\text{yes}&\quad\text{if the
algorithm stops with a success}\\\ \text{no}&\quad\text{if the algorithm stops
with a failure}\\\ \text{loop}&\quad\text{if the algorithm enters a
loop}\end{array}\right.$

We next give a linear time algorithm for computing the function
$\text{output}(P,C)$.

###  4.3 Linear time algorithm for computing the output function

Given a QBF-Prolog program $P$ and a query Horn clause $C$, we describe an
algorithm which computes the $output(P,C)$ function in linear time, in the
length of the inputs. The challenge is to detect whether the algorithm enters
into loop in linear time.

As in the propositional case, we develop QBF-Prolog which is not only
interested in finding a refutation, but all possible refutations. Following
the ideas from [22], our proposed algorithm maintains five distinct states for
each existential variable of the QBF Prolog program. During the course of
processing, each existential variable $x$ is in one of the following states:

  * •

$state(x)=new$: the goal $\leftarrow x$ (ie., $\neg x$) has not yet processed.

  * •

$state(x)=yes$: the goal $\leftarrow x$ can be refuted in finite number of
ways and the refutation tree $T_{P}(\leftarrow x)$ does not contain an
infinite branch.

  * •

$state(x)=no$: refutation of the goal $\leftarrow x$ is not possible.

  * •

$state(x)=loop$: algorithm follows an infinite branch in the refutation tree
$T_{P}(\leftarrow x)$ while searching for the refuation. That is, algorithm
goes into a loop.

  * •

$state(x)=inf$: there exists infinitely many ways to refute the goal
$\leftarrow x$. Or, after finitely many refutations, the algorithm goes into a
loop (follows an infinite branch in the refutation tree).

Any universal variable $u$ of the QBF-Prolog program can be in any one of the
following two states. These state depends on the clause in which variable $u$
belongs to.

  * •

$blocked(u)=yes$: let $C$ be a clause and $u\in C$, and one cannot apply the
$\forall$-red step to $u$ in the clause $C$. To be precise, there exists an
existential literal $\ell\in C$ with $u\leq_{\Pi}\ell$, and
$(state(\ell)=no~{}or~{}state(\ell)=loop)$.

  * •

$blocked(u)=no$: let $C$ be a clause and $u\in C$. There does not exists an
existential literal $\ell$ with $u\leq_{\Pi}\ell$. That is, one can apply a
$\forall$-red step to $u$ in the clause $C$.
Or, for any existential literal $\ell\in C$ with $u\leq_{\Pi}\ell$ we have
$state(\ell)=yes$. That is, one can perform the $\forall$-red step on u in
future after refuting all the existential literals blocking $u$.

Before proceeding further, we present a simple example to clarify the
defintion of loop and inf.

Consider the following slightly modified QBF-Prolog program from [22]:

$P=\exists a\forall d\exists b,c.(a\leftarrow
d,b,c)\wedge(b)\wedge(b\leftarrow b)$

We have $state(b)=inf$: since we have a successful refutation of $\leftarrow
b$ followed by an infinite branch (loop) in $T_{P}(\leftarrow b)$. Refer,
Figure 2.

$\leftarrow b$$loop$$\leftarrow b$$\hskip 2.84526pt\Box\hskip 2.84526pt$
Figure 2: Refutation tree $T_{P}(\leftarrow a)$ showing that $state(b)=inf$

However, we have $state(a)=loop$: since in the refutation tree
$T_{P}(\leftarrow a)$, there exists no refutation for $\leftarrow d,c$ and
also has an infinite branch. Refer, Figure 3.

$\leftarrow b,d,c$$loop$$\leftarrow b,d,c$$\leftarrow d,c$$\leftarrow
d,b,c$$\leftarrow d,c$$\leftarrow a$ Figure 3: Refutation tree
$T_{P}(\leftarrow a)$ showing that $state(a)=loop$

Observe that given the state of all existentil literals of a clause, computing
the states of a universal variable is simple. Denote it by comp-block($u,C$).

So, consider the problem of computing $state(x)$ for an existential literal
$x$, given a QBF-Prolog program $P$. That is, we need to refute $\leftarrow
x$. Clearly, for computing the $\text{SLD-Q}_{\text{Prolog}}$-resolution
refututation of $\leftarrow x$, one has to perform resolution of the clause
$\leftarrow x$ with a clause having head $x$. There can be several clauses in
$P$ with head $x$. For computing $state(x)$, we need to consider each of them
in the order in which they appear in $P$. However, in order to make discussion
simple, let us focus on just one clause $C$ with head $x$ and compute the
intermediate result $state(x,C)$. We use this result for computing the final
one. Let $C=x\leftarrow x_{1},x_{2},\dots,x_{n}$ be a clause with head $x$.
Note that some of the $x_{i}$’s may be universal, but $x$ is existential.

  * •

$state(x,C)=yes$: if $n=0$,
Or, for all existential $x_{i}$, $1\leq i\leq n,state(x_{i})=yes$ and for all
universal variables $x_{i}$ $1\leq i\leq n,blocked(x_{i})=no$.

  * •

$state(x,C)=inf$: if for all existential $x_{i},1\leq i\leq
n,state(x_{i})\in\\{yes,inf\\}$, and for all universal $x_{i},1\leq i\leq
n,blocked(x_{i})=no$, and there exist an $x_{j},1\leq j\leq
n,state(x_{j})=inf$.

  * •

$state(x,C)=loop$: there exists an existential $x_{i},1\leq i\leq
n,state(x_{i})=loop$, and for all existential $x_{k},1\leq
k<i,state(x_{k})=\\{yes,inf\\}$, and for all universal $x_{k},1\leq
k<i,blocked(x_{k})=no$.
Or, there exists an existential $x_{i},1\leq i\leq n$, such that while
refuting $\leftarrow x_{i}$, the refutation of $\leftarrow x$ is called
recursively, and for all existential $x_{k},1\leq
k<i,state(x_{k})=\\{yes,inf\\}$, and for all universal $x_{k},1\leq
k<i,blocked(x_{k})=no$.
Or, there exists $x_{i},2\leq i\leq n,state(x_{i})=no$, and there exists an
existential $x_{k},1\leq k<i,state(x_{k})=inf$, and for all existential
$x_{k},1\leq k<i,state(x_{k})=\\{yes,inf\\}$, and for all universal
$x_{k},1\leq k<i,blocked(x_{k})=no$.

  * •

$state(x,C)=no$: there exists an existential $x_{i},1\leq
i<n,state(x_{i})=no$, and for all existential $x_{k},1\leq
k<i,state(x_{k})=yes$, and for all universal $x_{k},1\leq
k<i,blocked(x_{k})=no$.
Or, there exists a universal variable $x_{k},1\leq k\leq
n,blocked(x_{k})=yes$.

Using these intermediate results, we are ready to describe the procedure of
refuting $\leftarrow x$ with a QBF-Prolog program $P$. That is, procedure to
compute $state(x)$, for any existential variable $x$.

Let the definite Horn clauses $C_{x}^{1},C_{x}^{2},\dots,C_{x}^{m}$ be the
clauses of $P$ with head $x$.

  * •

$state(x)=yes$: there exists an $i,1\leq i\leq m,state(x,C_{x}^{i})=yes$, and
for all $k,1\leq k<i,state(x,C_{x}^{k})=no$, and for all $j,i<j\leq
n,state(x,C_{x}^{j})\not\in\\{inf,loop\\}$.

  * •

$state(x)=inf$: there exists an $i,1\leq i\leq m,state(x,C_{x}^{i})=inf$, and
for all $k,1\leq k<i,state(x,C_{x}^{k})=no$
Or there exists an $i,1\leq i\leq m,state(x,C_{x}^{i})=yes$, and for all
$k,1\leq k<i,state(x,C_{x}^{k})=no$, and for all $j,i<j\leq
m,state(x,C_{x}^{j})\in\\{loop,inf\\}$.

  * •

$state(x)=loop$: there exists an $i,1\leq i\leq m,state(x,C_{x}^{i})=loop$,
and for all $k,1\leq k<i,state(x,C_{x}^{k})=no$.

  * •

$state(x)=no$: for all $i,1\leq i\leq m,state(x,C_{x}^{i})=no$.

Now, we are ready to present our linear time algorithm for computing the
function $output(P,C)$. Our algorithm is inspired and a slight modification of
the Algorithm from [22, Algorithm 5.16].

QBF-Prolog-linear: linear time algorithm
Recall the problem: given a QBF-Prolog program $P=\Pi.\phi$ and a query
definite Horn clause $C=(x\leftarrow x_{1},\dots,x_{n})$, with
$var(C)\subseteq var(P)$, answer the following:

$\displaystyle\text{Is }\Pi.\phi\models\Pi.(\phi\wedge C)?$

Following Lemma 5, we modify $P$ as $P^{\prime}=\Pi_{i}.(\neg x\wedge
x_{1}\wedge\dots\wedge x_{n}\wedge\phi)$ and want to find an
$\text{SLD-Q}_{\text{Prolog}}$-resolution of $\leftarrow x$ from $P^{\prime}$
efficiently.

In other words, we need to compute $state(x)$. We design the following
function for the same:
Refutation(x, loc-h(x)): the function computes $state(x)$. It takes two
parameters: variable $x$ and ‘loc-h(x)’: list of clauses from $P^{\prime}$
with head $x$. It output one of the following: $no,yes,loop,inf$. We maintain
these outputs as enum data structure: enum status = $\\{$ no, yes, loop, inf
$\\}$. (Thus, here enumeration variable ‘no’ represents $0$). Finally we set
the function $output(P,C)$ as follows:

$\text{output}(P,C)=\left\\{\begin{array}[]{l l}\text{yes}&\quad\text{if
Refutation(x,loc-h(x))}\in\\{yes,inf\\}\\\ \text{Refutation(x,loc-
h-x)}&\quad\text{otherwise}\end{array}\right.$

Here is our efficient pseudocode:

_status QBF-Prolog-linear(_quantified cnf-formula * $P$, cnf-clause * $C$_)_

Input: QBF-Prolog program $P=\Pi.\phi$ as a list of definite quantified Horn
clauses, and a definite query clause $C$ as a list

Output: output(P,C): yes, if Refutation return $\\{$yes, inf$\\}$, otherwise
return the value of the Refutation function; that is, either loop or no. The
return type is the enumeration status

/* $C=x\leftarrow x_{1},x_{2},\dots,x_{n}$, let $i$ represent the maximum
level of the literals of $C$ */

$P^{\prime}=\Pi_{i}.(\neg x\wedge x_{1}\wedge\dots\wedge x_{n}\wedge\phi)$

foreach  _existential variable $x\in var(P^{\prime})$_ do

$state(x)=new$

end foreach

result = Refutation(x,loc-h-x)

/* Call the Refutation function [Algorithm 3], which computes $state(x)$ and
store the output in the variable result. Refutation takes the variable x, and
a list of clauses from $P^{\prime}$ with head $x$ as its parameters. */

if  _result $\in\\{yes,inf\\}$_ then

return yes

else

return (result)

/* result can be no or loop */

end if

End Function

Algorithm 2 Linear time algorithm for QBF-Prolog inspired from [22].

We only need to present the linear time function Refutation. Before presenting
the speudocode for the same, we mention some preliminary remarks:

Observe that, for computing $state(x)$ for an existential variable $x$, we
need to consider all definite clauses $C_{x}^{i}$ of the QBF-Prolog program
$P$ with head $x$ in sequence. If $state(x,C_{x}^{i})=no$ for all of them then
we need to return a $no$. Otherwise, if we found a $loop$ or an $inf$ at any
moment, then we must return immediately a $loop$ or an $inf$ respectively.
Only when we encounter a yes for some definite Horn clause $C_{x}^{i}$, rest
of the clause of $P^{\prime}$ with head $x$ need to be considered.

During the course of execution, state of variables are going to change. At the
begining, we initialize $state(x)=new$ for all existential variables $x$
(refer, Algorithm 2). When we try to find a state of a variable $x$, we
replace it’s state from new to loop, as the first initialization. This will
make sure that the case of a recursive call for determining the state of $x$
is handled correctly. When a first refutation for $\leftarrow x$ is found, we
changed the state from loop to inf. This is the second initialization in our
Refutation function. Finally, we check that the correct answer is a yes
(finitely many refutations) or an inf (infinitely many refutations).

To make task easy, Refutation function uses another function Testclause.
TestClause: the function takes a definite Horn clause from $P^{\prime}$, and
finds the state of the positive literal of this clause based on the status of
it’s negative literals. In other words, it helps the Refutation function for
computing $state(x)$ by computing $state(x,C_{x}^{i})$, where $C_{x}^{i}$ is a
clause from $P^{\prime}$ with head $x$. TestClause uses Refutation function
for the same.

We now present the Refutation function in Algorithm 3.

_status Refutation(_variable $x$, list of quantified CNF clauses $S$ with head
$x$ from $P^{\prime}$_)_

Input: variable $x$, and a list of quantified CNF clauses with head $x$

Output: $state(x)$: return type is enumeration status.

if  _$state(x)==new$_ then

/* variable $x$ has not considered yet */

if  _is-empty $(S)$_ then

/* No clauses with $x$ as it’s head */

$state(x)=no$ /* we got the answer */

else

$state(x)=loop$;

/* First initialization. This handle the case of a recursive call */

stop = false;

while  _(not stop) and (not is-empty $(S)$)_ do

result = TestClause(first($S$))

/* first($S$) gives first clause from $S$ with head $x$ */

if  _result == no_ then

$S=S\setminus first(S)$

else

stop = true

end if

end while

if  _result $\neq$ yes_ then

state(x)=result /* we got the answer */

else

/* test remaining clauses for yes or inf */

infflag = false

$S=S\setminus first(S)$; $state(x)=inf$

while  _(not infflag) and (not is-empty $(S)$)_ do

result = TestClause(first($S$))

infflag = (result == loop) or (result == inf)

$S=S\setminus first(S)$

end while

if  _infflag_ then

$state(x)=inf$ /* encountered only loop or inf */

else

$state(x)=yes$

end if

end if

end if

return $state(x)$

End Function

Algorithm 3 Linear time algorithm for QBF-Prolog inspired from [22].

Now we finish this Section by presenting the function TestClause:

_status TestClause(_CNF clause *C_)_

Input: Clause $C=x\leftarrow x_{1},x_{2},\dots,x_{n}$ with existential head

Output: $state(head(C))$ with respect to the tail of $C$

/* literals of $C$ are arranged as per $\Pi_{i}$. Initialize as $n=0$ */

success = true; infflag = false; result = yes; i =1;

/* compute state of all universal literals of $C$ */

$\forall i$, with $x_{i}$ universal, result-array[i]=com-
block($x_{i},C^{\prime}$), where $C^{\prime}=C\setminus x$

while  _(success) and (not is-empty $(C)$)_ do

if  _sign(first( $C$)) == positive_ then

/* first($C$) returns first literal of $C$, i.e., ignore the head of $C$ */

$C=C\setminus first(C)$

else

/* consider next literal from the body of $C$ */

if  _first( $C$) == $\forall$_ then

if  _result-array[ $i$] = yes_ then

result = no /*  answer found, $x_{i}$ is blocked */

break /*  break the while loop */

i++ /* $x_{i}$ not blocked */

else

result-array$[$i$]$ = Refutation(first($C$), loc-h(first($C$)))

result = result-array$[$i$]$; i++;

success = (result == yes) or (result == inf)

/* when result ==loop, success = false and while loop ends */

if  _result == inf_ then

infflag = true

$C=C\setminus first(C)$

end if

end if

end while

switch  _result_ do

case  _result $\in\\{yes,inf\\}$_ do

if  _infflag_ then

return inf

else

return yes

end if

end case

case  _result == loop_ do

return loop

end case

case  _return == no_ do

if  _infflag_ then

return loop

else

return no

end if

end case

end switch

Algorithm 4 TestClause Function computing $state(x,C_{x})$ inspired from [22].

Time Complexity Analysis:
The time complexity of Refutation is linear in the length of the QBF-Prolog
program $P^{\prime}$, as every clause of $P^{\prime}$ is processed at most
once. Only we need to be careful in the function TestClause, as we need to
compute the state of universal variables as well. For this, we just maintained
and array ‘result-array’ and computed the required information at the very
begining. Thus, this increases the complexity additively. This proves the
following.

######  Theorem 4.1.

For a QBF-Prolog program $P$ and a query clause $C$, with $var(C)\subseteq
var(P)$, it is possible to compute the function $output(P,C)$ in linear time
in the length of $P$ and $C$.

##  5 Theory for QBF-Prolog with no restrictions on the query clause

In this Section, we develop theory for the QBF-Prolog without any restrictions
on the query Horn clause. That is, the query clause may contains new variables
as well. To be precise, given a QBF-Prolog program $P=\Pi.\phi$ and a query
Horn clause $C$, is the following true:

$P=\Pi.\phi\models\Pi^{\prime}.(\phi\wedge C)?$

where, $C$ may contains new variables which do not occur in $P$. Here,
$\Pi^{\prime}$ is obtained by extending $\Pi$ by the new variables of $C$.
There is no restriction on how these new variables are placed in the prefix
$\Pi$.

We show in this section, that this case is not interesting for the QBFs. That
is, if the query clause $C$ contains a new existential variable, then $C$ will
be implied by $P$ for sure, and if $C$ has a new universal variable $u$, one
can drop $u$ and still preserves the answer.

We show this using the property QIOR+ from [27]. We show that if the query
clause contains a new existential variable, then $C$ will satisfy the QIOR+
property for sure and hence $C$ will be redundant for the QBF-Prolog program
$P$. We need the following definitions:

######  Definition 5 (Outer clause[17]).

The outer clause of a clause $C$ on literal $\ell\in C$ with respect to the
prefix $\Pi$ is the clause $OC(\Pi,C,\ell)=\\{k~{}|~{}k\in
C,k\leq_{\Pi}\ell,k\neq\ell\\}.$

Clearly, $OC(\Pi,C,\ell)$ of clause $C$ on literal $\ell\in C$ contains all
literals of $C$, exluding $\ell$, which are smaller than or equal to $\ell$ in
the variable ordering of prefix $\Pi$.

######  Definition 6 (Outer resolvent[17]).

Let $C$ be a clause with $\ell\in C$ and $D$ a clause occurring in QBF
$\Pi.\phi$ with $\neg\ell\in D$. The outer resolvent of $C$ with $D$ on
literal $\ell$ with respect to the quantifier prefix $\Pi$, denoted
$OR(\Pi,C,D,\ell)$ is the following:

$OR(\Pi,C,D,\ell)=C\setminus\\{\ell\\}\cup OC(\Pi,D,\neg\ell)$

The following Definition is the extension of the property Quantified Implied
Outer Resolvent (QIOR) from [17].

######  Definition 7 (QIOR+ [27]).

A clause $C$ has property QIOR+ with respect to QBF $\Pi.\phi$ on literal
$\ell\in C$ iff

$\Pi.\phi\equiv\Pi.(\phi\wedge OR(\Pi,C,D,\ell))$

for each clause $D\in\phi$ with $\neg\ell\in D$.

Recall, that by, $\Pi.\phi\equiv\Pi.(\phi\wedge OR(\Pi,C,D,\ell)$, we mean
that both QBFs are logical equivalent, that is, every model of one QBF is also
the model of another. It has been proved in [27], that a clause with QIOR+
property on some existential literal $\ell$ with respect to a QBF
$\mathcal{F}=\Pi.\phi$ is redundant for the QBF $\mathcal{F}$. That is, we may
add or remove the clause $C$ from $\mathcal{F}$ without effecting the
satisfiability of $\mathcal{F}$. We below state the corresponding Theorem from
[27].

######  Theorem 5.1 ([27]).

Given a QBF $\mathcal{F}=\Pi.\phi$ and a clause $C$ with QIOR+ on an
existential literal $\ell\in C$ with respect to QBF
$\mathcal{F}^{\prime}=\Pi^{\prime}.\phi^{\prime}$, where
$\phi^{\prime}=\phi\setminus\\{C\\}$ and $\Pi^{\prime}$ is same as $\Pi$ with
variables and respective quantifiers removed that no longer appear in
$\phi^{\prime}$. Then $\mathcal{F}\equiv_{\text{sat}}\mathcal{F}^{\prime}$.

Thus, Theorem 5.1 states that the clause $C$ with QIOR+ property on some
existential literal is redundant for the QBF, and can be added or removed. We
also have universal elimination theorem from [27].

######  Theorem 5.2 ([27]).

Given a QBF $\mathcal{F}_{0}=\Pi.\phi$ and $\mathcal{F}=\Pi.(\phi\cup\\{C\\})$
where $C$ has QIOR+ on a universal literal $\ell\in C$ with respect to the QBF
$\mathcal{F}_{0}$. Let $\mathcal{F}^{\prime}=\Pi.(\phi\cup\\{C^{\prime}\\})$,
with $C^{\prime}=C\setminus\\{\ell\\}$. Then
$\mathcal{F}\equiv_{\text{sat}}\mathcal{F}^{\prime}$.

Remarks: Although, QIOR+ is extremely powerful in terms of redundancy
detection, checking for the QIOR+ property in practice is too costly. Since,
even for the propositional case checking whether an outer resolvent is implied
by a propositional formula is co-NP hard. So, one needs a redundancy property
that can be checked in polynomial time. One such redundancy property is the
QRAT [17]. Following QRAT, QRAT+ [27] have been introduced, which is a
polynomial time redundancy property for a clause, based on QUP (quantified
unit propogation). It has been proved in [27], that QRAT+ is more powerful
than QRAT in terms of redundancy detection.

However, we do not need QRAT+ to prove our results, QIOR+ will suffice.

######  Observation 4.

Let $P=\Pi.\phi$ be a QBF Prolog program. And, let $C$ be a definite Horn
query clause. If there exists an existential literal say, $\ell\in C$ which is
new. That is, $\ell\in var(C)$ but $\ell\not\in var(\phi)$. Then, we know that
$C$ for sure has QIOR+ property with respect to the QBF Prolog program $P$:
since there exists no clause $D$ in $\phi$ with $\neg\ell\in D$. Therefore,
$C$ is redundant by Thereom 5.1. That is, the answer is yes for our problem.

######  Observation 5.

Let $P=\Pi.\phi$ be a QBF Prolog program. And, let $C$ be a definite Horn
query clause. If there exists a universal literal $\ell\in C$ which is a new
literal, that is universal $\ell\in var(C)$ but $\ell\not\in var(\phi)$. Then
by Thereom 5.2, we can drop universal literal $\ell$ from $C$ safely and then
ask the problem for the remaining clause.

QBF-Prolog for First-order Predicate Horn Logic: Recall the Definition of
first-order predicate Horn logic from Section 2. In this logic, we may replace
each literal in a Horn clause by arbitrary predicate of any bounded arity. The
QBF-Prolog defined in the previous section is capable of solving the first-
order Horn logic. That is, given facts, rules and query as first-order
predicate Horn formulas, the QBF-Prolog computes the function output(P,C) in
linear time. Note that a predicate may contains arbirary quantified variables,
which is not allowed in the existing Prolog. The algorithm for first-order
predicate Horn logic is exactly as the Algorithm 2. The only difference is
that now the algorithm treats each predicate of the query Horn clause as a
literal. For the resolution step of literals corresponding to the predicates,
the algorithm may use unification to make them syntatically equal.

To be precise, let $C$ be a first-order query Horn clause. Every predicates
$P(x_{1},\cdots,x_{k})$ appearing in clause $C$ is considered as a literal
$\ell$. Also, the literal $\ell=P(x_{1},\cdots,x_{k})$ is considered as an
existential literal (recall the definition of abstraction). We can resolve the
literal $P(x_{1},\cdots,x_{k})$ with the same predicate
$P(y_{1},\cdots,y_{k})$ in rule clause $\tilde{C}$ only if for each index $i$,

  1. (1)

the quantifier of $y_{i}$ is $\forall$, or,

  2. (2)

if quantifier of $y_{i}$ is $\exists$ then the quantifier of $x_{i}$ is
$\exists$.

Recall that the variables occur in the same order as in the quantifier prefix.
As the quantification of variables stays same in the resolvent, it can
restricts the set of clause with which one can resolve a predicate $P$.

Note that for any literals $P(x)$ and $P(y)$ with $x\neq y$, separate states
will be maintained by the algorithms.

##  6 Applications of QBF-Prolog

In this Section, we present some applications of the QBF-Prolog. Observe that
the existing Prolog is a subset of QBF-Prolog. Hence, QBF-Prolog can handle
problems that can be handled by the existing Prolog. Now we present some
examples which can be handled by QBF-Prolog but not by the exisiting Prolog.

###  6.1 Application 1: QBFs

Recall the limitations of Prolog: it is not possible to define rules having an
existentially quantified head, and having body with arbitrary quantifications.

Below example illustrates, that the QBF-Prolog has no such restrictions. Let
us consider the following simple QBF-Prolog program [4]:

$\displaystyle\mathcal{P}_{n}=\Pi.\phi=$ $\displaystyle\exists e_{0}\forall
u_{1}\exists e_{1}\dots u_{n}\exists e_{n}.$
$\displaystyle\textrm{For~{}}i\in[n],D_{i}$
$\displaystyle:~{}~{}~{}~{}({e}_{i-1}\vee\neg u_{i}\vee\neg e_{i})\ \wedge$
$\displaystyle D_{n+1}$ $\displaystyle:~{}~{}~{}~{}({e}_{n})$

Clearly, in this QBF-Prolog program, the head ($e_{i-1}$) of the rules are
existential, which is not possible in Prolog. Also, the body of the Horn
clauses have both existentially (i.e., $e_{i}$’s) and universally (i.e.,
$u_{i}$’s) quantified variables.

Consider a simple query clause $C=(e_{0})$. Observe that $var(C)\subseteq
var(\mathcal{P}_{n})$. As, the variable $e_{0}$ belongs to the first level in
the quantifier prefix $\Pi$, we have the abstraction $\Pi_{1}.\phi$ is same as
$\Pi.\phi$. Since, we have simple SLD-Q-Res refutation of $\Pi_{1}.(\neg
e_{0}\wedge\phi)$ (Figure 4), the QBP-Prolog is capable to show that the
following: $\Pi.\phi\models\Pi.(\phi\wedge C)$.

To be precise, in order to solve the above problem, we invoke the Algorithm 2,
with parameters $\mathcal{P}_{n}$ and $(e_{0})$. The Algorithm inturn calls
the Algorithm 3, with parameters $e_{0}$ (precisely, $\neg e_{0}$) and
$(e_{0}\vee\neg u_{1}\vee\neg e_{1})$. Algorithm 3 inturn call the Algorithm
4, with the parameter $(e_{0}\vee\neg u_{1}\vee\neg e_{1})$. The recursion
will end when the TestCase($(e_{n})$) function returns a yes, which evetually
reaches to the first level of recursion and Algorithm 2 also returns a yes.

$\hskip 2.84526pt\Box\hskip 2.84526pt$$\neg u_{1}\vee\cdots\vee\neg
u_{n}$$\neg u_{1}\vee\cdots\vee\neg u_{n}\vee\neg e_{n}$$\hskip
2.84526pte_{n}\hskip 2.84526pt$$D_{n+1}$$\neg u_{1}\vee\neg u_{2}\vee\neg
u_{3}\vee\neg e_{3}$$\neg u_{1}\vee\neg u_{2}\vee\neg e_{2}$$e_{2}\vee\neg
u_{3}\vee\neg e_{3}$$D_{3}$$\neg u_{1}\vee\neg e_{1}$$e_{1}\vee\neg
u_{2}\vee\neg e_{2}$$D_{2}$$\hskip 2.84526pt\neg e_{0}\hskip 2.84526pt$$\neg
C$$e_{0}\vee\neg u_{1}\vee\neg e_{1}$$D_{1}$$n~{}\forall$-Red steps Figure 4:
An SLD-Q-Res refutation of $\Pi.(\neg e_{0}\wedge\phi)$ [4] for Application
6.1

###  6.2 Application 2: Tree-bipartite-problem

Consider the problem tree-bipartite from Example 1 of Section 1.1. The problem
has the following rules: undirected graphs without cycles are bipartite, and
trees are acyclic. Such rules can be easily encoded in the Existing Prolog.
Let us present an encoding in detail. The encoding uses the following
predicates with the following interpretations:

$\displaystyle Nocycle(g)~{}~{}/*\text{the predicate is 1 iff }g\text{ has no
cycles}*/$ $\displaystyle Bipartite(g)~{}~{}/*\text{ the predicate is 1 iff
}g\text{ is bipartite}*/$ $\displaystyle Tree(g)~{}~{}/*\text{ the predicate
is 1 iff }g\text{ is a tree}*/$

Now, using these predicates, we have the following QBF-Prolog program for the
tree-bipartite problem.

$\displaystyle\forall g.Nocycle(g)\rightarrow Bipartite(g)~{}~{}/*\text{ rule
1}*/$ $\displaystyle\forall g.Tree(g)\rightarrow Nocycle(g)~{}~{}/*\text{ rule
2}*/$

Consider the following query which cannot be handled by the existing Prolog as
they required universally quantified variables: are all trees bipartite? Below
is the query clause for the same.

$\displaystyle\forall g.Tree(g)\rightarrow Bipartite(g)~{}~{}/*\text{
query}*/$

Our algorithm solves the problem as follows: It first adds the negation of the
query clause in the QBF-Prolog program. That is we have,

$\displaystyle P^{\prime}=\Pi_{i}.\neg Bipartite(g)\wedge Tree(g)\wedge\phi$

Certainly, the predicates corresponding to the query clause becomes
existential. The algorithm picks the $\neg Bipartite(g)$ as the top clause and
derives the empty clause using rule 1, and rule 2, as follows: $\neg
Bipartite(g)$ $\neg Nocycle(g)\vee Bipartite(g)$ $\neg Nocycle(g)$ $\neg
Tree(g)\vee Nocycle(g)$ $\neg Tree(g)$ $Tree(g)$ $\Box$

###  6.3 Application $3$: Bipartite problem

Consider the problem related to the simple bipartite graphs $G=(V,E)$ with
vertex partitions $U$ and $W$, from Section 1.1 (refer Example 2). Assume that
$G$ has no loops and multiple edges. Consider a QBF-Prolog program which
specifies the class of bipartite graphs. This can be encoded in first-order
predicate Horn logic with only universally quantified variables. Let us
present below one of the encodings in detail. The encoding uses the following
predicates with the following interpretations:

$\displaystyle E(x,y)~{}~{}/*\text{the predicate is 1 iff there exists and
edge between vertices }x\text{ and }y*/$ $\displaystyle first(x)~{}~{}/*\text{
the predicate is 1 iff }x\text{ belongs to the first part }U\text{ of the
bipartite graph}*/$ $\displaystyle second(x)~{}~{}/*\text{ the predicate is 1
iff }x\text{ belongs to the second part }W\text{ of the bipartite graph}*/$

Now, using these predicates, we have the following QBF-Prolog program for the
bipartite graphs.

$\displaystyle\forall x,y.[first(x)\wedge E(x,y)]\rightarrow
second(y)~{}~{}/*\text{ rule 1}*/$ $\displaystyle\forall x,y.[E(x,y)\wedge
second(x)]\rightarrow first(y)~{}~{}/*\text{ rule 2}*/$ $\displaystyle\forall
x.first(x)\rightarrow\neg second(x)~{}~{}/*\text{ rule 3}*/$
$\displaystyle\forall x.E(x,y)\rightarrow E(y,x)~{}~{}/*\text{ rule 4}*/$

We quickly explain the above rules: Rule 1 says that if an edge $\\{x,y\\}$ is
present in the bipartite graph $G$ and $x\in U$ then we have $y\in W$.
Similarly, rule 2 can be explained. Rule 3 says that if a vertex belong to $U$
then it does not belong to $W$. Rule 4 says that the predicate $E(x,y)$ is
symmetric in nature.

Now, consider the following query regarding a bipartite graph
$G=(\\{U,W\\},E)$ which uses universal variables and hence cannot be supported
by the existing Prolog: starting from any vertex $x\in U$, and after jumping
two hops via edges in $G$, do we again reach the set $U$? Below is the
quantified query clause $C$ for the same:

$\displaystyle\forall x,y,z.[first(x)\wedge E(x,y)\wedge E(y,z)]\rightarrow
first(z)~{}~{}/*\text{ query Horn clause for QBF-Prolog}*/$

Certainly, such queries are valid for the QBF-Prolog. The algorithm solves the
problem as follows: It first adds the negation of the query clause $C$ in the
QBF-Prolog program. That is, we have

$P^{\prime}=\Pi_{i}.\neg first(z)\wedge first(x)\wedge E(x,y)\wedge
E(y,z)\wedge\phi$

Clearly, all the literal in $P^{\prime}$ corresponding to the predicate of $C$
becomes existential. The algorithm picks $\neg first(z)$ and resolves it with
rule 2 after substituting $y/z$ in the same. Substituting $y/z$ in rule 2 we
get: $\neg E(x,z)\vee\neg second(x)\vee first(z)$. That is, we have $\neg
first(z)$ $\neg E(x,z)\vee\neg second(x)\vee first(z)$ $\neg E(x,z/y)\vee\neg
second(x)$ $E(x,y)$ $\neg second(x)$

We derived $\neg second(x)$ at this moment. We proceed as follows: $\neg
second(x/y)$ $\neg first(x)\vee\neg E(x,y)\vee second(y)~{}~{}\text{ /*rule
1*/}$ $\neg first(x)\vee\neg E(x,y)$ $first(x)$ $\neg E(x,y)$ $E(x,y)$ $\Box$

Thus, the algorithm returns true for this query.

###  6.4 Application 4: Simple relations

Consider the problem of Example 3 of the Section 1.1. The problem uses the
following predicates:

$\displaystyle P(h,k)~{}~{}\text{/* the predicate is 1 iff }k=2h*/$
$\displaystyle R(h,k)~{}~{}\text{/* the predicate is 1 iff }h<k*/$

We may give several interpretations to these predicates. For example, if $k$
and $h$ represent graphs, then the predicate $R(k,h)$ is $1$ iff the graph $h$
is a subgraph of the graph $k$. The predicate $P(k,h)$ is $1$ iff the graph
$k$ is a superset of the graph $h$. That is, the graph $k$ is constructed from
$h$ by say adding a vertex.

Let us now consider the following facts and rules:

$\displaystyle\forall h\exists k.P(h,k)~{}~{}\text{/* fact 1 */}$
$\displaystyle\forall h,k.P(h,k)\rightarrow R(h,k)~{}~{}\text{/* rule 1 */}$
$\displaystyle\forall h_{1},h_{2},h_{3}.[R(h_{1},h_{2})\wedge
R(h_{2},h_{3})]\rightarrow R(h_{1},h_{3})~{}~{}\text{ /* rule 2 */}$

Now consider the following query:

$\displaystyle\forall h\exists g,k.[P(h,g)\wedge P(g,k)]\rightarrow
R(h,k)~{}~{}\text{ /* query */}$

Clearly the query is correct according to our interpretation. Our algorithm
solves the problem as follows: It first adds the negation of the query clause
in the QBF-Prolog program. That is, we have,

$\displaystyle P^{\prime}=\Pi_{i}.\neg R(h,k)\wedge P(h,g)\wedge
P(g,k)\wedge\phi$

Recall, all predicates of the query clause becomes existential. The algorithm
picks $\neg R(h,k)$ as the top clause and derive the empty clause as follows:
$\neg R(h,k)$ $\neg P(h,k)\vee R(h,k)\text{/* rule 1 */}$ $\neg P(h,k)$
$P(h,g/k)\text{/* added clause from }P^{\prime}*/$ $\Box$

###  6.5 Application 5

Consider the Prolog program mentioned in Example 4. The problem cannot be
handeled by existing Prolog, as it requires variables with both quantifiers.
Also, the proof for the problem is based on induction, as a result, instead of
solving the problem, the QBF-Prolog return a loop.

Let us now encode the problem: given trees with unique root and such that
every node has only one parent node. The program uses the following
predicates:

$\displaystyle E(x,y)~{}~{}/*\text{the predicate is 1 iff there exists and
edge between vertices }x\text{ and }y*/$ $\displaystyle
Notroot(x)~{}~{}/*\text{ the predicate is 1 iff }x\text{ is not the root}*/$
$\displaystyle Root(x)~{}~{}/*\text{ the predicate is 1 iff }x\text{ is the
root}*/$ $\displaystyle P(x)~{}~{}/*\text{ the predicate is an indicator used
for connectivity}*/$

Using the above predicates we now present a QBF-Prolog program specifying the
trees.

$\displaystyle\forall x,y.E(x,y)\rightarrow\neg E(y,x)~{}~{}/*\text{ rule 1:
tree is directed}*/$ $\displaystyle\forall x\exists y.Notroot(x)\rightarrow
E(y,x)~{}~{}/*\text{ rule 2: if x is not root then it has a parent y}*/$
$\displaystyle\forall x\exists y\forall z.E(y,x)\wedge
Notroot(x)\wedge\neg(z=y)\rightarrow\neg E(z,x)~{}~{}/*\text{rule3: every non
root node has unique parent}*/$ $\displaystyle\forall x.Root(x)\rightarrow\neg
Notroot(x)~{}~{}/*\text{ rule4: if x is a root then x is not a Nonroot}*/$
$\displaystyle\exists x\forall yRoot(x)\wedge\neg(y=x)\rightarrow\neg
Root(y)~{}~{}/*\text{ rule5: there is a unique root}*/$ $\displaystyle\exists
x.Root(x)\rightarrow P(x)~{}~{}/*\text{rule6: if x is a root then the
indicator P(x) is true}*/$ $\displaystyle\forall x,y.P(x)\wedge
E(y,x)\rightarrow P(y)~{}~{}/*\text{rule7: this rule is for connectivity}*/$

Now, consider the following query:

$\displaystyle\forall x.P(x)~{}~{}/*\text{ is tree connected?}*/$

Observe that one may easily prove this query via induction. However, QBF-
Prolog will detect a loop since it unables to mimic the inductive proofs. To
be precise, the algorithm adds the negation of the predicate of the query
clause in the QBF-Prolog program. That is, we have

$P^{\prime}=\Pi_{i}.\neg P(x)\wedge\phi$

So we have $\neg P(x)$ $\neg P(x)\vee\neg E(x,y/x)\vee P(y/x)~{}~{}\text{ rule
7: substitute y by x}$ $\neg P(x)\vee\neg E(x,y/x)$ The algorithm again needs
to refute $\leftarrow P(x)$ hence outputs a loop.

##  7 Conclusion

The paper overcomes one of the major logical limitations of Prolog of not
allowing arbitrary quantified variables in the rules, facts and queries. The
paper achieves this by extending the SLD-Res proof systems to quantified
Boolean Horn formuals, followed by proposing an efficient implementation for
the following problem: given a quantified Boolean Horn formula
$\mathcal{F}=\Pi.\phi$ and a clause $C$, is $\Pi.\phi\implies\Pi.(\phi\wedge
C)?$. The paper shows that the implementation can also handles the first-order
predicate Horn logic.

We also saw that the proposed algorithms unables to solve problems with
inductive proofs. The next step is to extend the algorithm for simple problems
based on induction. For example, extending the algorithm to handle the tree
problem of Application 6.5.

The satisfiability problem for the first-order predicate formulas is known as
the Satisfiability Modulo Theories (SMT) problem. Designing efficient SMT
solvers for formulas over arbitrary quantified variables is challenging. Our
implementation behaves as an SMT-solver for the first-order predicate Horn
formulas, over arbitrary quantified variables.

#### Acknowledgements.

We thank Olaf Beyersdorff, Meena Mahajan, and Leroy Chew for useful
discussions on extending Prolog to QBFs in the Dagstuhl Seminar ‘SAT and
Interactions’ (20061). This work is partially supported by FONDECYT-CONICYT
postdoctorate program project: 3190527 in the Department of Mathematics,
Pontifica Universidad Catolica de Chile ($1$st author).

## References

  * [1] Sanjeev Arora and Boaz Barak.  Computational Complexity – A Modern Approach.  Cambridge University Press, 2009.
  * [2] Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko.  Solving existentially quantified Horn clauses.  In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 869–882. Springer, 2013.
  * [3] Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew.  Lower bounds: From circuits to QBF proof systems.  In Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science, Cambridge, MA, USA, January 14-16, 2016, pages 249–260, 2016.
  * [4] Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla.  Are short proofs narrow? QBF resolution is _Not_ so simple.  ACM Trans. Comput. Log., 19(1):1:1–1:26, 2018.
  * [5] Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko.  On solving universally quantified Horn clauses.  In Francesco Logozzo and Manuel Fähndrich, editors, Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, volume 7935 of Lecture Notes in Computer Science, pages 105–125. Springer, 2013.
  * [6] A. Blake.  Canonical expressions in Boolean algebra.  PhD thesis, University of Chicago, 1937.
  * [7] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.  Counterexample-guided abstraction refinement for symbolic model checking.  J. ACM, 50(5):752–794, 2003.
  * [8] Alain Colmerauer and Philippe Roussel.  The birth of prolog.  In John A. N. Lee and Jean E. Sammet, editors, History of Programming Languages Conference (HOPL-II), Preprints, Cambridge, Massachusetts, USA, April 20-23, 1993, pages 37–52. ACM, 1993.
  * [9] Alain Colmerauer and Philippe Roussel.  The birth of prolog.  In History of Programming Languages Conference (HOPL-II), Preprints, Cambridge, Massachusetts, USA, April 20-23, 1993, pages 37–52, 1993\.
  * [10] Ronald de Wolf and Shan-Hwei Nienhuys-Cheng.  Foundations of Inductive Logic Programming. LNCS (LNAI), volume 1228\.  Springer, Heidelberg, 1997.
  * [11] Jean H. Gallier.  Logic for Computer Science: Foundations of Automatic Theorem Proving, Second Edition.  Dover, Mineola, New York, 2015.
  * [12] Allen Van Gelder.  Contributions to the theory of practical quantified boolean formula solving.  In Principles and Practice of Constraint Programming (CP), pages 647–663, 2012.
  * [13] Alexandra Goultiaeva, Vicki Iverson, and Fahiem Bacchus.  Beyond CNF: A circuit-based QBF solver.  In Theory and Applications of Satisfiability Testing (SAT), pages 412–426, 2009.
  * [14] Armin Haken.  The intractability of resolution.  Theoretical Computer Science, 39(2-3):297–308, August 1985.
  * [15] Joseph Y. Halpern.  Presburger arithmetic with unary predicates is $\Pi_{1}^{1}$-complete.  J. Symb. Log., 56(2):637–642, 1991.
  * [16] Jean-Jacques Hébrard.  A linear algorithm for renaming a set of clauses as a Horn set.  Theor. Comput. Sci., 124(2):343–350, 1994.
  * [17] Marijn J. H. Heule, Martina Seidl, and Armin Biere.  Solution validation and extraction for QBF preprocessing.  J. Autom. Reasoning, 58(1):97–125, 2017.
  * [18] Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke.  Solving QBF with counterexample guided refinement.  In Theory and Applications of Satisfiability Testing (SAT), pages 114–128, 2012.
  * [19] Mikolás Janota and João P. Marques Silva.  Abstraction-based algorithm for 2QBF.  In Theory and Applications of Satisfiability Testing (SAT), pages 230–244, 2011.
  * [20] Jan Johannsen.  Unpublished.  2005\.
  * [21] Hans Kleine Büning, Marek Karpinski, and Andreas Flögel.  Resolution for quantified boolean formulas.  Inf. Comput., 117(1):12–18, 1995.
  * [22] Hans Kleine Büning and Theodor Lettmann.  Propositional logic - deduction and algorithms, volume 48 of Cambridge tracts in theoretical computer science.  Cambridge University Press, 1999.
  * [23] William Klieber, Samir Sapra, Sicun Gao, and Edmund M. Clarke.  A non-prenex, non-clausal QBF solver with game-state learning.  In Theory and Applications of Satisfiability Testing (SAT), pages 128–142, 2010.
  * [24] Robert Kowalski and Donald Kuehner.  Linear resolution with selection function.  Artificial Intelligence, 2:227–260, 1971.
  * [25] Robert A. Kowalski.  Predicate logic as programming language.  In IFIP Congress, pages 569–574, 1974.
  * [26] Florian Lonsing and Uwe Egly.  Depqbf 6.0: A search-based QBF solver beyond traditional QCDCL.  In Automated Deduction (CADE), pages 371–384, 2017.
  * [27] Florian Lonsing and Uwe Egly.  QRAT+: generalizing QRAT by a more powerful QBF redundancy property.  In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 161–177. Springer, 2018.
  * [28] D. W. Loveland.  A linear format for resolution.  In Symposium on Automated Deduction, Lecture Notes in Mathematics, 125:147–162, 1970.
  * [29] Peter J. F. Lucas and Linda C. van der Gaag.  Principles of expert systems.  International computer science series. Addison-Wesley, 1991.
  * [30] David Monniaux and Laure Gonnord.  Cell morphing: From array programs to array-free Horn clauses.  In Xavier Rival, editor, Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, volume 9837 of Lecture Notes in Computer Science, pages 361–382. Springer, 2016.
  * [31] Roussel Philippe.  Prolog.  manuel de r fdrence et d’utilisalion, Groupe Intelligence Artificielle, Faculta des Sciences de Luminy, Universit6 Aix-Marseille II, France, 1975.
  * [32] John Alan Robinson.  A machine-oriented logic based on the resolution principle.  Journal of the ACM, 12:23–41, 1965.
  * [33] Neil C. Rowe.  Artificial intelligence through Prolog.  Prentice Hall, 1988.
  * [34] Ashish Sabharwal.  Algorithmic Applications of Propositional Proof Complexity.  PhD thesis, University of Washington, 2005.
  * [35] Anil Shukla.  On proof complexity for quantified Boolean formulas.  PhD thesis, The Institute of Mathematical Sciences, Chennai, 2017.
  * [36] João P. Marques Silva and Karem A. Sakallah.  GRASP: A search algorithm for propositional satisfiability.  IEEE Trans. Computers, 48(5):506–521, 1999.
  * [37] Marco Voigt.  Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates.  PhD thesis, Saarland University, Saarbrücken, Germany, 2019.
  * [38] Robert S Wolf.  A Tour through Mathematical Logic.  The Carus Mathematical Monographs, Number Thirty, California Polytechnic State University, 2005.
  * [39] N. K . Zamov and V. I. Sharanov.  A class of strategies for the determination of provability by the resolution method.  In A.O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic, Part III, Seminars in Mathematics, V.A. Steklov Mathematical Institute, Leningrad, 16:26–31, 1971.  Translated from Russian by J. S. Wood.
  * [40] Lintao Zhang and Sharad Malik.  Conflict driven learning in a quantified boolean satisfiability solver.  In Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design (ICCAD), pages 442–449, 2002.