= Solution
Let $V$ be the <set> of <Boolean variables> occurring in $T$ or the initial query $Q$, and put $N=|V|$. Represent a current query by a <subset> $R\subseteq\{\neg p:p\in V\}$: the <Boolean literals> in this <set> are the outstanding obligations. The initial state is $R=Q$, and the <goal test> is $R=\varnothing$.
An action chooses a <Horn clause> $C\in T$ with positive <Boolean literal> $p$, provided $\neg p\in R$. Its <search transition model> is precisely the given <resolution inference rule>:
$$
R\longmapsto R'=(C\cup R)\setminus\{p,\neg p\}.
$$
Thus it removes the obligation $\neg p$ and inserts all negative <Boolean literals> of $C$. Repeated <Boolean literals> merge because queries are <sets>. A <Horn clause> without a positive <Boolean literal> supplies no action under the rule specified in this paper; it must not be treated as an additional way of finishing the query.
Give every action unit cost. A <graph path> with $\ell$ actions gives a proof containing $\ell+1$ queries, so minimizing either quantity gives the same shortest proof. <Uniform-cost search> orders the <search frontier> by the number of actions already taken and applies the <goal test> when removing a <search node> for expansion. Recording parent actions reconstructs the proof.
There are at most two choices, present or absent, for each of the $N$ negative <Boolean literals>. Therefore
$$
\boxed{c(R,C,R')=1,\qquad |\mathcal S|\le 2^N.}
$$
This bounds the <state space>, including the empty query, rather than the possibly infinite <search tree> of action histories.<Intelligent Systems examination paper by the University of Oxford (2015)>[Printed p. 2, corrected Question 1, definitions and part (a)]{ref}
Back to article page
