1: \documentclass{article}

2: \usepackage{times}

3: \usepackage{amssymb}

4: \usepackage[latin1]{inputenc}

5: \usepackage{proof}

6: %\usepackage{amsthm}

7: 

8: \usepackage{epsfig}

9: \usepackage{latexsym}

10: 

11: 

12: \usepackage[dvips]{color}

13: 

14: \usepackage{url}

15: 

16: \def\nat{\mathbb{N}}

17: \def\int{\mathbb{Z}}

18: 

19: 

20: 

21: 

22: \usepackage{float}

23: \floatstyle{ruled}

24: \newfloat{algo}{h}{lop}

25: \floatname{algo}{Algorithm}

26: 

27: 

28: \def\proof{{\bf Proof: }}

29: \def\endproof{}

30: \def\qed{\hfill$\Box$\vskip0.8em}

31: 

32: 

33: 

34: \newtheorem{theorem}{Theorem}

35: \newtheorem{lemma}{Lemma}

36: \newtheorem{example}{Example}

37: 

38: \newcounter{countlem}

39: \newcounter{countth}

40: \def\savelemmacounter{\setcounter{countlem}{\value{lemma}}}

41: \def\restorelemmacounter{\setcounter{lemma}{\value{countlem}}}

42: \def\savethcounter{\setcounter{countlem}{\value{theorem}}}

43: \def\restorethcounter{\setcounter{theorem}{\value{countlem}}}

44: \def\namelem#1{\setcounter{#1}{\value{lemma}}}

45: \def\putlem#1{\setcounter{lemma}{\value{#1}}}

46: \def\nameth#1{\setcounter{#1}{\value{theorem}}}

47: \def\putth#1{\setcounter{theorem}{\value{#1}}}

48: 

49: \newcommand\ForAuthors[1]%          %  temporary remark for the

50:  {\par\smallskip                     %  authors:

51:   \begin{center}%                    %

52:    \fbox%                            %    --------

53:    {\parbox{0.9\linewidth}%          %    |  #1  |

54:     {\raggedright\sc--- #1}%         %    --------

55:    }%                                %

56:   \end{center}%                      %

57:   \par\smallskip                     %

58:  }

59: 

60: \def\limp{\mathbin{\Rightarrow}}

61: \def\liff{\mathbin{\Leftrightarrow}}

62: \def\limpleft{\mathbin{\Leftarrow}}

63: 

64: \def\sem#1{[\mskip-\thinmuskip[{#1}]\mskip-\thinmuskip]}

65: 

66: 

67: \def\onevar{\mathcal{V}_1}

68: \def\flat{\mathcal{F}}

69: \def\c{\mathcal C}

70: \def\onevarh{\mathcal{V}_1Horn}

71: \def\flath{\mathcal{F}Horn}

72: \def\ch{\mathcal CHorn}

73: \def\reach{\mathsf{reach}}

74: \def\known{\mathsf{known}}

75: \def\empcl{\Box}

76: \def\atle{\le}

77: \def\atge{\ge}

78: \def\atlt{<}

79: \def\atltss{<_s}

80: \def\atgt{>}

81: \def\sublt{\prec}

82: \def\subltss{\prec_s}

83: \def\subst{\Omega}

84: \def\substt{\Gamma}

85: \def\substtt{\Delta}

86: \def\abs{\sqsubseteq}

87: \def\abss{\abs}

88: \def\absh{\abs_h}

89: \def\pmodels{\vDash_{\mathrm{p}}}

90: \def\pnmodels{\nvDash_{\mathrm{p}}}

91: \def\seq#1{({#1})}

92: \def\repl{\rightarrow}

93: \def\replres{\rightarrow_{\mathcal R}}

94: \def\splres{\rightarrow_{spl}}

95: \def\ssplres{\rightarrow_{nspl}}

96: \def\predssplres{\rightarrow_{\sspreds-nspl}}

97: \def\epssplres{\rightarrow_{\epsilon-spl}}

98: \def\atordfsplres{\Rightarrow_{\atlt,\phi}}

99: \def\subordfsplres{\Rightarrow_{\sublt,\phi}}

100: \def\subordfsplreplres{\Rightarrow_{\sublt,\phi,\mathcal R}}

101: \def\atordfsplreplres{\Rightarrow_{\atlt,\phi,\mathcal R}}

102: \def\subordselfssplreplres{\Rrightarrow_{\sublt_s,\phi,\mathcal R}}

103: \def\subordselnosplreplres{\Rrightarrow_{\sublt_s,\phi_0,\mathcal R}}

104: \def\subordselfssplreplresh{\Rrightarrow_{\sublt_s,\phi_h,\mathcal R}}

105: \def\atordselfssplreplres{\Rrightarrow_{\atlt_s,\phi,\mathcal R}}

106: \def\atordres{\Rightarrow_{\atlt}}

107: \def\atordselres{\Rrightarrow_{\atlt_s}}

108: \def\absres{\blacktriangleright}

109: \def\absresh{{\blacktriangleright_h}}

110: 

111: \def\inst{\mathsf{I}}

112: \def\insti{\mathsf{I}_i}

113: \def\instone{\mathsf{I}_1}

114: \def\insttwo{\mathsf{I}_2}

115: \def\instthree{\mathsf{I}_3}

116: \def\instfour{\mathsf{I}_4}

117: \def\instko{\mathsf{I}_{k_1}}

118: \def\instkt{\mathsf{I}_{k_2}}

119: \def\proj{\pi}

120: \def\comp{\mathsf{comp}}

121: \def\eps{\mathsf{eps}}

122: \def\ov{\mathsf{ov}}

123: \def\ground{\mathsf{gr}}

124: \def\fv{\mathsf{fv}}

125: \def\sspreds{\mathcal Q}

126: \def\epspreds{\mathcal Q_1}

127: \def\grpreds{\mathcal Q_0}

128: \def\anypreds{\mathcal Q'}

129: \def\allclauses{\mathbb C}

130: \def\ssp#1{\overline{#1}}

131: \def\qrep#1{\underline{#1}}

132: \def\varset{{\bf X}}

133: \def\varone{{\bf x}_1}

134: \def\vartwo{{\bf x}_2}

135: \def\varthree{{\bf x}_3}

136: \def\varr{{\bf x}_r}

137: \def\varn{{\bf x}_n}

138: \def\varrone{{\bf x}_{r+1}}

139: \def\varrtwo{{\bf x}_{r+2}}

140: \def\varrthree{{\bf x}_{r+3}}

141: \def\varrr{{\bf x}_{2r}}

142: %\def\varrn{{\bf x}_{r+n}}

143: \def\vari{{\bf x}_i}

144: \def\varione{{\bf x}_{i_1}}

145: \def\varitwo{{\bf x}_{i_2}}

146: \def\varin{{\bf x}_{i_n}}

147: \def\varik{{\bf x}_{i_k}}

148: \def\varij{{\bf x}_{i_j}}

149: \def\varlione{{\bf x}_{i^l_1}}

150: \def\varlikl{{\bf x}_{i^l_{k_l}}}

151: \def\varlijl{{\bf x}_{i^l_{j_l}}}

152: \def\rvarset{{\bf X}_r}

153: \def\rpvarset{{\bf X'}_r}

154: 

155: \def\ngrr{\mathsf{Ngrr}}

156: \def\ngrone{\mathsf{Ngr_1}}

157: \def\ngr{\mathsf{Ngr}}

158: \def\ngs{\mathsf{Ngs}}

159: \def\ng{\mathsf{Ng}}

160: \def\gone{\mathsf{G_1}}

161: \def\g{\mathsf{G}}

162: \def\u{\mathsf{U}}

163: % Remove for camera-ready copy

164: %\pagestyle{plain}

165: 

166: \begin{document}

167: \title{Flat and One-Variable Clauses: Complexity of Verifying

168: Cryptographic Protocols with Single Blind Copying}

169: \author{Helmut Seidl \quad Kumar Neeraj Verma\\

170: Institut f\"ur Informatik, TU M\"unchen, Germany\\

171: {\tt \{seidl,verma\}@in.tum.de}}

172: 

173: \maketitle

174: 

175: \begin{abstract}

176: Cryptographic protocols with single blind copying were defined and

177: modeled by Comon and Cortier using the new class $\mathcal C$ of

178: first order clauses.  They showed its

179: satisfiability problem to be in 3-DEXPTIME.  We improve this result by

180: showing that satisfiability for this class is NEXPTIME-complete, using

181: new resolution techniques.  We show satisfiability to be DEXPTIME-complete

182: if clauses are Horn, which is what is required for modeling cryptographic

183: protocols. While translation to Horn clauses only gives a DEXPTIME upper

184: bound for the secrecy problem for these protocols, we further show that

185: this secrecy problem is actually DEXPTIME-complete.

186: \end{abstract}

187: 

188: %%% keywords: cryptographic protocols,  first order logic, horn clauses,

189: %%% ordered resolution, propositional satisfiability

190: 

191: 

192: 

193: 

194: \section{Introduction}

195: \label{sec:intro}

196: 

197: Several researchers have pursued modeling of cryptographic protocols using

198: first order clauses~\cite{Blanchet:prolog,comon:rta03,Weidenbach:crypto} 

199: and related formalisms like

200: tree automata and set constraints\cite{cc:tamem,glrv:jlap04,Monniaux:SAS99}.

201: While protocol insecurity is NP-complete in case of a bounded number of sessions

202: \cite{Turuani:np}, this is helpful only for detecting some attacks.

203: For certifying protocols, the number of sessions cannot be bounded, although

204: we may use other safe abstractions.

205: The approach using first order clauses

206: is particularly useful for this class of problems.

207: A common safe abstraction is to allow a bounded number of nonces, i.e.

208: random numbers, to be used in infinitely many sessions.

209: Security however

210: still remains undecidable~\cite{cc:tamem}. Hence further restrictions are 

211: necessary to obtain decidability. 

212: 

213: In this direction, Comon and Cortier~\cite{comon:rta03,cortier:thesis}

214: proposed the notion of protocols with single blind copying. 

215: Intuitively this restriction means that

216: agents are allowed to copy at most one piece of data blindly in any

217: protocol step, a restriction satisfied by most protocols in the literature. 

218: Comon and Cortier modeled the secrecy problem for these protocols using 

219: the new class $\c$ of first order clauses, 

220: and showed satisfiability for $\c$ to be 

221: decidable~\cite{comon:rta03} in 3-DEXPTIME~\cite{cortier:thesis}. 

222: The NEXPTIME lower bound is easy. We show in this paper

223: that satisfiability of this class is in NEXPTIME, thus NEXPTIME-complete. 

224: If clauses

225: are restricted to be Horn, which suffices for modeling of cryptographic

226: protocols,  we show that

227: satisfiability is DEXPTIME-complete (again the lower bound is easy).

228: While translation to clauses only gives a DEXPTIME upper bound for the

229: secrecy problem for this class of protocols, 

230: we further show that the secrecy problem for these protocols 

231: is also DEXPTIME-complete. 

232: 

233: For proving our upper bounds, we introduce several variants of

234: standard ordered resolution with selection and splitting~\cite{BG:HAR}.

235: Notably we consider resolution as consisting of instantiation of clauses, and

236: of generation of propositional implications. This is in the style 

237: of Ganzinger and Korovin~\cite{ganzinger:instantiation}, 

238: but we adopt a slightly different approach, and

239: generate interesting implications to obtain optimal complexity. 

240: More precisely, while the approach of~\cite{ganzinger:instantiation}, 

241: emphasizes a single phase of instantiation

242: followed by propositional satisfiability checking, we  interleave

243: generation of interesting instantiations and propositional implications in an

244: appropriate manner to obtain optimal complexity. 

245: We further show how this technique

246: can be employed also in presence of rules for replacement 

247: of literals in clauses,

248: which obey some ordering constraints. To deal with the notion of single blind

249: copying we show  how terms containing a single variable can be decomposed

250: into simple terms whose unifiers are of very simple forms. As byproducts,

251: we obtain optimal complexity for several subclasses of  $\c$, 

252: involving so called {\em flat} and {\em one-variable} clauses.

253: 

254: 

255: \noindent

256: {\bf Outline:}

257: We start in Section~\ref{sec:fol} by recalling basic notions about first order

258: logic and resolution refinements. In Section~\ref{sec:protocols} we introduce 

259: cryptographic protocols with single blind copying, discuss their

260: modeling using the class $\c$ of first order clauses, and show that their

261: secrecy problem is DEXPTIME-hard. To decide the class $\c$ we gradually

262: introduce our techniques by obtaining DEXPTIME-completeness and

263: NEXPTIME-completeness for one-variables

264: clauses and flat clauses in Sections~\ref{sec:onevar} and~\ref{sec:flat}

265: respectively.  In Section~\ref{sec:nh}, the

266: techniques from the two cases are combined with further ideas to show

267: that satisfiability for $\c$ is NEXPTIME-complete. In Section~\ref{sec:horn}

268: we adapt this proof to show that satisfiability for the Horn fragment of 

269: $\c$ is DEXPTIME-complete. 

270: 

271:  

272: 

273: \section{Resolution}

274: \label{sec:fol}

275: 

276: We recall standard notions from first order logic.

277: Fix a signature $\Sigma$ of function symbols each with a given arity, and 

278: containing at least one zero-ary symbol. 

279: Let $r$ be the maximal arity of function symbols in $\Sigma$.

280: Fix a set $\varset = \{\varone,\vartwo,\varthree,\ldots\}$ of variables.

281: Note that $\varone,\vartwo,\ldots$ (in bold face) are the actual elements of

282: $\varset$, where as $x,y,z,x_1,y_1,\ldots$ are used to represent arbitrary

283: elements of $\varset$. The set $T_{\Sigma}(\varset)$ of terms built from

284: $\Sigma$ and $\varset$ is defined as usual. 

285: $T_{\Sigma}$ is the set of {\em ground terms}, i.e. those not containing any 

286: variables. {\em Atoms} $A$ are of the form $P(t_1,\ldots,t_n)$ where $P$ is an 

287: $n$-ary predicate and $t_i$'s are terms. {\em Literals} $L$ are either positive 

288: literals $+ A$ (or simply $A$) or negative literals $- A$, where $A$ is an atom.

289: $-(-A)$ is another

290: notation for $A$.  $\pm$ denotes $+$ or $-$ and $\mp$ denotes the

291: opposite sign (and similarly for notations $\pm',\mp',\ldots$).

292: A {\em clause} is a finite set of literals.

293: A {\em negative clause} is one which contains only negative literals.

294: If $M$ is any term, literal or clause then

295: the set $\fv(M)$ of variables occurring in them is defined as usual.

296: If $C_1$ and $C_2$ are clauses then $C_1\lor C_2$ denotes $C_1\cup C_2$.

297: $C \lor \{L\}$ is written as $C \lor L$ (In this notation, we allow the

298: possibility of $L\in C$). If $C_1,\ldots,C_n$ are clauses such that

299: $\fv(C_i)\cap \fv(C_j)=\emptyset$ for $i\neq j$, and if $C_i$ is non-empty

300: for $i\ge 2$, then the clause $C_1 \lor \ldots\lor C_n$ is also written as 

301: $C_1 \sqcup \ldots \sqcup C_n$ to emphasize this property.

302:  {\em Ground literals and clauses} are ones not 

303: containing variables.

304: A term, literal or clause is {\em trivial} if it contains no

305: function symbols.

306: A substitution is a function $\sigma : \varset \rightarrow T_{\Sigma}(\varset)$.

307: {\em Ground substitutions} map every variable to a ground term.

308: We write $\sigma = \{x_1\mapsto t_1,\ldots,x_n\mapsto t_n\}$ to say that

309: $x_i\sigma = t_i$ for $1\le i\le n$ and $x\sigma = x$ for 

310: $x\notin\{x_1,\ldots,x_n\}$.

311: If $M$ is a term, literal, clause, substitution or set of such objects,

312: then the effect $M\sigma$ of

313: applying $\sigma$ to $M$ is defined as usual.

314: {\em Renamings} are bijections $\sigma : \varset \rightarrow \varset$. 

315: If $M$ is a term, literal, clause or substitution, 

316: then a renaming of $M$ is of the form

317: $M\sigma$ for some renaming $\sigma$, and an

318: instance of $M$ is of the form

319: $M\sigma$ for some substitution $\sigma$.

320: If $M$ and $N$ are terms or literals then a {\em unifier} of $M$ and $N$

321: is a substitution $\sigma$ such that $M\sigma = N\sigma$. 

322: If such a unifier exists then there is also a {\em most general unifier (mgu)},

323: i.e. a unifier $\sigma$ such that for every unifier $\sigma'$ of $M$ and $N$,

324: there is some $\sigma''$ such that $\sigma' = \sigma\sigma''$. Most

325: general unifiers are unique upto renaming: if $\sigma_1$ and $\sigma_2$ are

326: two mgus of $M$ and $N$ then $\sigma_1$ is a renaming of $\sigma_2$. Hence

327: we may use the notation $mgu(M,N)$ to denote one of them.

328: We write $M[x_1,\ldots,x_n]$ to say that $\fv(M) \subseteq \{x_1,\ldots,x_n\}$.

329: If $t_1,\ldots,t_n$ are terms then $M[t_1,\ldots,t_n]$ denotes 

330: $M \{x_1 \mapsto t_1, \ldots, x_n \mapsto t_n\}$.

331: If $N$ is a set of terms them $M[N] = \{M[t_1,\ldots,t_n] \mid

332: t_1,\ldots,t_n\in N\}$. If $M$ is a set of terms, atoms, literals or clauses

333: them $M[N] = \bigcup_{m\in M} m[N]$. A {\em Herbrand interpretation} 

334: $\mathcal H$ is a set of ground atoms. A clause $C$ is {\em satisfied} in 

335: ${\mathcal H}$ if for 

336: every ground substitution $\sigma$, either $A \in\mathcal H$ for

337: some  $A \in C\sigma$, or 

338: $A \notin {\mathcal H}$ for some $-A \in C\sigma$. 

339: A set $S$ of clauses is satisfied in $\mathcal H$ if every clause of $S$

340: is satisfied in $\mathcal H$.  If such a $\mathcal H$

341: exists then $S$ is {\em satisfiable}, and $\mathcal H$ is a {\em Herbrand model}

342: of $S$.

343: A {\em Horn clause} is one containing at most one positive literal. If a set

344: of Horn clauses is satisfiable then it has a least Herbrand model

345: wrt the subset ordering.

346: 

347: Resolution and its refinements are well known methods for

348:  testing satisfiability of clauses.

349: Given a strict partial order $\atlt$ on atoms, a literal

350: $\pm A$ is {\em maximal} in a clause $C$ if there is no literal

351: $\pm' B\in C$ with $A \atlt B$.

352: {\em Binary ordered resolution} and {\em ordered factorization} 

353: wrt ordering $\atlt$ are defined by the following two rules respectively: 

354: 

355: \[

356: %\begin{tabular}{|lr|}

357: %\hline

358: \prooftree

359: C_1\lor A \quad   - B \lor C_2

360: \justifies C_1\sigma \lor C_2\sigma

361: \endprooftree 

362: \quad\quad\quad\quad\prooftree

363: C_1 \lor \pm A \lor \pm B

364: \justifies C_1\sigma\lor A\sigma

365: \endprooftree

366: %\hline

367: %\end{tabular}

368: \]

369: 

370: \noindent

371: where $\sigma = mgu(A,B)$ in both rules,

372: $A$ and $B$ are maximal in the left and right premises 

373: respectively of the first rule, and

374: $A$ and $B$ are both maximal in the premise of the second rule.

375: We rename the premises of the first rule before resolution so that

376: they don't share variables.  The ordering

377: $\atlt$ is {\em stable} if: whenever $A_1 \atlt A_2$ then 

378: $A_1\sigma \atlt A_2\sigma$ for all substitutions $\sigma$.  We

379: write $S \atordres S \cup \{C\}$

380:  to say that $C$ is obtained by one application of

381: the binary ordered resolution or binary factorization rule on clauses in

382: $S$ (the subscript denotes the ordering used). 

383: %$R_1 R_2$ denotes the composition of two binary relations $R_1$ and $R_2$. 

384: 

385: Another resolution rule is 

386: {\em splitting}. This can be described using {\em tableaux}. A {\em tableau}

387: is of the form $S_1 \mid \ldots \mid S_n$, 

388: where $n\ge 0$ and each $S_i$, called a {\em branch} of the tableau,

389:  is a set of 

390: clauses (the $\mid$ operator is associative and commutative). 

391: A tableau is {\em satisfiable} if at least one of its branches is satisfiable.

392: The tableau

393: is called {\em closed} if each $S_i$ contains the empty clause, denoted

394: $\empcl$. The {\em splitting}

395: step on tableaux is defined by the rule $${\mathcal T} \mid S \splres

396: {\mathcal T} \mid (S \setminus \{C_1\sqcup C_2\}) \cup \{C_1\} \mid

397: (S \setminus \{C_1\sqcup C_2\}) \cup \{C_2\}$$ whenever $C_1\sqcup C_2 \in S$

398: and $C_1$ and $C_2$ are non-empty. $C_1$ and $C_2$ are called {\em components}

399:  of the clause $C_1 \sqcup C_2$ being split.

400: It is well known that splitting preserves satisfiability of tableaux.

401: We may choose to apply splitting eagerly,

402: or lazily or in some other fashion. Hence we define a {\em splitting strategy}

403: to be a function $\phi$ such that $\mathcal T \splres \phi(\mathcal T)$ for all

404: tableaux $\mathcal T$. 

405: The relation $\atordres$ is extended to tableaux as expected.

406: Ordered resolution with splitting strategy is then

407: defined by the rule $${\mathcal T}_1 \atordfsplres \phi({\mathcal T}_2)

408: \textrm{ whenever } {\mathcal T}_1 \atordres {\mathcal T}_2$$ 

409: This provides us with a well known

410: sound and complete method for testing satisfiability.

411: For any binary relation $R$,

412: $R^*$ denotes the reflexive transitive closure of $R$, and $R^+$ 

413: denotes the transitive closure of $R$. 

414: \begin{lemma}%[\cite{BG:HAR}]

415: \label{lemma:ordspl:compl}

416: For any set $S$ of clauses, for any stable ordering $\atlt$, and for

417: any splitting strategy $\phi$, $S$ is unsatisfiable iff

418: $S \atordfsplres^* \mathcal T$ for some closed $\mathcal T$.

419: \end{lemma}

420: 

421: 

422: If all predicates are zero-ary then the resulting clauses are

423: {\em propositional clauses}. In this case we write $S \pmodels T$ to say

424: that every Herbrand model of $S$ is a Herbrand model of $T$. This notation

425: will also be used when $S$ and $T$ are sets of first order clauses, by treating

426: every (ground or non-ground) atom as a zero-ary predicate.

427: For example $\{P(a),- P(a)\} \pmodels \empcl$ but $\{P(x),-P(a)\}\pnmodels

428: \empcl$.  $S\pmodels \{C\}$ is also written as $S\pmodels C$. If

429: $S\pmodels C$ then clearly

430: $S\sigma \pmodels C\sigma$ for all substitution $\sigma$.

431: 

432: 

433: \section{Cryptographic Protocols}

434: \label{sec:protocols}

435: 

436: We assume that $\Sigma$ contains the binary functions $\{\_\}_{\_}$ and

437: $\langle\_,\_\rangle$ 

438: denoting encryption and pairing. {\em Messages} are terms of

439: $T_{\Sigma}(\varset)$.

440: A {\em state} is of the form $S(M_1,\ldots,M_n)$ where $S$ with arity $n$

441: is from a finite set of {\em control points}

442: and $M_i$ are messages. It denotes an agent at control point $S$

443: with messages $M_i$ in its memory.  An {\em initialization state} is a

444: state not containing variables. We assume some strict partial order $<$ on the

445: set of control points. A {\em protocol rule} is of the form

446: $$S_1(M_1,\ldots,M_m):\mathsf{recv}(M) \rightarrow 

447: S_2(N_1,\ldots,N_n):\mathsf{send}(N)$$ where $S_1 < S_2$, $M_i,N_j$ are messages,

448: and $M$ and $N$ are each either a message, or a dummy symbol $?$ indicating

449: nothing is received (resp. sent). For secrecy analysis we can replace $?$

450: by some public message, i.e. one which is known to everyone including the

451: adversary.

452: The rule says that an agent in state

453: $S_1(M_1,\ldots,M_m)$ can receive message $M$, send a message $N$, and then

454: move to state $S_2(N_1,\ldots,N_n)$, thus also modifying the messages in

455: its memory. A {\em protocol} is a finite set of initialization states

456: and protocol rules. This model is in the style of~\cite{durgin:fmsp99} and

457: \cite{cc:tamem}. The assumption of single blind copying then says that

458: each protocol rule contains at most one variable (which may occur anywhere

459: any number of times in that rule). For

460: example, the public-key Needham-Schroeder protocol 

461: 

462: \[\begin{array}{r l}

463: \hspace*{1pt}

464: A \rightarrow B : & \{A,N_A\}_{K_B}\\

465: \hspace*{1pt}

466: B \rightarrow A : & \{N_A,N_B\}_{K_B}\\

467: \hspace*{1pt}

468: A \rightarrow B : & \{N_B\}_{K_B}

469: \end{array}\]

470: 

471: \noindent

472: is written in our notation as follows. 

473: For every pair of agents $A$ and $B$

474: in our system (finitely many of

475:  them suffice for finding all attacks

476: against secrecy~\cite{comon:esop03,comon:rta03}) we have two nonces

477: $N^1_{AB}$ and $N^2_{AB}$ to be used in sessions where $A$ plays the

478: initiator's role and $B$ plays the responder's role.

479: We have initialization states 

480: $\mathsf{Init_0}(A,N^1_{AB})$ and $\mathsf{Resp_0}(B,N^2_{AB})$ for all

481: agents $A$ and $B$.

482: Corresponding to the three lines in the protocol

483: we have rules for all agents $A$ and $B$

484: 

485: \[\begin{array}{r@{:}l@{\rightarrow}r@{:}l}

486: \mathsf{Init_0}(A,N^1_{AB}) &  \mathsf{recv}(?)  &  

487: \mathsf{Init_1}(A,N^1_{AB}) & \mathsf{send} (\{\langle A,N^1_{AB}

488: \rangle\}_{K_B})\\

489: \mathsf{Resp_0}(B,N^2_{AB}) &  \mathsf{recv}(\{\langle A,x\rangle\}_{K_B})

490:  &  \mathsf{Resp_1}(B,x,N^2_{AB}) &  \mathsf{send}(\{\langle x,N^2_{AB}\rangle\}_{K_A})\\

491: \mathsf{Init_1}(A,N^1_{AB})  &  \mathsf{recv}(\{\langle N^1_{AB},x\rangle\}_{K_A})

492:  & \mathsf{Init_2}(A,N^1_{AB},x)  &  \mathsf{send}(\{x\}_{K_B})\\

493: \mathsf{Resp_1}(B,x,N^2_{AB}) & \mathsf{recv}(\{N^2_{AB}\}_{K_B})  & 

494: \mathsf{Resp_2}(B,x,N^2_{AB})  &  \mathsf{send}(?) 

495: \end{array}\]

496: 

497: 

498: 

499: Any initialization state can be created any number of times and any 

500: protocol rule can be executed any number of times. The adversary has

501: full control over the network: all messages received by agents are

502: actually sent by the adversary and all messages sent by agents are

503: actually received by the adversary. The adversary can obtain

504: new messages from messages he knows, e.g. by performing encryption

505: and decryption.  To model this using Horn

506: clauses, we create a unary predicate $\reach$ to model reachable

507: states, and a unary predicate $\known$ to model messages known to the

508: adversary. The initialization state $S(M_1,\ldots,M_n)$

509: is then modeled by the clause

510: $\reach(S(M_1,\ldots,M_n))$, where $S$ is a new function symbol we create.

511: The protocol rule 

512: $$S_1(M_1,\ldots,M_m):\mathsf{recv}(M) \rightarrow

513: S_2(N_1,\ldots,N_n):\mathsf{send}(N)$$

514: is modeled by the clauses

515: $$\begin{array}{c}\known(N) \lor - \reach(S_1(M_1,\ldots,M_m)) \allowbreak

516: \lor \allowbreak - \known(M) \\

517: \reach(S_2(N_1,\ldots,N_n)) \allowbreak \lor \allowbreak - \reach(\allowbreak S_1(\allowbreak M_1,\allowbreak \ldots,\allowbreak M_m)) \allowbreak \lor \allowbreak -

518: \known(M)\end{array}$$

519: Under the assumption

520: of single blind copying it is clear that all these clauses are {\em 

521: one-variable clauses}, i.e. clauses containing at most one variable. 

522:  We need further clauses to express adversary capabilities. 

523: The clauses 

524: $$\begin{array}{c}

525: \known(\{\varone\}_{\vartwo}) \lor - \known(\varone)\lor - \known(\vartwo)\\

526: \known(\varone) \lor - \known(\{\varone\}_{\vartwo}) \lor - \known(\vartwo)

527: \end{array}$$

528:  express the encryption

529: and decryption abilities of the adversary. We have similar clauses for

530: his pairing and unpairing abilities, as well as clauses

531: $$\known(\allowbreak f\allowbreak (\allowbreak \varone\allowbreak ,\allowbreak \ldots\allowbreak ,\allowbreak \varn\allowbreak )\allowbreak ) \lor - \known(\varone)\lor \ldots \lor -

532: \known(\varn)$$

533:  for any function $f$ that the adversary knows to apply. All these

534: are clearly {\em flat clauses}, i.e. clauses of the form

535: $$C=\bigvee_{i=1}^k \pm_i P_i(f_i(x^i_1,\ldots,x^i_{n_i})) \lor

536: \bigvee_{j=1}^l \pm_j Q_j(x_j)$$

537: where $\{x^i_1,\ldots,x^i_{n_i}\} = \fv(C)$ for $1\le i\le k$.

538: Asymmetric keys, i.e. keys $K$ such that message $\{M\}_K$ can only be decrypted

539: with the inverse key $K^{-1}$,  are also easily dealt with using flat and 

540: one-variable clauses.

541: The adversary's knowledge of other data $c$

542: like agent's names, public keys, etc are expressed by clauses $\known(c)$.

543: Then the least Herbrand model of this set of clauses describes exactly the

544: reachable states and the messages known to the adversary. Then to check whether

545: some message $M$ remains secret, we add the clause

546: $ - \known(M)$ and check whether the resulting set is satisfiable.

547: 

548: 

549: A set of clauses is in the class $\onevar$ if each of its members is a

550: one-variable clause. 

551: A set of clauses is in the class $\flat$ if each of its members is a

552: flat clause. More generally we have the class 

553: $\c$ proposed by Comon and Cortier~\cite{comon:rta03,cortier:thesis}: 

554: a set of clauses $S$ is in the class $\c$ if for each $C\in S$ one of the

555: following conditions is satisfied.

556: \begin{enumerate}

557: \item $C$ is a one-variable clause

558: \item $C=\bigvee_{i=1}^k \pm_i P_i(u_i[f_i(x^i_1,\ldots,x^i_{n_i})]) \lor

559: \bigvee_{j=1}^l \pm_j Q_j(x_j)$,

560: where for  $1\le i\le k$ we have $\{x^i_1,\ldots,x^i_{n_i}\} = \fv(C)$ and

561: $u_i$ contains at most one variable.

562: \end{enumerate}

563: If all clauses are Horn then we have the corresponding classes

564: $\onevarh$, $\flath$ and $\ch$. 

565: Clearly the classes $\onevar$ (resp. $\onevarh$) and $\flat$ (resp. 

566: $\flath$) are included in the class $\c$ (resp.

567: $\ch$) since the $u_i$'s above can be trivial.

568: Conversely any clause set in $\c$ can be considered as containing just

569: flat and one-variable clauses. This is because we can replace a clause

570: $C \lor \pm P(u[f(x_1,\ldots,x_n)])$ by the clause

571: $C \lor \pm Pu(f(x_1,\ldots,x_n))$ and add clauses

572: $ - Pu(x) \lor P(u[x])$ and $Pu(x) \lor  - P(u[x])$ where $Pu$ is a

573: fresh predicate. This transformation takes polynomial time and preserves

574: satisfiability of the clause set.  Hence now we 

575: need to deal with just flat and one-variable clauses.

576: In the rest of the paper we derive optimal complexity results

577: for all these classes.

578: 

579: Still this  only gives us an upper bound for the secrecy problem of 

580: protocols since the clauses could be more general than necessary.

581: It turns out, however, that this is not the case. In order to show this

582: we rely on a reduction of 

583: the reachability problem for {\em alternating pushdown systems (APDS)}. 

584: In form of Horn clauses, an {\em APDS} is a finite 

585: set of clauses of the form 

586: \begin{enumerate}

587: \item[(i)] $P(a)$ where $a$ is a zero-ary symbol

588: \item[(ii)] $P(s[x])\lor - Q(t[x])$ where $s$ and $t$ involve only unary function 

589: symbols, and

590: \item[(iii)] $P(x) \lor - P_1(x) \lor - P_2(x)$

591: \end{enumerate}

592:  Given any set $S$ of {\em definite}

593: clauses (i.e. Horn clauses having some positive literal),

594: a ground atom $A$ is {\em reachable} if $A$ is in the least

595: Herbrand model of $S$, i.e. if $S \cup

596: \{ - A\}$ is unsatisfiable. Reachability in APDS is

597: DEXPTIME-hard~\cite{kozen:alternation}. 

598: We encode this problem into secrecy of protocols, 

599: as in~\cite{durgin:fmsp99}. 

600: Let $K$ be a (symmetric) key not known to the adversary.

601: Encode atoms $P(t)$ as messages $\{\langle P,t\rangle\}_K$, by treating

602: $P$ as some data. 

603: Create initialization states $S_1$ and $S_2$ 

604: (no message is stored in the states).

605: Clauses (i-iii) above are translated as 

606: $$\begin{array}{l l l}

607: S_1: & \mathsf{recv}(?) & \rightarrow S_2:\mathsf{send}(\{\langle P,a\rangle\}_K)\\

608: S_1: & \mathsf{recv}(\{\langle Q,t[x]\rangle\}_K) \allowbreak & \rightarrow \allowbreak S_2:\mathsf{send}(\{\langle P,s[x]\rangle\}_K)\\

609: S_1: & \mathsf{recv}\allowbreak (\allowbreak \langle \allowbreak \{\allowbreak \langle \allowbreak P_1\allowbreak ,\allowbreak x\allowbreak \rangle\allowbreak \}_K,\{\allowbreak \langle \allowbreak P_2\allowbreak ,\allowbreak x\allowbreak \rangle\}_K\rangle) 

610: & \rightarrow S_2:\mathsf{send}(\{\langle P,x\rangle\}_K)

611: \end{array}$$

612: The intuition is that the adversary cannot decrypt messages encrypted with

613: $K$. He also cannot encrypt messages with $K$. He can only forward messages

614: which are encrypted with $K$. However he has the ability to pair messages.

615: This is utilized in the translation of clause (iii). Then a message

616: $\{M\}_K$ is known to the adversary iff $M$ is of the form $\langle P,t\rangle$ 

617: and $P(t)$ is reachable in the APDS.

618: \begin{theorem}

619: \label{th:hardness}

620: Secrecy problem for cryptographic protocols with single blind copying,

621: with bounded number of nonces but unbounded number of sessions is 

622: DEXPTIME-hard, even if no message is allowed to be stored at any control point.

623: \end{theorem} 

624: 

625: \section{One Variable Clauses: Decomposition of Terms}

626: \label{sec:onevar}

627: 

628: 

629: We first show that satisfiability for the classes $\onevar$ and $\onevarh$ is 

630: DEXPTIME-complete.  We recall also that although we consider only unary 

631: predicates, this is no restriction in the case of one-variable clauses, 

632: since we can encode atoms $P(t_1,\ldots,t_n)$ as

633: $P'(f_n(t_1\ldots,t_n))$ for fresh $P'$ and $f_n$ for every $P$ of arity $n$.

634: As shown in~\cite{comon:rta03,cortier:thesis}, ordered

635: resolution on one-variable clauses, for a suitable ordering,

636:  leads to a linear bound on the height of

637: terms produced. This does not suffice for obtaining a DEXPTIME upper bound 

638: and we need to examine the forms of unifiers

639: produced during resolution. We consider terms containing at most one variable

640: (call them {\em one-variable terms}) to be compositions of

641: simpler terms.

642: A non-ground one-variable term $t[x]$ is called {\em reduced} if it is not of 

643: the form $u[v[x]]$ for any non-ground non-trivial one-variable terms $u[x]$ 

644: and $v[x]$. The term $f(g(x),h(g(x)))$ for example

645: is not reduced because it can be written

646: as $f(x,h(x))[g(x)]$. The term $f'(x,g(x),a)$ is reduced. Unifying it with the

647: reduced term $f'(h(y),g(h(a)),y)$ produces ground unifier $\{x\mapsto h(y)[a],

648: y\mapsto a\}$ and both $h(y)$ and $a$ are strict subterms of the given terms.

649: Indeed we find:

650: 

651: 

652: \newcounter{lemsxtyred}

653: \namelem{lemsxtyred}

654: \def\lemsxtyredstatement{

655: Let $s[x]$ and $t[y]$ be reduced, non-ground and non-trivial terms

656: where $x\neq y$ and $s[x] \neq t[x]$. 

657: If $s$ and $t$ have a unifier $\sigma$ then

658: $x\sigma, y\sigma \in U[V]$ where $U$ is the set of non-ground

659: (possibly trivial) strict subterms of $s$ and $t$, and $V$ is the set of ground 

660: strict subterms of $s$ and $t$.

661: }

662: \begin{lemma}

663: \label{lemma:sxty:red}

664: \lemsxtyredstatement

665: \end{lemma}

666: \proof

667: See Appendix~\ref{appone}.

668: 

669: In case both terms (even if not reduced) have the same variable

670: we have the following easy result: 

671: \newcounter{lemsxtx}

672: \namelem{lemsxtx}

673: \def\lemsxtxstatement{

674: Let $\sigma$ be a unifier of two non-trivial,

675: non-ground and distinct one-variable terms $s[x]$ and $t[x]$. Then 

676: $x\sigma$ is a ground strict subterm of $s$ or of $t$.

677: }

678: \begin{lemma}

679: \label{lemma:sxtx}

680: \lemsxtxstatement

681: \end{lemma}

682: \proof

683: See Appendix~\ref{appone}.

684: 

685: 

686: In the following one-variable clauses are simplified to

687: involve only reduced terms.

688: \newcounter{lemdecomp}

689: \namelem{lemdecomp}

690: \def\lemdecompstatement{

691: Any non-ground one-variable term $t[x]$ can be uniquely written as

692: $t[x] = t_1[t_2[\ldots[t_n[x]]\ldots]]$ where $n\ge 0$ and each $t_i[x]$ is

693: non-trivial, non-ground and reduced. This decomposition

694: can be computed in time polynomial in the size of $t$.

695: }

696: \begin{lemma}

697: \label{lemma:decomp}

698: \lemdecompstatement

699: \end{lemma}

700: \proof 

701: We represent $t[x]$ as a DAG by doing maximal sharing of subterms.

702: If $t[x]=x$ then the result is trivial. Otherwise

703: let $N$ be the position in this graph, other than the root node,

704:  closest to the root such that 

705: $N$ lies on every path from the root to the node corresponding to the

706: subterm $x$. 

707: Let $t'$ be the strict subterm of $t$ at position $N$ and

708: let $t_1$ be the term obtained from $t$ by replacing the sub-DAG at $N$

709: by $x$. Then $t=t_1[t']$ and $t_1$ is reduced.

710: We then recursively decompose $t'$.

711: 

712: Uniqueness of decomposition follows from Lemma~\ref{lemma:sxty:red}.\qed

713: \endproof 

714: 

715: Above  and elsewhere, if $n=0$ then

716: $t_1[t_2[\ldots[t_n[x]]\ldots]]$ denotes $x$.

717: Now if a clause set contains a clause 

718: $C = C' \lor \pm P(t[x])$, with $t[x]$ being non-ground,

719: if $t[x] = t_1[\ldots[t_n[x]]\ldots]$

720: where each $t_i$ is non-trivial and reduced, then we 

721: create fresh predicates $Pt_1\ldots t_i$ for $1\le i\le n-1$ and replace $C$

722: by the clause $C' \lor \pm Pt_1\ldots t_{n-1}(t_n[x])$. 

723: Also we add clauses

724: $Pt_1\ldots t_i(t_{i+1}[x]) \lor - Pt_1\ldots t_{i+1}(x)$ and

725: $ - Pt_1\ldots t_i(t_{i+1}[x]) \allowbreak \lor \allowbreak Pt_1\ldots t_{i+1}\allowbreak (\allowbreak x\allowbreak )$ 

726: for $0\le i \le n-2$ to our clause set. 

727: Note that the predicates $Pt_1\ldots t_i$ are considered invariant under

728: renaming of terms $t_j$. For $i=0$, $Pt_1\ldots t_i$ is same as $P$. 

729: Our transformation preserves satisfiability of the clause set. 

730: By Lemma~\ref{lemma:decomp} this takes polynomial time and eventually all

731: non-ground literals in clauses are of the form $\pm P(t)$ with reduced $t$.

732: Next if the clause set is of the form $S\cup\{C_1\cup C_2\}$, 

733: where $C_1$ is non-empty and has only ground literals, and $C_2$ is non-empty

734: and has only non-ground literals,

735: then we do splitting to produce $S\cup\{C_1\}\mid S\cup \{C_2\}$.

736: This process produces at most exponentially many branches each of which 

737: has polynomial size. Now it suffices to decide satisfiability of each branch in

738: DEXPTIME. Hence now we assume that each clause is either:\\

739: \hspace*{7pt}

740: ({\bf Ca}) a ground clause, or\\

741: \hspace*{7pt}

742: ({\bf Cb}) a clause containing exactly one variable,

743: each of whose literals is of the form

744:       $\pm P(t[x])$ where $t$ is non-ground and reduced.\\

745: Consider a set  $S$ of clauses of type Ca and Cb. We show how to decide

746: satisfiability of the set $S$. Wlog we assume that all clauses in $S$ of type

747: Cb contain the variable $\varone$.

748: Let $\ng$ be the set of non-ground terms $t[\varone]$ occurring as arguments in 

749: literals in $S$. 

750: Let $\ngs$ be the set of non-ground subterms $t[\varone]$ of terms in $\ng$.

751: We assume that $\ng$ and $\ngs$ always contain the trivial term $\varone$,

752: otherwise we add this term to both sets.

753: Let $\g$ be the set of ground subterms of terms occurring as arguments in

754: literals in $S$. The sizes of $\ng,\ngs$ and $\g$ are polynomial.

755: Let $S^\dag$ be the set of clauses of type Ca and Cb 

756: which only contain literals of the form 

757: $\pm P(t)$ for some $t\in \ng\cup \ng[\ngs[\g]]$ (observe that $\g \subseteq

758: \ngs[\g] \subseteq \ng[\ngs[\g]]$). The size of $S^\dag$ is at most exponential.

759: 

760: For resolution we use ordering $\sublt$: $P(s) \sublt Q(t)$ iff $s$ is a

761: strict subterm of $t$. We call $\sublt$ the subterm ordering without

762: causing confusion. This is clearly stable. 

763: This is the ordering that we are going to use throughout this

764: paper. 

765: In particular this means that if a clause contains literals $\pm P(x)$ and

766: $\pm' Q (t)$ where $t$ is non-trivial and contains $x$, then we cannot 

767: choose the literal $\pm P(x)$ to resolve upon in this clause.

768: Because of the simple form of unifiers of reduced terms we have:

769: 

770: 

771: \newcounter{lemovresol}

772: \namelem{lemovresol}

773: \def\lemovresolstatement{

774: Binary ordered resolution and ordered factorization, wrt the subterm

775: ordering, on clauses in $S^\dag$ produces clauses which are

776: again in $S^\dag$ (upto renaming). 

777: }

778: \begin{lemma}

779: \label{lemma:ovresol}

780: \lemovresolstatement

781: \end{lemma}

782: \proof  

783: Factorization on a ground clause doesn't produce any new clause.

784: Now suppose we factorize the non-ground clause $C[\varone]

785: \lor \pm P(s[\varone])\lor \pm P(t[\varone])$ 

786: to produce the clause $C[\varone]\sigma\lor \pm P(s[\varone])\sigma$ where

787: $\sigma=mgu(s[\varone],t[\varone])$. If the premise has only trivial literals

788: then factorization is equivalent to doing nothing. Otherwise by ordering

789: constraints, $s$ and $t$ are non-trivial.

790: By Lemma~\ref{lemma:sxtx} either $s[\varone]=t[\varone]$ in which case

791: factorization does nothing,

792: or $\varone\sigma$ is a ground subterm of $s[\varone]$ or of $t[\varone]$. 

793: In the latter case all literals in $(C[\varone]\lor P(s[\varone])\sigma$ 

794: are of the form $\pm' Q(t'[\varone]\sigma))$ where $t'[\varone]\in \ng$ 

795: and $\varone\sigma\in \g\subseteq \ngs[\g]$.

796: 

797: Now we consider binary resolution steps.

798: We have the following cases:

799: \begin{itemize}

800: \item If both clauses are ground then the result is clear.

801: 

802: \item Now consider both clauses $C_1[\varone]$ and 

803: $C_2[\varone]$ to be non-ground. Before resolution we rename

804: the second clause to obtain $C_2[\vartwo]$.

805: Clearly all literals in $C_1[\varone]$ and $C_2[\varone]$ are of the form

806: $\pm Q(u[\varone])$ where $u[\varone]\in \ng$.  

807: Let $C_1[\varone] = C'_1[\varone] \lor P(s[\varone])$ and 

808: $C_2[\vartwo] = - P(t[\vartwo]) \lor C'_2[\vartwo]$ 

809: where $P(s[\varone])$ and $-P(t[\vartwo])$ are the literals

810: to be resolved upon in the respective clauses.

811: If $s[\varone]$ and $t[\vartwo]$ are unifiable then from

812: Lemma~\ref{lemma:sxty:red}, one of the following cases hold:

813: 

814: \begin{itemize}

815: \item $s[\varone] = \varone$ (the case where $t[\vartwo] = \vartwo$

816: is treated similarly). From the definition of $\sublt$,

817: for $P(s[\varone])$ to be chosen for resolution,

818: all literals in $C'_1[\varone]$ are of the form $\pm Q(\varone)$.

819: The resolvent is $C[\vartwo] = C'_1[\varone]\sigma \cup C'_2$,

820: where $\sigma = \{\varone \mapsto t[\vartwo]\}$.

821: Each literal in $C'_1[\varone] \sigma$ is of the form 

822: $\pm Q(t[\vartwo])$ and each 

823: literal in $C'_2[\vartwo]$ is of the form $\pm Q(t'[\vartwo])$ where 

824: $t'\in \ng$. Hence $C[\varone] \in S^\dag$.

825: 

826: \item $s[\varone] = t[\varone]$. Then the resolvent is $C'_1[\varone]\lor

827: C'_2[\varone]$. 

828: 

829: \item $s[\varone]$ and $t[\vartwo]$ have a mgu $\sigma$ such that 

830:       $\varone\sigma, \vartwo\sigma \in \ngs[\g]$.

831:       The resolvent $C'_1[\varone]\sigma \lor C'_2[\vartwo]\sigma$ 

832:       has only ground atoms of the form $\pm Q(t')$ where $t'\in \ng[\ngs[\g]]$.

833: \end{itemize}

834: 

835: \item Now let the first clause $C_1[\varone]=C'_1[\varone]\lor \pm 

836: P(t[\varone])$ be non-ground, and the second clause $C_2 = \mp P(s) \lor C'_2$ 

837: be ground with $\pm P(t[\varone])$ and $\mp P(s)$ being the

838: respective literals chosen from $C_1[\varone]$ and $C_2$ for resolution.

839: All literals in $C_1[\varone]$ are of the form $\pm' Q(t'[\varone])$ 

840: with $t'\in \ng$.  All literals in $C_2$ are of the

841: form $\pm' Q(t')$ with $t'\in \ng[\ngs[\g]]$. 

842: Suppose that $s$ and $t[\varone]$ do unify.

843: We have the following cases:

844: \begin{itemize}

845: \item $s\in \ngs[\g]$. Then the resolvent $C = 

846: C'_1[\varone]\sigma \cup C'_2$ where $\sigma = \{\varone\mapsto g\}$ 

847: where $g$ is subterm of $s$. As $s\in \ngs[\g]$ hence

848: $g\in \ngs[\g]$. Hence all literals in $C'_1[\varone]\sigma$ are of

849: the form $\pm Q(t')$ where $t'\in \ng[\ngs[\g]]$. Hence $C \in S^\dag$.

850: 

851: \item

852: Now suppose $s\in \ng[\ngs[\g]]\setminus \ngs[\g]$. 

853: We must have $s = s_1[s_2]$ for some non-trivial $s_1[\varone] \in \ng$ and

854: some $s_2\in \ngs[\g]$.

855: This is the interesting case which shows why the

856: terms remain in the required form during resolution. 

857: The resolvent is

858: $C = C'_1[\varone]\sigma \lor C'_2$ where $\sigma=\{\varone\mapsto g\}$

859: is the mgu of $t[\varone]$ and $s$ for some ground term $g$.

860: As $t[g] = s_1[s_2]$, $\sigma_1 = \{\varone\mapsto g,\vartwo\mapsto s_2\}$ 

861: is a unifier of the terms $t[\varone]$ and $s_1[\vartwo]$. 

862: By Lemma~\ref{lemma:sxty:red} we have the following cases:

863: \begin{itemize}

864: \item $t[\varone]=\varone$, so that $g=s\in \ng[\ngs[\g]]$. By definition

865: of $\sublt$, for $\pm P(t[\varone])$ to be chosen for resolution, 

866: all literals in $C_1[\varone]$ must be of the form $\pm' Q(\varone)$. 

867: Hence all literals in $C'_1\sigma$ are of the

868: form $\pm' Q(g)$.  Hence $C \in S^\dag$.

869: 

870: \item $t[\varone] = s_1[\varone]$.

871: Then $g = s_2\in \ngs[\g]$.

872: Hence all literals in $C'_1\sigma$ are of the form

873: $\pm' Q(t'[g])$ where $t'[\varone]\in \ng$. Hence $C \in S^\dag$.

874: 

875: \item $g=\varone\sigma\in \ngs[\g]$. 

876: Hence all literals in $C'_1\sigma$ are of the form

877: $\pm' Q(t'[g])$ where $t'\in \ng$. Hence $C \in S^\dag$.

878: \qed

879: 

880: \end{itemize} 

881: \end{itemize}

882: \end{itemize}

883: \endproof 

884: 

885: Hence to decide satisfiability of $S \subseteq S^\dag$, we keep 

886: generating new clauses of $S^\dag$ by doing ordered binary resolution and 

887: ordered factorization wrt the subterm ordering till no new clause 

888: can be generated, 

889: and then check whether the empty clause has been produced. Also recall

890: that APDS consist of Horn one-variable clauses. Hence:

891: \begin{theorem}

892: \label{theorem:onevar}

893: Satisfiability for the classes $\onevar$ and

894: $\onevarh$ is DEXPTIME-complete.

895: \end{theorem}

896: 

897: 

898: \section{Flat Clauses: Resolution Modulo Propositional Reasoning}

899: \label{sec:flat}

900: 

901: Next we show how to decide the class $\flat$ of flat clauses in NEXPTIME.

902: This is well known when the maximal arity $r$ is a constant, or when all

903: non-trivial literals in a clause have the same {\em sequence}

904:  (instead of the same 

905: {\em set}) of variables.  But we are not aware of a proof of NEXPTIME upper

906: bound in the general case. We show how to obtain 

907: NEXPTIME upper bound in the general

908: case, by doing resolution modulo propositional reasoning.

909: While this constitutes an interesting result of its own,

910: the techniques allow us  to deal with the full class $\c$ efficiently.

911: Also this shows that the generality of the class $\c$ does

912: not cost more in terms of complexity.

913: An {\em $\epsilon$-block} is a one-variable clause which contains only

914: trivial literals. A complex clause $C$ is a flat clause

915: $\bigvee_{i=1}^k \pm_i P_i(f_i(x^i_1,\ldots,x^i_{n_i})) \lor

916: \bigvee_{j=1}^l \pm_j Q_j(x_j)$ in which $k\ge 1$. Hence a flat clause is either

917: a complex clause, or an 

918: {\em $\epsilon$-clause} which is defined to be a disjunction of 

919: $\epsilon$-blocks, i.e. to be  of the form 

920: $B_1[x_1] \sqcup \ldots \sqcup  B_n[x_n]$ where each $B_i$ is an 

921: $\epsilon$-block. $\epsilon$-clauses are difficult to deal with, hence we

922: split them to produce $\epsilon$-blocks.

923: Hence define {\em $\epsilon$-splitting} as the restriction of the splitting rule

924: in which one of the components is an $\epsilon$-block.

925: 

926: Recall that $r$ is the maximal arity of symbols in $\Sigma$. 

927: Upto renaming, any complex clause $C$ is such that

928: $\fv(C) \subseteq \rvarset = \{\varone,\ldots,\varr\}$, and 

929: any $\epsilon$-block $C$ is such that $\fv(C) \subseteq \{\varrone\}$.

930: The choice of $\varrone$ is not crucial. Now notice that

931: ordered resolution between complex clauses and $\epsilon$-blocks only 

932: produces flat

933: clauses, which can then be split to be left with only complex and

934: $\epsilon$-blocks. E.g. 

935: Resolution between $$P_1(\varone) \lor -P_2(\vartwo) 

936: \lor P_3(f(\varone,\vartwo)) \lor -P_4(g(\vartwo,\varone))$$ and

937: $$P_4(g(\varone,\varone)) \lor -P_5(h(\varone)) \lor P_6(\varone)$$ produces 

938: $$P_1(\varone) \lor -P_2(\varone) \lor P_3(f(\varone,\varone))

939: \lor -P_5(h(\varone)) \lor P_6(\varone)$$ 

940: %Resolution between $P_1(\varrone) \lor P_2(\varrone)$ and $-P_2(h(\varone)) 

941: %\lor P_3(\varone)$ produces $P_1(h(\varone)) \lor P_3(\varone)$. 

942: %Resolution between

943: %$P_1(\varrone) \lor P_2(\varrone)$ and $-P_2(\varrone) \lor P_3(\varrone)$

944: %produces $P_1(\varrone) \lor P_3(\varrone)$.

945: Resolution between $$P_2(\varrone) \quad\textrm{ and }\quad

946: -P_2(f(\varone,\vartwo)) \lor P_3(\varone) \lor P_4(\vartwo)$$ produces

947: $P_3(\varone) \lor P_4(\vartwo)$ which can then be split. The point is that

948: we always choose a non-trivial literal from a clause for resolution, if there

949: is one. As there are finitely many complex clauses and $\epsilon$-blocks this gives

950: us a decision procedure. Note however that the number of complex clauses

951: is doubly exponential. This is because we allow clauses of the form

952: $P_1(f_1(\varone,\varone,\vartwo)) \lor P_2(f_2(\vartwo,\varone)) \lor

953: P_3(f_3(\vartwo,\varone,\vartwo)) \lor ...$, i.e. the nontrivial terms

954: contain arbitrary number of repetitions of  variables in arbitrary order.

955: The number of such variable sequences of $r$ variables is exponentially

956: many, hence the number of clauses is doubly exponential. Letting

957: the maximal arity $r$ to be a constant, or forcing all 

958: non-trivial literals in a clause

959: to have the same variable sequence would have produced only exponentially

960: many clauses. In presence of splitting, this would have given us the well-known

961: NEXPTIME upper bound, which is also optimal. 

962: But we are not aware of a proof of NEXPTIME upper

963: bound in the general case. To obtain NEXPTIME upper bound

964: in the general case we introduce the technique of

965: resolution modulo propositional reasoning.

966: 

967: 

968: 

969: %Let $\rvarset = \{\varone,\ldots,\varr\}$. 

970: %Let $\subst_r$ be the set of all substitutions

971: %$\sigma$ such that $\sigma(\rvarset) \subseteq \rvarset$ and such that

972: %$x \sigma = x$ for $x\notin \rvarset$.

973: For a clause $C$, define the set of its projections as

974: $\proj(C) = C[\rvarset]$. Essentially projection involves making certain

975: variables in a clause equal. As we saw, resolution between two complex clauses

976: amounts to propositional resolution between their projections.

977: Define the set $\u = \{f(x_1,\ldots,x_n) \mid f \in \Sigma

978: \textrm{ and each }x_i\in\rvarset\}$ of size exponential in $r$.

979: Resolution between $\epsilon$-block $C_1$ and a good

980: complex clause  $C_2$ amounts to

981: propositional resolution of a clause from $C[\u]$ with $C_2$. Also

982: note that propositional resolution followed by further projection is 

983: equivalent to projection followed by propositional resolution.  Each complex

984: clause has exponentially many projections. This suggests that we can

985: compute beforehand the exponentially many projections of complex clauses and

986: exponentially many instantiations of $\epsilon$-blocks. All new complex clauses

987: generated by propositional resolution are ignored.

988: But after several such propositional resolution steps, we may get an 

989: $\epsilon$-clause, which should then be split and instantiated and used for

990: obtaining further propositional resolvents. 

991: In other words we only compute such

992: propositionally implied $\epsilon$-clauses, do splitting and instantiation and

993: iterate the process. This generates all resolvents upto propositional

994: implication. 

995: %The difference from the approach of

996: %Ganzinger and Korovin~\cite{ganzinger:instantiation} is that they

997: % have a

998: %single phase of instantiation followed by propositional satisfiability checking.

999: %In contrast, we compute certain interesting propositional implications which are

1000: %further instantiated, and iterate the process.

1001: We now formalize our approach.

1002: We start with the following observation which 

1003: is used in this and further sections.

1004: 

1005: \begin{lemma}

1006: \label{lemma:sequnif}

1007: Let $x_1,\ldots,x_n,y_1,\ldots,y_n$ be variables, not necessarily distinct,

1008: but with $\{x_1,\ldots,x_n\} \cap \{y_1,\ldots,y_n\} = \emptyset$.

1009: Then the terms $f(x_1,\ldots,x_n)$ and

1010: $f(y_1,\ldots,y_n)$ have an mgu $\sigma$ such that

1011: $\{x_1,\ldots,x_n\}\sigma \subseteq \{x_1,\ldots,x_n\}$

1012: and $y_i\sigma = x_i\sigma$ for $1\le i\le n$.

1013: \end{lemma}

1014: 

1015: 

1016: 

1017: For a set $S$ of clauses, $\comp(S)$ is the set of complex clauses in $S$,

1018:  $\eps(S)$ the set of $\epsilon$-blocks in $S$,

1019: $\proj(S) = \bigcup_{C\in S} \proj(C)$ and

1020: $\inst(S) = \proj(\comp(S)) \cup \eps(S)[\varrone] \cup \eps(S)[\u]$. 

1021: For sets $S$ and $T$ of complex clauses and $\epsilon$-blocks,

1022: $S \abs T$ means that:\\

1023: -- if $C\in S$ is a complex clause then $\inst(T) \pmodels \proj(C)$, and\\

1024: -- if $C\in S$ is an $\epsilon$-block then $C[\varrone] \in \eps(T)[\varrone]$.\\

1025: For tableaux ${\mathcal T}_1$ and ${\mathcal T}_2$ involving only complex clauses and

1026: $\epsilon$-blocks we write ${\mathcal T}_1 \abs {\mathcal T}_2$ if

1027: ${\mathcal T}_1$ can be written as $S_1 \mid \ldots \mid S_n$ 

1028: and ${\mathcal T}_2$

1029: can be written as $T_1 \mid \ldots \mid T_n$ (note same $n$)

1030: such that $S_i \abs T_i$ for $1\le i\le n$. Intuitively 

1031: ${\mathcal T}_2$ is a succinct representation of ${\mathcal T}_1$.

1032: Define the splitting strategy $\phi$ as the one which repeatedly

1033: applies $\epsilon$-splitting on a tableau as long as possible. The

1034: relation $\subordfsplres$ provides us a sound and complete method for

1035: testing unsatisfiability.

1036: We define the alternative procedure for testing unsatisfiability by using

1037: succinct representations of tableaux.  We define $\absres$ by the rule:

1038: $\mathcal T \mid S \absres \mathcal T \mid S \cup \{B_1\} \mid \ldots \mid

1039: S \cup \{B_k\}$ 

1040: whenever $\inst(S) \pmodels C = B_1[\varione] \sqcup \ldots

1041: \sqcup B_k[\varik]$, $C$ is an $\epsilon$-clause, and

1042: $1\le i_1,\ldots,i_k \le r+1$.  Then $\absres$ simulates $\subordfsplres$:

1043: \newcounter{lemabsimulate}

1044: \namelem{lemabsimulate}

1045: \def\lemabsimulatestatement{

1046: If $S$ is a set of complex clauses and $\epsilon$-blocks, $S \abs T$ and $S

1047: \subordfsplres {\mathcal T}$, then all clauses occurring in ${\mathcal

1048: T}$ are complex clauses or $\epsilon$-blocks and $T \absres^* {\mathcal T}'$

1049: for some ${\mathcal T}'$ such that ${\mathcal T} \abs {\mathcal T}'$.

1050: }

1051: \begin{lemma}

1052: \label{lemma:abs:simulate}

1053: \lemabsimulatestatement

1054: \end{lemma}

1055: \proof 

1056: We have the following ways in which ${\mathcal T}$ is obtained from $S$

1057: by doing one resolution step followed by splitting:

1058: 

1059: \begin{itemize}

1060: 

1061: \item

1062: We resolve two $\epsilon$-blocks 

1063: $C_1$ and $C_2$ of $S$ to get an $\epsilon$-block $C$, and

1064: ${\mathcal T} = S \cup \{C\}$. Then 

1065: $\{C_1[\varrone],C_2[\varrone]\}\pmodels C[\varrone]$. Also

1066: as $S \abs T$ we have  $\{C_1[\varrone],C_2[\varrone]\} \subseteq 

1067: \eps(T)[\varrone]$.  We have $\inst(T) \pmodels C[\varrone]$.

1068: Hence $T \absres T \cup \{C[\varrone]\}$

1069: and clearly $S \cup \{C\} \abs T \cup \{C\}$.

1070: 

1071: \item

1072: We resolve an $\epsilon$-block $C_1[\varrone]$ with a complex clause 

1073: $C_2[\varone,\ldots,\varr]$, both from $S$ upto renaming, and we have

1074: $C_1[\varrone]\in \eps(T)[\varrone]$ and $\inst(T) \pmodels 

1075: \proj(C_2)$. By ordering constraints, we have $C_1[\varrone] = 

1076: C'_1[\varrone] \lor \pm P(\varrone)$ and 

1077: $C_2[\varone,\ldots,\varr] = \mp P(f(x_1,\ldots,x_n)) \lor 

1078: C'_2[\varone,\ldots,\varr]$ so that resolution produces

1079: $C[\varone,\ldots,\varr]

1080:  = C'_1[f(x_1,\ldots,x_n)] \lor C'_2[\varone,\ldots,\varr]$.

1081: Clearly $C_1[\u] \cup \{C_2[\varone,\ldots,\varr]\} \pmodels 

1082: C[\varone,\ldots,\varr]$. Also $\proj(C_1[\u]) = C_1[\u]$.

1083: Hence $\inst(T) C_1[\u] \cup \proj(C_2) \pmodels 

1084: \proj(C) \supseteq \{C[\varone,\ldots,\varr]\}$.

1085: \begin{itemize}

1086: \item

1087: If $C'_1$ is not empty or if $C'_2$ has some non-trivial literal then

1088: $C$ is a complex clause and ${\mathcal T} = S \cup \{C\} \abs T$.

1089: \item If $C'_1$ is empty and $C'_2$ has only trivial literals then 

1090: $C[\varone,\ldots,\varr]$ is 

1091: an $\epsilon$-clause of the form $B_1[\varione] \sqcup \ldots \sqcup

1092: B_k[\varik]$ 

1093: with $1\le i_1,\ldots,i_k\le r$.

1094: ${\mathcal T} = S \cup \{B_1\} \mid \ldots \mid S \cup \{B_k\}$.

1095: Since $\inst(T) \pmodels C[\varone,\ldots,\varr]$, 

1096: hence $T \absres {\mathcal T}'$ where ${\mathcal T}' = 

1097: T \cup \{B_1\}  \mid \ldots \mid T \cup \{B_k\}$ and we have

1098: ${\mathcal T} \abs {\mathcal T}'$.

1099: \end{itemize}

1100: 

1101: \item

1102: We resolve two complex clauses $C_1[\varone,\ldots,\varr]$ and 

1103: $C_2[\varone,\ldots,\varr]$, both from $S$ upto renaming, and we have

1104: $\inst(T) \pmodels \proj(C_1)$ and $\inst(T) \pmodels \proj(C_2)$.

1105: First we rename the second clause as $C_2[\varrone,\ldots,\varrr]$ by

1106: applying the renaming $\sigma_0 = \{\varone \mapsto \varrone,

1107: \ldots,\varr \mapsto \varrr\}$.

1108: By ordering constraints, $C_1[\varone,\ldots,\varr]$ is of the form 

1109: $C'_1[\varone,\ldots,\varr] \lor 

1110: \pm P(f(x_1,\ldots,x_n))$ and $C_2[\varrone,\ldots,\varrr]$ is of the form

1111: $\mp P(f(y_1,\ldots,y_n)) \lor C'_2[\varrone,\ldots,\varrr]$ so that 

1112: $\pm P(f(x_1,\ldots, x_n))$ and $\mp P(f(y_1,\ldots,y_n))$ are

1113: the literals to be resolved from the respective clauses. 

1114: By Lemma~\ref{lemma:sequnif}, the resolvent is $C = C'_1[\varone,\ldots,\varr]

1115: \sigma \lor C'_2 [\varrone,\ldots,\varrr]\sigma$ where $\sigma$ is such that

1116: $\{x_1,\ldots,x_n\} \sigma \subseteq \{x_1,\ldots,x_n\}$

1117: and $y_i\sigma = x_i\sigma$ for $1\le i\le n$. 

1118: $C$ is obtained by propositional resolution from

1119: $C_1\allowbreak [\allowbreak \varone,\allowbreak \ldots,\allowbreak \varr\allowbreak ]\allowbreak \sigma \allowbreak \in\allowbreak  \proj(C_1)$ 

1120: and $C_2[\varrone,\ldots,\varrr]\sigma

1121: = C_2[\varone,\ldots,\varr]\sigma_0\sigma \in \proj(C_2)$.

1122: Hence $\proj(C_1) \cup \proj(C_2) \pmodels C[\varone,\ldots,\varr]$. 

1123: Hence $\proj(\proj(C_1)) \cup \proj(\proj(C_2)) = \proj(C_1) \cup

1124: \allowbreak \proj\allowbreak (C_2) 

1125: \pmodels \proj(C)$.  As $\inst(T) \pmodels \proj(C_1)$ and

1126: $\inst(T) \pmodels \proj(C_2)$.

1127: hence $\inst(T) \pmodels \proj(C) \supseteq \{C[\varone,\ldots,\varr])\}$.

1128: 

1129: 

1130: \begin{itemize}

1131: \item

1132: If either $C'_1$ or $C'_2$ contains a non-trivial literal then 

1133: $C$ is a complex clause and ${\mathcal T} = S \cup \{C\} \abs T$. 

1134: \item

1135: If $C'_1$ and $C'_2$ contain only trivial literals then 

1136: $C[\varone,\ldots,\varr]$ is an

1137: $\epsilon$-clause of the form $B_1[\varione]\sqcup\ldots\sqcup B_k[\varik]$

1138: with $1\le i_1, \ldots, i_k \le r$.

1139: ${\mathcal T} = S \cup \{B_1\} \mid \ldots \mid S \cup \{B_k\}$.

1140: As $\inst(T) \pmodels C[\varone,\ldots,\varr]$ we have

1141: $T \absres \mathcal T'$ where $\mathcal T' =

1142: T \cup \{B_1\} \mid \ldots \mid T \cup \{B_k\}$.

1143: Also $\mathcal T \abs \mathcal T'$.

1144: \end{itemize}

1145: 

1146: \item

1147: $C[\varone,\ldots,\varr]$ is a renaming of a 

1148: complex clause in $S$, and we factor $C\allowbreak [\allowbreak \varone\allowbreak ,\allowbreak \ldots\allowbreak ,\allowbreak \varr\allowbreak ]$ 

1149: to get a complex clause $C[\varone,\ldots,\varr]\sigma$ where

1150: $\rvarset\sigma\subseteq \rvarset$, and 

1151: ${\mathcal T} = S\cup\{C[\varone,\ldots,\varr]\sigma\}$.

1152: $C[\varone,\ldots,\varr]\sigma \in \proj(C)$.

1153: Hence $\proj\allowbreak (\allowbreak \{\allowbreak C\allowbreak [\allowbreak \varone\allowbreak ,\allowbreak \ldots,\varr\allowbreak ] \sigma\}) \subseteq 

1154: \proj(\proj(C)) = \proj(C)$.

1155: As $S \abs T$ hence $\inst(T) \pmodels \proj(C)$.

1156: Hence $\inst(T) \pmodels \proj(\{C[\varone,\allowbreak \ldots,\allowbreak \varr]\sigma\})$.

1157: Hence we have $\mathcal T = S \cup \{C[\varone,\allowbreak \ldots,\allowbreak \varr]\sigma\} \abs T$.\qed

1158: \end{itemize}

1159: \endproof 

1160: Hence we have completeness of $\absres$:

1161: \begin{lemma}

1162: \label{lemma:abs:complete}

1163: If a set $S$ of good complex clauses and $\epsilon$-blocks is unsatisfiable then 

1164: $S \absres^* \mathcal T$ for some closed $\mathcal T$.

1165: \end{lemma}

1166: \proof 

1167: By Lemma~\ref{lemma:ordspl:compl},

1168: $S \subordfsplres^* S_1 \mid \ldots \mid S_n$ such

1169: that each $S_i\owns \empcl$.

1170: As $S \abs S$, hence by Lemma~\ref{lemma:abs:simulate}, we have some

1171: $T_1,\ldots,T_n$ such that $S\absres^* T_1\mid\ldots\mid T_n$ and $S_i\abs T_i$ for

1172: $1\le i\le n$. Since $\empcl \in S_i$ and $\empcl$ is an $\epsilon$-block,

1173: hence $\empcl\in T_i$ for $1\le i\le n$.

1174: \qed

1175: \endproof 

1176: 

1177: Call a set $S$ of complex clauses and $\epsilon$-blocks

1178: {\em saturated} if the following condition is satisfied:

1179: if $\inst(S) \pmodels B_1[\varione] \sqcup \ldots \sqcup B_k[\varik]$ 

1180: with $1\le i_1,\ldots,i_k\le r+1$, each $B_i$ being an $\epsilon$-block, 

1181: then there is some $1\le j\le k$ such that $B_j[\varrone] \in S[\varrone]$.

1182: 

1183: 

1184: \begin{lemma}

1185: \label{lemma:abs:saturate}

1186: If $S$ is a satisfiable set of complex clauses and $\epsilon$-blocks 

1187: then $S \absres^* \mathcal T \mid T$ for some $\mathcal T$ and some

1188: saturated set $T$ of complex clauses and $\epsilon$-blocks,

1189: such that $\empcl \notin T$.

1190: \end{lemma}

1191: \proof 

1192: We construct a sequence $S = S_0 \subseteq S_1\subseteq S_2 \subseteq \ldots$

1193: of complex clauses and $\epsilon$-blocks such that $S_i$ is satisfiable and

1194: $S_i \absres^* S_{i+1} \mid \mathcal T_i$ for some $\mathcal T_i$ for each $i$. 

1195: $S=S_0$ is satisfiable by assumption.

1196: Now assume we have already defined $S_0,\ldots,S_i$ and $\mathcal T_0,

1197: \ldots,\mathcal T_{i-1}$.

1198: Let $C^l = B^l_1[\varlione] \sqcup \ldots \sqcup B^l_k[\varlikl]$

1199: for $1\le l\le N$ be all the possible $\epsilon$-clauses such that 

1200: $\inst(S_i) \pmodels C^l$, $1\le i^l_1,\ldots,i^l_{k_l}\le r+1$.

1201: Since $S_i$ is satisfiable,

1202:  $S_i \cup \{C^l \mid 1\le l\le N\}$ is satisfiable.

1203: Since $\varlione,\ldots,\varlikl$ are mutually distinct for $1\le l\le N$,  

1204: there are $1\le j_l\le k_l$ for $1\le l\le N$ such that

1205: $S_i \cup \{B^l_{j_l}\mid 1\le l\le N\}$ is satisfiable.

1206: Let $S_{i+1} = S_i \cup \{B^l_{j_l}\mid 1\le l\le N\}$. 

1207: $S_{i+1}$ is satisfiable.

1208: Also it is clear that $S_i \absres^* S_{i+1} \mid \mathcal T_i$ for some

1209: $\mathcal T_i$.

1210: If $S_{i+1} = S_i$ then $S_i$ is saturated, otherwise $S_{i+1}$ has

1211: strictly more $\epsilon$-blocks upto renaming. 

1212: As there are only finitely many $\epsilon$-blocks upto renaming, 

1213: eventually we will end up with a saturated set $T$

1214: in this way. Since $T$ is satisfiable, $\empcl \notin T$. From construction

1215: it is clear that there is some $\mathcal T$ such that $S \absres^* \mathcal T

1216: \mid T$.

1217:  \qed

1218: \endproof 

1219: 

1220: \begin{theorem}

1221: \label{theorem:flatsat}

1222: Satisfiability for the class $\flat$ is NEXPTIME-complete.

1223: \end{theorem}

1224: \proof 

1225: The lower bound comes from reduction of satisfiability of positive set

1226: constraints which is NEXPTIME-complete~\cite{akvw:set}. For the upper bound

1227: let $S$ be a finite set of flat clauses. 

1228: Repeatedly apply $\epsilon$-splitting to obtain 

1229: $f(S)=S_1 \mid \ldots \mid S_m$.  $S$ is satisfiable iff

1230: some $S_i$ is satisfiable. 

1231: The number $m$ of branches in $f(S)$ is at most exponential. 

1232: Also each branch has size linear in the size of $S$. 

1233: We non-deterministically choose some $S_i$ and check its satisfiability

1234: in NEXPTIME.

1235: 

1236: Hence wlog we may assume that the given set $S$ has only complex clauses and

1237: $\epsilon$-blocks.  We non-deterministically choose a certain number of

1238: $\epsilon$-blocks $B_1,\ldots,B_N$ 

1239: and check that $T =  S_1 \cup \{B_1,\ldots,B_N\}$

1240: is saturated and $\empcl\notin T$.

1241: By Lemma~\ref{lemma:abs:saturate}, 

1242: if $S$ is satisfiable then clearly there is such a set $T$.

1243: Conversely if there is such a set $T$, then whenever $T \absres^* 

1244: \mathcal T$, we will have $\mathcal T = T \mid \mathcal T'$ 

1245: for some ${\mathcal T}'$. Hence we can never have $T \absres^* {\mathcal T}$

1246: where $\mathcal T$ is closed.  Then by Lemma~\ref{lemma:abs:complete}

1247: we conclude that $T$ is satisfiable. Hence $S \subseteq T$ is also satisfiable.

1248: 

1249: Guessing the set $T$ requires non-deterministically 

1250: choosing from among exponentially many $\epsilon$-blocks.

1251: To check that $T$ is saturated, for every  

1252: $\epsilon$-clause $C = B_1[\varione] \sqcup \ldots \sqcup B_k[\varik]$, 

1253: with $1\le i_1, \ldots, i_k\le r+1$, and $B_j[\varrone]

1254:  \notin T[\varrone]$ for $1\le j\le k$, we check that

1255: $\inst(T) \pnmodels C$, i.e. 

1256: $\inst(T) \cup \lnot C$ is propositionally satisfiable

1257: (where $\lnot(L_1\lor\ldots\lor L_n)$ denotes $\{-L_1,\ldots,-L_n\}$).

1258: This can be checked in NEXPTIME since

1259: propositional satisfiability can be checked in NPTIME.

1260: We need to do such checks for at most exponentially many possible

1261: values of $C$. \qed

1262: \endproof 

1263: 

1264: 

1265: 

1266: 

1267: 

1268: 

1269: 

1270: 

1271: 

1272: 

1273: 

1274: 

1275: 

1276: 

1277: 

1278: 

1279: 

1280: 

1281: 

1282: 

1283: 

1284: 

1285: 

1286: 

1287: 

1288: 

1289: 

1290: 

1291: 

1292: 

1293: 

1294: 

1295: 

1296: 

1297: 

1298: \section{Combination: Ordered Literal Replacement}

1299: \label{sec:nh}

1300: 

1301: Combining flat and one-variable clauses creates additional difficulties.

1302: First observe that resolving a one variable clause 

1303: $C_1 \lor \pm P(f(s_1[x],\ldots,s_n[x]))$

1304: with a complex clause $\mp P(f(x_1,\ldots,x_n)) \lor C_2$ produces a 

1305: one-variable clause. If $s_i[x]=s_j[x]$ for all $x_i=x_j$, and if

1306: $C_2$ contains a literal $P(x_i)$ then the resolvent contains a literal

1307: $P(s_i[x])$. The problem now is that even if

1308: $f(s_1[x],\ldots,s_n[x])$ is reduced, $s_i[x]$ may not be reduced. E.g.

1309: $f(g(h(x)),x)$ is reduced but $g(h(x))$ is not reduced. Like in

1310: Section~\ref{sec:onevar} we may think of replacing this literal by simpler

1311: literals involving fresh predicates. Firstly we have to ensure that in this

1312: process we do not generate infinitely many predicates. Secondly

1313: it is not clear that mixing ordered resolution steps

1314: with replacement of literals is still complete. Correctness is easy to show

1315: since the new clause is in some sense equivalent to the old deleted clause.

1316: However deletion of clauses arbitrarily can violate completeness of the 

1317: resolution procedure. The key factor which preserves completeness is that

1318: we replace literals by smaller literals wrt the given ordering $\atlt$.

1319: 

1320: Formally a {\em replacement rule} is of  the form 

1321: $A_1 \repl A_2$ where $A_1$ and $A_2$

1322: are (not necessarily ground) atoms.  The clause set 

1323: {\em associated} with this rule is $\{A_1 \lor - A_2, 

1324:  - A_1 \lor A_2\}$.

1325: Intuitively such a replacement rule says that  $A_1$ and

1326: $A_2$ are equivalent. The clause set $cl(\mathcal R)$

1327: associated with a set $\mathcal R$

1328: of replacement rules is the union of the clause sets associated with the 

1329: individual replacement rules in $\mathcal R$.

1330: Given a stable ordering $\atlt$ on atoms, a 

1331: replacement rule $A_1 \repl A_2$ is {\em ordered} iff

1332: $A_2\atlt A_1$. 

1333: We define the relation $\repl_{\mathcal R}$ as: $S \repl_{\mathcal R}

1334: (S \setminus \{\pm A_1 \sigma \lor C \}) \cup \{\pm A_2\sigma \lor C\}$ 

1335: whenever $S$ is a set of clauses, $\pm A_1\sigma \lor C \in S$, 

1336: $A_1 \repl A_2 \in \mathcal R$ and $\sigma$ is some substitution. 

1337: Hence we replace literals in a clause by smaller literals.

1338: The relation is extended to tableaux as usual.

1339: This is reminiscent of the well-studied  

1340: case of resolution with some equational theory

1341: on terms. There, however, the ordering

1342: $\atlt$ used for resolution is compatible with the equational theory and one

1343: essentially works with the equivalence classes of terms and atoms. This is not

1344: the case here.

1345: 

1346: Next note that in the above resolution example, even if 

1347: $f(s_1[x],\ldots,s_n[x])$ is non-ground, some $s_i$ may be ground. 

1348: Hence the resolvent may have ground as well as non-ground literals. We avoided

1349: this in Section~\ref{sec:onevar} by initial preprocessing. Now we may think

1350: of splitting these resolvents during the resolution procedure. This however

1351: will be difficult to simulate using the alternative resolution procedure

1352: on succinct representations of tableaux because we will generate doubly 

1353: exponentially many one-variable clauses. To avoid this

1354: we use a variant of splitting 

1355: % , introduced in~\cite{voronkov:splitting}, and 

1356: called {\em splitting-with-naming}~\cite{voronkov:splitting}. 

1357: %in~\cite{JGL:SOresol}. 

1358: Instead of creating two branches after

1359: splitting, this rule puts both components into the same set, but with

1360: tags to simulate branches produced by ordinary splitting. 

1361: Fix a finite set $\mathbb P$ of predicate symbols. 

1362: $\mathbb P$-clauses are clauses whose predicates are all from $\mathbb P$.

1363: Introduce fresh zero-ary predicates 

1364: $\ssp{C}$ for $\mathbb P$-clauses $C$ modulo renaming, i.e. 

1365: $\ssp{C_1}=\ssp{C_2}$

1366: iff $C_1\sigma=C_2$ for some renaming $\sigma$. Literals $\pm \ssp{C}$

1367: for $\mathbb P$-clauses $C$ are  {\em splitting literals}.

1368: The {\em splitting-with-naming} rule is defined as:

1369: $S \ssplres (S \setminus \{C_1 \sqcup C_2\}) \cup \{C_1 \lor -\ssp{C_2},

1370: \ssp{C_2} \lor C_2\}$ where $C_1 \sqcup C_2\in S$,

1371: $C_2$ is non-empty and has only non-splitting literals, and

1372: $C_1$ has at least one non-splitting literal. 

1373: Intuitively $\ssp{C_2}$ represents the negation of $C_2$.

1374: We will use both

1375: splitting and splitting-with-naming according to some predefined strategy.

1376: Hence for a finite set

1377: $\sspreds$ of splitting atoms, define {\em $\sspreds$-splitting}

1378: as the restriction of the splitting-with-naming rule where the splitting

1379: atom produced is restricted to be from $\sspreds$. Call this restricted

1380: relation as $\predssplres$. This is extended to tableaux as usual.

1381: Now once we have generated the clauses

1382: $C_1 \lor -\ssp{C_2}$ and $\ssp{C_2} \lor C_2$ we would like to keep resolving

1383: on the second part of the second clause till we are left with the clause

1384: $\ssp{C_2}$ (possibly with other positive splitting literals)

1385:  which would then be resolved with the first clause to produce

1386: $C_1$ (possibly with other positive splitting literals)

1387:  and only then the literals in $C_1$ would be resolved upon.

1388: Such a strategy cannot be ensured by ordered resolution, hence we introduce

1389: a new rule.

1390: An ordering $\atlt$ over non-splitting atoms is extended to the ordering

1391: $\atltss$ by letting $q\atltss A$ whenever $q$ is a splitting atom

1392: and $A$ is a non-splitting atom, and $A \atltss B$

1393: whenever $A,B$ are non-splitting atoms and $A \atlt B$.

1394: %A stable ordering $\atlt$ is {\em admissible} if $q\atlt P(t)$ whenever

1395: %$q$ is splitting and $P(t)$ non-splitting literal.

1396: We define {\em modified ordered binary resolution} by the following rule:\\

1397: \strut\hfill$\prooftree

1398: C_1\lor A \quad   - B \lor C_2

1399: \justifies C_1\sigma \lor C_2\sigma

1400: \endprooftree$\hfill\ 

1401: 

1402: \noindent

1403: where $\sigma = mgu(A,B)$ and the following conditions are satisfied:\\

1404: (1) $C_1$ has no negative splitting literal, and $A$ is maximal in $C_1$.\\

1405: (2) (a) either $B\in \sspreds$, or\\

1406: \hspace*{15pt}(b) $C_2$ has no negative splitting literal, and $B$ is maximal in $C_2$.\\

1407: As usual we rename the premises before resolution so that 

1408: they don't share variables. This rule says that we must select a negative

1409: splitting literal to resolve upon in any clause, provided the clause has

1410: at least one such literal. If no such literal is present in the clause, then

1411: the ordering $\atltss$  enforces that a positive splitting literal will

1412: not be selected as long as the clause has some non-splitting literal.

1413: We write 

1414: $S \atordselres S \cup \{C\}$ to say that $C$ is obtained by one application of

1415: the modified binary ordered resolution or the (unmodified)

1416: ordered factorization rule on clauses in $S$. This is extended to tableaux

1417: as usual.

1418: A {\em $\sspreds$-splitting-replacement strategy} is  a 

1419: function $\phi$ such that $\mathcal T (\predssplres \cup\splres \cup\replres)^* 

1420: \phi(\mathcal T)$  for any tableaux $\mathcal T$. Hence we allow both normal

1421: splitting and $\sspreds$-splitting.

1422: Modified ordered resolution with $\sspreds$-splitting-replacement

1423: strategy $\phi$ is defined by the relation: $S \atordselfssplreplres \phi(T)$ 

1424: whenever $S \cup cl(\mathcal R) \atordselres T$. 

1425: This is extended to tableaux as usual.  The above modified ordered

1426: binary resolution rule can be considered as an instance of 

1427: {\em ordered resolution with selection}~\cite{BG:HAR}, which is known 

1428: to be sound and complete even with splitting and its variants. 

1429: Our manner of extending $\atlt$ to $\atltss$ is essential for completeness.

1430: We now show 

1431: that soundness and completeness hold even under arbitrary ordered replacement 

1432: strategies. It is not clear to the authors if such rules have been studied elsewhere.

1433:  Wlog we forbid the useless case of replacement rules

1434: containing splitting symbols.

1435: The relation $\atlt$ is  {\em enumerable} if 

1436: the set of all 

1437: ground atoms can be enumerated as $A_1,A_2,\ldots$ 

1438: such that if $A_i \atlt A_j$ then $i < j$. 

1439: The subterm ordering is enumerable.

1440: 

1441: 

1442: 

1443: 

1444: 

1445: 

1446: 

1447: 

1448: 

1449: 

1450: 

1451: 

1452: 

1453: 

1454: 

1455: 

1456: 

1457: 

1458: 

1459: 

1460: 

1461: 

1462: 

1463: 

1464: 

1465: 

1466: 

1467: \newcounter{thcompl}

1468: \nameth{thcompl}

1469: \def\thcomplstatement{

1470: Modified ordered resolution, wrt a stable and enumerable ordering,

1471: with splitting and $\sspreds$-splitting and ordered  literal

1472: replacement is sound and complete for any strategy. I.e.

1473: for any set $S$ of $\mathbb P$-clauses, for any strict stable and enumerable

1474: partial order $\atlt$ on atoms, for any set

1475: $\mathcal R$ of ordered replacement rules,

1476: for any finite set $\sspreds$ of splitting atoms, and for any 

1477: $\sspreds$-splitting-replacement strategy $\phi$, $S \cup cl(\mathcal  R)$

1478: is unsatisfiable iff $S \atordselfssplreplres^* \mathcal T$ 

1479: for some closed $\mathcal T$.

1480: }

1481: \begin{theorem}

1482: \label{th:compl}

1483: \thcomplstatement

1484: \end{theorem}

1485: \proof

1486: See Appendix~\ref{apptwo}.

1487: 

1488: 

1489: 

1490: 

1491: 

1492: 

1493: 

1494: 

1495: 

1496: 

1497: 

1498: 

1499: 

1500: 

1501: 

1502: 

1503: 

1504: 

1505: 

1506: 

1507: 

1508: 

1509: 

1510: 

1511: For the rest of this section fix a set $\mathbb S$ of one-variable 

1512: $\mathbb P$-clauses and complex $\mathbb P$-clauses whose satisfiability 

1513: we need to decide.  Let $\ng$ be the set of non-ground

1514: terms occurring as arguments in literals in the one-variable clauses

1515: of $\mathbb S$. We rename all terms in $\ng$ to contain only the variable

1516: $\varrone$.

1517: Wlog assume $\varrone \in \ng$.

1518: Let $\ngs$ be the set of non-ground subterms of terms in $\ng$,

1519: and $\ngr = \{s[\varrone]\mid s \textrm{ is non-ground and reduced,}

1520:  \allowbreak \textrm{and for some } t, s[t]\in \ngs\}$.

1521: Define $\ngrr = 

1522: \{s_1[\allowbreak \ldots\allowbreak [\allowbreak s_m\allowbreak ]\allowbreak \ldots\allowbreak ]\allowbreak \mid s_1[\ldots[s_n]\ldots] \in \ngs,\allowbreak m\le n,

1523: \textrm{ and each } s_i \allowbreak 

1524: \textrm{ is \allowbreak non-trivial \allowbreak and \allowbreak reduced}\}$.

1525: Define the set of predicates $\mathbb Q = \{Ps \mid P\in\mathbb P,s \in \ngrr\}$.

1526: Note that $\mathbb P \subseteq \mathbb Q$.

1527: Define the set of replacement rules $\mathcal R = 

1528: \{Ps_1\ldots s_{m-1} (s_m[\varrone]) \repl \allowbreak Ps_1\ldots s_m \allowbreak (\allowbreak [\allowbreak \varrone\allowbreak ]\allowbreak ) 

1529: \mid Ps_1\ldots s_m  \in \mathbb Q\}$. They are clearly ordered wrt $\sublt$.

1530: Let $\g$ be the set of ground subterms of terms occurring as arguments in 

1531: literals in $\mathbb S$. 

1532: Define the set $\grpreds = \{\ssp{\pm P(t)} \mid P \in \mathbb P,

1533: t\in \g\}$ of splitting atoms. Their purpose is to remove ground literals from 

1534: a non-ground clause.  All sets defined above have polynomial size. 

1535: Let $\sspreds\supseteq\grpreds$ be any set of splitting atoms. For dealing with

1536: the class $\c$ we only need $\sspreds=\grpreds$, but for a more precise analysis

1537: of the Horn fragment in the next Section, we need $\sspreds$ to also contain 

1538: some other splitting atoms.

1539: We also need the set $\ngrone = \{\varrone\} \cup 

1540: \{f (s_1,\ldots,s_n) \mid \exists g(t_1,\ldots,t_m) \in \ngr \cdot

1541: \{s_1,\ldots,s_n\}=\{t_1,\ldots,t_m\}\}$ which has exponential size.

1542: These terms are produced by resolution of non-ground one-variable

1543: clauses with complex clauses, and are also reduced. 

1544: In the ground case we have the set

1545: $\gone = \{f(s_1,\ldots,s_n) \mid \exists g(t_1,\ldots,t_m)

1546: \in \g \mid \{s_1,\ldots,s_n\}=\{t_1,\ldots,t_m\}\}$ of exponential size.

1547: For a set $\mathbb P'$ of predicates and a set $U$ of terms,

1548: the set $\mathbb P'[U]$ of atoms is defined as usual. For a set $V$ of

1549: atoms the set $-V$ and $\pm V$ of literals is defined as usual.

1550: The following types of clauses will be required during resolution:

1551: \begin{enumerate}

1552: \item[(C1)] clauses $C \lor D$, where

1553: $C$ is an $\epsilon$-block with predicates from $\mathbb Q$, and

1554: $D\subseteq\pm\sspreds$.

1555: \item[(C2)] clauses $C \lor D$  where

1556: $C$ is a renaming of a one-variable clause with literals from 

1557: $\pm \mathbb Q(\ngrone)$,

1558: $C$ has at least one non-trivial literal, and $D\subseteq\pm \sspreds$.

1559: \item[(C3)] clauses $C \lor D$ 

1560: where $C$ is a non-empty clause with literals from 

1561: $\pm \mathbb Q(\ngrone[\ngrr[\gone]])$, and $D\subseteq\pm\sspreds$.

1562: \item[(C4)] clauses $C\lor D$ where $C= 

1563: \bigvee_{i=1}^k \pm_i P_i(f_i(x^i_1,\ldots,x^i_{n_i})) \lor

1564: \bigvee_{j=1}^l \pm_j Q_j(x_j)$ is a complex clause

1565: with each $P_i\in \mathbb Q$, each $n_i\ge2$, each $Q_j \in \mathbb P$ and 

1566: $D\subseteq\pm\sspreds$

1567: \end{enumerate}

1568: 

1569: We have already argued why we need splitting literals in the above clauses,

1570: and why we need $\ngrone$ instead of $\ngr$ in type C2.

1571: In type C3 we have $\ngrr$ in place of the set $\ngs$ that we had in

1572: Section~\ref{sec:onevar}, to take care of interactions between one-variable 

1573: clauses and complex clauses.  In type C4 the trivial literals involve

1574: predicates only from $\mathbb P$ (and not $\mathbb Q$). This is what ensures 

1575: that we need only finitely many fresh predicates (those from $\mathbb Q

1576: \setminus \mathbb P$) because these are the literals that are involved in

1577: replacements when this clause is resolved with a one-variable clause.

1578: We have also required that each $n_i\ge 2$. This is only to ensure that types

1579: C2 and C4 are disjoint. The clauses that are excluded because of this condition

1580: are necessarily of type C2.

1581: 

1582: The $\grpreds$-splitting steps that we use in this section consist of

1583: replacing a tableau $\mathcal T \mid S$ by the tableau $\mathcal T \mid

1584: (S \setminus \{C \lor L\}) \cup \{C \lor -\ssp{L},

1585: \ssp{L} \lor L\}$, where $C$ is non-ground, $L\in\pm\mathbb P(\g)$

1586: and $C \lor L \in S$.

1587: The replacement steps we are going to use are of the following kind:\\

1588: (1) replacing clause $C_1[x] = C\lor\pm P(t_1[\ldots[t_n[s[x]]]\ldots])$

1589: by clause $C_2[x] = C \lor \pm Pt_1\ldots t_n(s[x])\}$ where $P\in\mathbb P$,

1590: $s[\varrone]\in\ngr$ is  non-trivial, and $t_1[\ldots[t_n]\ldots] \in \ngrr$.

1591: We have $\{C_1[\varrone]\} \cup cl(\mathcal R)[\ngrr] \pmodels C_2[\varrone]$.

1592: \\

1593: (2) replacing ground clause $C_1 = C\lor\pm P(t_1[\ldots[t_n[g]]\ldots])$

1594: by clause $C_2 = C \lor \pm Pt_1\ldots t_n[g]\}$ where $P\in\mathbb P,

1595: g\in \ngrr[\gone]$ and $t_1[\ldots[t_n]\ldots] \in \ngrr$. This replacement

1596: is done only when $t_1[\ldots[t_n[g]]\ldots] \in \ngrr[\ngrr[\gone]]\setminus

1597: \ngrone[\ngrr[\gone]]$. We have

1598: $\{C_1\} \cup cl(\mathcal R)[\ngrr[\ngrr[\gone]]] \pmodels C_2$.\\

1599: Define the $\grpreds$-splitting-replacement strategy $\phi$ as one which 

1600: repeatedly applies first $\epsilon$-splitting,

1601: then the above $\grpreds$-splitting steps, then the above two 

1602: replacement steps till no further change is possible. Then

1603: $\subordselfssplreplres$ gives us a sound and complete method for

1604: testing unsatisfiability. 

1605: 

1606: As in Section~\ref{sec:flat} we now define

1607: a succinct representation of tableaux and an alternative resolution procedure

1608: for them. As we said, a literal 

1609: $\ssp{L} \in\grpreds$ represents $-L$. Hence for a clause $C$ we define

1610: $\qrep{C}$ as the clause obtained by replacing every $\pm\ssp{L}$ by the

1611: literal $\mp L$.  This is extended to sets of clauses as usual. Observe that

1612: if $S \pmodels C$ then $\qrep S \pmodels \qrep C$.

1613: As before  $\u = \{f(x_1,\ldots,x_n) \mid

1614: f\in\Sigma, \textrm{ and each } x_i \in \rvarset\}$.

1615: The functions $\eps$ and $\comp$ of Section~\ref{sec:flat} are now modified

1616: to return clauses of type C1 and C2 respectively. 

1617: For a set $S$ of clauses, define $\ov(S)$ as the set of clauses of type C2

1618: in $S$. The function $\proj$ is as before.

1619: We need to define which kinds of instantiations are to be used to generate

1620: propositional implications.

1621: %%% extend eps comp .. in presence of splitting literals

1622: For a clause $C$, define 

1623: \[\begin{array}{r l}

1624: \instone(C) = &  C[\u[\ngrr \cup \ngrr[\ngrr[\gone]]]] 

1625: \cup C[\ngrone] \cup C[\ngrone[\ngrr[\gone]]]\\

1626: \insttwo(C) = & \{C[\varrone]\} \cup C[\ngrr[\gone]]\\

1627: \instthree(C) = & \{C\}\\

1628: \instfour(C) = & \proj(C) \cup C[\ngrr \cup \ngrr[\ngrr[\gone]]]

1629: \end{array}\]

1630: 

1631: The instantiations defined by $\inst_i$ are necessary for clauses of

1632: type C$i$. Observe that $C[U]\subseteq\instone(C)$.

1633: For a set $S$ of clauses, define $\insti(S) = \bigcup_{C\in S} \insti(C)$. 

1634: For a set $S$ of clauses of type C1-C4 define

1635: $\inst(S) =  \instone(\qrep{\eps(S)}) \cup 

1636: \insttwo(\qrep{\ov(S)}) \cup  \instthree(\qrep{\ground(S)}) \cup

1637: \instfour(\qrep{\comp(S)}) \cup cl(\mathcal R)[\ngrr \cup \ngrr[\ngrr[\gone]]]$.

1638: Note that instantiations of clauses in $cl(\mathcal R)$ are necessary for

1639: the replacement rules, as argued above.

1640: For a set $T$ of clauses define the following properties:

1641: \begin{itemize}

1642: \item

1643: $C$ satisfies property P1$_T$ iff $C[\varrone] \in T$.

1644: \item

1645: $C$ satisfies property P2$_T$ iff $\inst(T) \pmodels \insttwo(\qrep{C})$.

1646: \item

1647: $C$ satisfies property P3$_T$ iff $\inst(T) \pmodels \instthree(\qrep{C})$.

1648: \item

1649: $C$ satisfies property P4$_T$ iff $\inst(T)\pmodels\instfour(\qrep{C})$.

1650: \end{itemize}

1651: For sets of clauses $S$ and $T$, define $S \abss T$ to mean that 

1652: every $C\in S$ is of type C$i$ and satisfies property P$i_T$ for some

1653: $1\le i\le 4$. This is extended to tableaux as usual.

1654: We first consider the effect of one step of the above resolution procedure 

1655: without splitting. Accordingly let $\phi_0$ be the variant of 

1656: $\phi$ which applies 

1657: replacement rules and $\grpreds$-splitting, but no $\epsilon$-splitting. 

1658: 

1659: \begin{lemma}

1660: \label{lemma:nhresol}

1661: Let $S$ be a set of clauses of type C1-C4. If

1662: $S\subordselnosplreplres S'$ then one of the following 

1663: statements holds.

1664: \begin{itemize}

1665: \item $S' \abss S$

1666: \item $S' = S \cup \{C\} \cup S''$, $C$ is a renaming of

1667: $B_1[\varione]\sqcup \ldots \sqcup

1668: B_k[\varik]\sqcup D$, each $B_i$ is an $\epsilon$-block, 

1669: $1\le i_1,\ldots,i_k\le r$, $D \subseteq\pm\sspreds$,

1670: $\inst(S) \pmodels \qrep C$, and $S''$ is a set of clauses of type C3 and

1671: $\emptyset \pmodels \qrep{S''}$. If $k\ge 2$ then $D$ has no literals $-q$

1672: with $q\in\sspreds\setminus\grpreds$.

1673: \end{itemize}

1674: \end{lemma}

1675: \proof 

1676: The set $S''$ in the second statement will contain the clauses $\ssp{L} \lor

1677: L$ added by $\grpreds$-splitting, while $C$ will be the clause produced by

1678: binary resolution or factoring, possibly followed by applications of

1679: replacement rules and by

1680: replacement of ground literals $L$ by $-\ssp{L}$. Hence $S''=\emptyset$ in all

1681: cases except when we need to perform $\grpreds$-splitting.

1682: 

1683: First we consider resolution steps where splitting literals are resolved upon.

1684: A positive splitting literal cannot be chosen to resolve upon in a clause

1685: unless the clause

1686: has no literals other than positive splitting literals. Hence this clause

1687: is $C_1 = q \lor q_1\lor\ldots\lor q_m$ of type C1,

1688: The other clause must be $C_2= C'_2 \lor -q$ 

1689: of type C$i$ for some $1\le i\le4$. Resolution produces clause 

1690: $C = C'_2 \lor  q_1\lor\ldots\lor  q_m$ of type C$i$, 

1691: and no replacement or splitting rules apply. 

1692: We have $\{C_1,C_2\}\pmodels C$ and $\{\qrep{C_1},\qrep{C_2}\}\pmodels

1693: \qrep{C}$. Hence $\inst(S) \supseteq \qrep{C_1} \cup \insti(\qrep{C_2}) \pmodels

1694: \insti(\qrep{C})$.

1695: If $i=1$ then the second statement of the lemma holds because 

1696: $\insti(\qrep C)$ contains a renaming of $\qrep C$. If $i>1$ then the first

1697: statement holds.

1698: 

1699: Now we consider binary resolution steps where no splitting literals are 

1700: resolved upon.

1701: This is possible only when no negative splitting literals are present in

1702: the premises. Then the resolvent has no negative splitting literals. 

1703: $\grpreds$ splitting may create negative splitting literals, but none of them

1704: are from $\sspreds\setminus\grpreds$. Hence the last part of the second

1705: statement of the lemma is always true.

1706: In the following $D,D_1,\ldots$ denote subsets of $\grpreds$.

1707: When we write $C\lor D$, it is implicit that $C$ has no splitting literals.

1708: We have the following cases:

1709: 

1710: \begin{enumerate}

1711: \item We do resolution between two clauses $C_1$ and $C_2$ from $S$, 

1712: both of type C1, and the resolvent  $C$ is of type C1.

1713: Hence no splitting or replacement rules apply,

1714: ${S'} = S \cup \{C\}$, $\inst(S) \supseteq 

1715: \{\qrep{C_1}[\varrone],\qrep{C_2}[\varrone]\} \pmodels \qrep{C}[\varrone]$.

1716: Hence the second statement holds.

1717: 

1718: \item We do resolution between a clause $C_1[\varrone] = C'_1[\varrone]

1719: \lor D_1 \lor \pm P(\varrone)$, of type C1,

1720: and a clause $C_2[\varrone] = \mp P(t[\varrone]) 

1721: \lor C'_2[\varrone] \lor D_2$, of type C2,

1722: both from $S$ upto renaming, and the resolvent 

1723: is $C[\varrone] = C'_1[t[\varrone]] \lor C'_2[\varrone]\lor  D_1 \lor D_2$.

1724: By ordering constraints $t[\varrone]\in \ngrone$  is non-trivial.

1725: All literals in $C'_1[t[\varrone]]\lor C'_2[\varrone]$ 

1726: are of the form $\pm' Q(t'[\varrone])$  with $t'[\varrone]\in\ngrone$. 

1727: Hence no splitting or replacement rules apply and $S' = S \cup \{C\}$. 

1728: $\qrep{C_1}[\ngrone] \cup \{\qrep{C_2}[\varrone]\}\pmodels \qrep{C}[\varrone]$. 

1729: Hence $\inst(S) \supseteq \instone(\qrep{C_1}) \cup \insttwo(\qrep{C_2}) 

1730: \supseteq

1731: \qrep{C_1}[\ngrone] \cup \qrep{C_2}[\allowbreak \ngrone[\allowbreak \ngrr[\allowbreak \gone]]] \cup

1732: \{\qrep{C_2}[\varrone]\} \cup \qrep{C_2}[\ngrr[\gone]] \pmodels 

1733: \{\qrep{C}[\varrone]\} \cup \qrep{C}[\ngrr[\gone]] =

1734: \insttwo(\qrep{C}[\varrone])$. 

1735: If $C'_1$ is non-empty or $C'_2$ has some 

1736: non-trivial literal

1737:  then $C[\varrone]$ is  of type C2, $S' \abss S$ and the first statement

1738: holds.

1739: If $C'_1$ is empty and $C'_2$ has only trivial

1740: literals, then $C$ is of type C1 and the second statement holds.

1741: 

1742: 

1743: 

1744: \item We do resolution between a clause $C_1[\varrone] = 

1745: C'_1[\varrone] \lor D_1 \lor \pm P(\varrone)$ of type C1,

1746: and a clause $C_2 = \mp P(t) \lor C'_2 \lor D_2$ of type C3,

1747: both from $S$ upto renaming, and the resolvent 

1748: is $C = C'_1[t] \lor C'_2\lor  D_1 \lor D_2$.

1749: We know that $t\in \ngrone[\ngrr[\gone]]$. 

1750: Hence no splitting or replacement rules apply, and

1751: ${S'} = S \cup \{C\}$.

1752: $\{C_1[t],C_2\} \pmodels C$.  Hence

1753: $\inst(S)\supseteq \instone(\qrep{C_1}[\varrone]) \cup \instthree(\qrep{C_2}) 

1754: \supseteq \qrep{C_1}[\ngrone[\ngrr[\gone]]] \cup \{\qrep{C_2}\}  \pmodels 

1755: \instthree(\qrep{C}) = \{\qrep{C}\}$.

1756: If $C'_1$ or $C'_2$ is non-empty.

1757: then $C[\varrone]$ is  of type C3, $S' \abss S$ and the first statement 

1758: holds.  If $C'_1$ and $C'_2$ are empty

1759: then $C$ is of type C1 and the second statement holds.

1760: 

1761: \item We do resolution between a clause $C_1[\varrone] = C'_1[\varrone]

1762: \lor D_1 \lor \pm P(\varrone)$ of type

1763: C1, and a clause $C_2[\varone,\ldots,\varr] = \mp P(x_1,\ldots,x_n) \lor 

1764: C'_2[\varone,\ldots,\varr] \lor D_2$  of type C4, both from $S$ upto renaming, 

1765: and the resolvent is $C[\varone,\ldots,\varr]

1766:  = C'_1[f(x_1,\ldots,x_n)] \lor C'_2[\varone,\ldots,\varr]\lor  D_1 \lor D_2$.

1767: (By ordering constraints we have chosen a non trivial literal from $C_2$

1768: for resolution). 

1769: No splitting or replacement rules apply and

1770:  ${S'} = S \cup \{C\}$. We have

1771: $\qrep{C_1}[\u] \cup \{\qrep{C_2}[\varone,\ldots,\varr]\} \supseteq

1772: \{\qrep{C_1}[f(x_1,\ldots,x_n)], \allowbreak

1773: \qrep{C_2}[\varone,\ldots,\varr]\}\pmodels 

1774: \qrep{C}[\varone,\ldots,\varr]$.

1775: Hence $\qrep{C_1}[\u] \cup \proj(\qrep{C_2}[\varone,\allowbreak \ldots,\varr]) \pmodels 

1776: \allowbreak \proj(\qrep{C}[\allowbreak \varone,\allowbreak \ldots,\varr])$ and

1777:  $\qrep{C_1}\allowbreak [\allowbreak \u\allowbreak [\allowbreak \ngrr \allowbreak \cup \allowbreak \ngrr\allowbreak [\ngrr[\gone]]] \cup 

1778: \qrep{C_2}[\ngrr \cup \ngrr[\ngrr[\gone]]]) \pmodels 

1779: \qrep{C}[\ngrr \cup \ngrr[\ngrr[\gone]]]$. Hence 

1780: $\inst(S) \supseteq \instone(\qrep{C_1}) \cup \instfour(\qrep{C_2}) \pmodels

1781: \instfour(\qrep{C})$.

1782: \begin{itemize}

1783: \item 

1784: Suppose $C'_1$ is non-empty or $C'_2$ has some non-trivial literal.

1785: Then $C$ is of type C4. 

1786: The only trivial literals in $C[\varone,\ldots,\varr]$ are those in 

1787: $C'_2[\varone,\ldots,\varr]$ and

1788: hence they involve predicates from $\mathbb P$. Hence $C[\varone,\ldots,\varr]$

1789: if of type C4 and the first statement holds.

1790: \item 

1791: Suppose $C'_1$ is empty and $C'_2$ has only trivial literals.

1792: Then $C[\varone,\ldots,\varr] =

1793: B_1[\varione] \sqcup \ldots \sqcup B_k[\varik] 

1794: \lor D_1 \lor D_2$ 

1795: where $1\le i_1,\ldots,i_k\le r$, and each $B_i$ is an $\epsilon$-block.

1796: The second statement holds.

1797: \end{itemize}

1798: 

1799: \item We do resolution between a clause $C_1[\varrone] =

1800: C'_1[\varrone] \lor D_1 \lor \pm P(s[\varrone])$ and a clause 

1801: $C_2[\varrone] = \mp P(t[\varrone]) \lor C'_2[\varrone] \lor D_2$,

1802: both of type C2, and both from $S$ upto renaming, and the resolvent is

1803: $C[\varrone]=C'_1[\varrone]\sigma\lor C'_2[\varrtwo]\sigma\lor  D_1\lor D_2$ 

1804: where $\sigma = mgu(s[\varrone],t[\varrtwo])$ (we renamed the 

1805: second clause before resolution). 

1806: We know that $s[\varrone], t[\varrone] \in \ngrone$, and by ordering constraints

1807: both $s$ and $t$ are non-trivial. By Lemma~\ref{lemma:sxty:red} 

1808: one of the following cases holds:

1809: \begin{itemize}

1810: \item $\varrone\sigma = \varrtwo\sigma = \varrone$. 

1811: $C[\varrone] = C'_1[\varrone] \lor C'_2[\varrone]$.

1812: Hence no splitting or replacement rules apply and $S' = S \cup \{C\}$.

1813: We have $\{C_1[\varrone],C_2[\varrone]\}\pmodels C[\varrone]$. 

1814: Hence $\insttwo(\qrep{C_1}[\varrone]) \cup \insttwo(\qrep{C_2}[\varrone]) 

1815: \pmodels \insttwo(\qrep{C}[\varrone]) \ni \qrep C[\varrone]$.

1816: If $C'_1$ or $C'_2$ contains some non-trivial literal 

1817: then $C[\varrone]$ is of type C2 and the first condition holds.

1818: If $C'_1$ and $C'_2$ contain only trivial literals then

1819: $C$ is of type C1 and the second condition holds.

1820: 

1821: \item $\varrone\sigma,\varrtwo\sigma \in \ngrr[\g] \subseteq \ngrr[\gone]$. 

1822: Then every literal in $C[\varrone]$ is of the

1823: form $\pm' Q(u)$ with $u\in \ngrone[\ngrr[\gone]]$.

1824: No splitting or replacement rules apply and $S' = S \cup \{C\}$.

1825: $\inst(S) \supseteq \qrep{C_1}[\ngrr[\gone]] \cup \qrep{C_2}[\ngrr[\gone]] 

1826: \pmodels \{\qrep{C}\} = \instthree(\qrep{C})$. 

1827: If $C'_1$ or $C'_2$ is non-empty then $C$ is of type

1828: C3 and the first statement holds.

1829: If $C'_1$ and $C'_2$ are empty then $C$ is of type C1 and the second statement

1830: holds.

1831: \end{itemize}

1832: 

1833: 

1834: \item We do resolution between a clause $C_1[\varrone] = C'_1[\varrone]

1835: \lor D_1 \lor \pm P(s[\varrone])$ of type C2, and a ground

1836: clause $\mp P(t) \lor C'_2 \lor D_2$ of type C3,

1837: both from $S$ upto renaming, and the resolvent is

1838: $C = C'_1[\varrone] \sigma \lor C'_2\lor  D_1 \lor D_2$ where $\sigma$ 

1839: is a unifier of $s[\varrone]$ and $t$. 

1840: We know that $s[\varrone]\in \ngrone$, $t\in \ngrone[\ngrr[\gone]]$,

1841: and by ordering constraints, $s$ is non-trivial.  We have the following cases:

1842: \begin{itemize}

1843: \item $t\in \gone$. Then $\varrone\sigma$ is a strict subterm of $t$ hence 

1844: $\varrone\sigma \in \g \subseteq \ngrr[\gone]$. 

1845: \item $t\in \ngrone[\ngrr[\gone]] \setminus \gone$. Hence we have $t=t_1[t']$

1846: for some non-trivial $t_1[\varrone]\in \ngrone$ and some $t'\in \ngrr[\gone]$. 

1847: Let $s' = \varrone\sigma$.

1848: As $s[s'] = t_1[t']$ hence $s[\varrone]$ and $t_1[\varrtwo]$ have a unifier

1849: $\sigma = \{\varrone\mapsto s', \varrtwo\mapsto t'\}$. From

1850: Lemma~\ref{lemma:sxty:red},  one of

1851: the following is true:

1852: \begin{itemize}

1853: \item $s[\varrone] = t_1[\varrone]$. Hence we

1854: have $\varrone\sigma = s'  = t' \in \ngrr[\gone]$.

1855: \item $\varrone\sigma_1, \varrtwo\sigma_1 \in \ngrr[\g] 

1856: \subseteq \ngrr[\gone]$. Hence $s'\in \ngrr[\gone]$. 

1857: \end{itemize}

1858: \end{itemize}

1859: In each case we have $\varrone\sigma = s'\in \ngrr[\gone]$. 

1860: Hence all literals in $C'_1[\varrone]\sigma$ are of the

1861: form $\pm Q(t)$ with $t\in \ngrone[\ngrr[\gone]]$. All literals

1862: in $C'_2$ are of the form $\pm' Q(t)$ with $t\in \ngrone[\ngrr[\gone]]$.

1863: Hence no splitting or replacement rules

1864: apply and ${S'} = S \cup \{C\}$. 

1865: $\inst(S) \supseteq \insttwo(\qrep{C_1}[\varrone]) \cup \instthree(\qrep{C_2}) 

1866: \supseteq \qrep{C_1}[\ngrr[\gone]] \cup \{\qrep{C_2}\}\pmodels \{\qrep{C}\} = 

1867: \instthree(\qrep{C})$.

1868: If $C'_1$ or $C'_2$ is non-empty then $C$ is of type C3

1869: and the first statement holds.

1870:  If $C'_1$ and $C'_2$ are empty then $C$ is of

1871: type C1 and the second statement holds.

1872: 

1873: 

1874: \item

1875: We do resolution between a clause $C_1[\varrone] = C'_1[\varrone] 

1876: \lor D_1 \lor \pm P(s[\varrone])$ of type C2,

1877: and a clause $C_2[\varone,\ldots,\varr] = \mp 

1878: P\allowbreak (\allowbreak f\allowbreak (\allowbreak x_1\allowbreak ,\allowbreak \ldots\allowbreak ,\allowbreak x_n\allowbreak )) \lor C'_2[\varone,\ldots,\varr] \lor D_2$ of type C4,

1879: both from $S$ upto renaming, and $\pm P(s[\varrone])$ and $\mp

1880: P(\allowbreak f(\allowbreak x_1,\allowbreak \ldots,\allowbreak x_n))$ are the literals resolved upon from the respective

1881: clauses. (By ordering constraints we have chosen a non-trivial literal to

1882: resolve upon in the second clause). 

1883: By  ordering constraints $s[\varrone]\in\ngrone$ is non-trivial. 

1884: Hence we have the following two cases for $s[\varrone] = 

1885: f(s_1[\varrone],\ldots,s_n[\varrone])$.

1886: 

1887: \begin{itemize}

1888: \item We have some $1\le i,j\le n$ such that

1889: $x_i=x_j$ but $s_i[\varrone]\neq s_j[\varrone]$. By Lemma~\ref{lemma:sxtx},

1890:  the only possible unifier of the terms

1891: $s[\varrone]$ and $f(x_1,\ldots,x_n)$ is $\sigma$ such that 

1892: $\varrone\sigma = g$ is a ground subterm

1893: of $s_i$ or $s_j$ and $x_k\sigma = s_k[g]$ for $1\le k\le n$.

1894: As $s[\varrone]\in \ngrone$, we have $g \in \g$ and

1895: each $s_k[\varrone] \in \ngrr \cup \g$. Hence $\varrone\sigma \in \g$ 

1896: and each $x_k\sigma \in \ngrr[\g] \cup \g \subseteq \ngrr[\gone]$. 

1897: The resolvent $C = C'_1[\varrone]\sigma \cup C'_2[\varone,\ldots,\varr]\sigma

1898: \lor  D_1 \lor D_2$ 

1899: is ground. 

1900: Each literal in $C'_1[\varrone]\sigma$ is of the

1901: form $\pm' Q(t)$ with $t\in \ngrone[\g] \subseteq \ngrone[\ngrr[\gone]]$. Each

1902: literal in $C'_2[\varone,\ldots,\varr]\sigma$  

1903: is of the form $\pm' Q(t)$ where the following cases can arise:

1904: \begin{itemize}

1905: \item $t = f'(x_{i_1},\ldots,x_{i_m})\sigma$ such that 

1906: $\{x_{i_1},\ldots,x_{i_m}\} = \{x_1,\ldots,x_n\}$. Then 

1907: $t = f'(s_{i_1},\ldots,s_{i_m})[g]\in \ngrone[\gone]\subseteq 

1908: \ngrone[\ngrr[\gone]]$.

1909: \item $t = x_k \sigma

1910: \in \ngrr[\gone]\subseteq \ngrone[\ngrr[\gone]]$ 

1911: for some $1\le k\le n$, where the literal

1912: $\pm' Q(x_k)$ is from $C_2$. 

1913: \end{itemize}

1914: We conclude that all non-splitting 

1915: literals in $C$ are of the form $\pm' Q(t)$ with

1916: $t\in \ngrone[\ngrr[\gone]]$, and no splitting or replacement rules apply. 

1917: We have ${S'} = S \cup \{C\}$.

1918: $\inst(S) \supseteq

1919: \insttwo(\qrep{C_1}[\varrone]) \cup \instfour(\qrep{C_2}[\varone,\ldots,\varr])

1920: \supseteq \qrep{C_1}[\ngrr[\gone]] \cup \qrep{C_2}[\ngrr[\gone]] \pmodels \{C\}

1921: =\instthree(C)$. 

1922: If $C'_1$ or $C'_2$  is non-empty then $C$ is of type C3, and the first

1923: statement holds.

1924: If $C'_1$ and $C'_2$ are empty then $C$ of type C1 and the second

1925: condition holds. 

1926: 

1927: \item For all $1\le i,j\le n$, if $x_i=x_j$ then

1928: $s_i[\varrone]=s_j[\varrone]$. 

1929: Then $s[\varrone]$ and $f(x_1,\ldots,x_n)$ have mgu $\sigma$ 

1930: such that $x_k\sigma = s_k[\varrone]\in \ngrr\cup \g$ for $1\le k\le n$ and 

1931: $x\sigma = x$ for $x \notin \{x_1,\ldots,x_n\}$.

1932: The resolvent $C[\varrone] = C'_1[\varrone] \lor C'_2\sigma\lor  D_1 \lor D_2$ is a 

1933: one-variable clause. 

1934: $\{C_1[\varrone]\}\cup C_2[\ngrr\cup\g] \pmodels C[\varrone]$. 

1935: All literals in $C'_1[\varrone]$ are of the form

1936: $\pm' Q(t)$ with $t\in \ngrone$, and no replacement rules

1937: apply on them. All literals in $C'_2[\varone,\ldots,\varr]\sigma$ 

1938: are of the form $\pm' Q(t[\varrone])$ where the following cases can arise:

1939: \begin{itemize}

1940: \item $t[\varrone] = f'(x_{i_1},\ldots,x_{i_m})\sigma$ such that 

1941: $\{x_{i_1},\ldots,x_{i_m}\} = \{x_1,\ldots,x_n\}$. Then $t[\varrone]\in 

1942: \ngrone$. No replacement rules apply on such a literal.

1943: \item $t[\varrone] = x_k \sigma = s_k[\varrone]\in \ngrr$ for some 

1944: $1\le k\le n$, where the literal

1945: $\pm' Q(x_k)$ is from $C_2$. Hence we must have $Q\in\mathbb P$. 

1946: Let $s_k[\varrone] = t_1[\ldots[t_p[\varrone]]\ldots]$ for some $p\ge 0$ 

1947: where each $t_i[\varrone]\in\ngr$ is non-trivial and reduced. Such a literal

1948: is replaced by the literal $\pm' \allowbreak Qt_1\ldots t_{p-1}\allowbreak (\allowbreak t_p\allowbreak [\allowbreak \varrone\allowbreak ]\allowbreak )$ and we 

1949: know that $t_p \in \ngr\subseteq \ngrone$.

1950: This new clause is obtained by propositional resolution between the former

1951: clause and clauses from $cl(\mathcal R)[\ngrr]$.

1952: \item $t[\varrone] = x_k \sigma = s_k\in \g$ for some 

1953: $1\le k\le n$, where the literal

1954: $\pm' Q(x_k)$ is from $C_2$. Hence we must have $Q\in\mathbb P$. 

1955: No replacement rules apply on such a literal.

1956: If $C$ contains only ground literals then

1957: this literal is left unchanged. Otherwise we perform

1958: $\grpreds$-splitting and this literal is replaced by the

1959: literal $- \ssp{\pm' Q(s_k)}$ and also a new clause $C'' = \ssp{\pm' Q(s_k)}

1960: \lor \pm' Q(s_k)$ of type C3 is added to $S$. If $C'$ is the new clause

1961: obtained by this splitting then $\qrep{C'}$ is clearly propositionally

1962: equivalent to the former clause. Also $\qrep{C''} = \mp' Q(s_k) \lor \pm'

1963: Q(s_k)$ is a propositionally valid statement.

1964: \end{itemize}

1965: We conclude that after zero or more replacement and splitting

1966: rules, we obtain a clause $C'[\varrone]$, 

1967: %all of whose literals are of the form $\pm'Q(t)$ with $t\in \ngrone$ or of the 

1968: %form $\pm q$ with $q\in\sspreds$, 

1969: together with a set $S''$ of clauses of type C3, 

1970: $\{\qrep C[\varrone]\} \cup cl(\mathcal R)[\ngrr]\pmodels

1971: \{\qrep{C}[\varrone]\}$, $\emptyset \pmodels \qrep{S''}$, and

1972: ${S'} = S \cup \{C'\}\cup S''$.

1973: %Also $S''=\emptyset$ if $C'$ is ground.

1974: $\{\qrep{C_1}[\varrone]\} \cup \qrep{C_2}[\ngrr \cup \g] 

1975: \cup cl(\mathcal R)[\ngrr]\pmodels \qrep{C'}[\varrone]$. 

1976: Hence $\inst(S) \supseteq \insttwo(\qrep{C_1}) \cup \instfour(\qrep{C_2})

1977: \supseteq \{\qrep{C_1}[\varrone]\} \cup \qrep{C_1}[\ngrr[\gone]]

1978: \cup \qrep{C_2}[\ngrr\cup\ngrr[\ngrr[\gone]]] 

1979: \cup cl(\mathcal R)[\ngrr] \cup cl(\mathcal R)[\ngrr[\ngrr[\gone]]]

1980: \pmodels \insttwo(\qrep{C'}) \cup \instthree(\qrep{S''}) = 

1981: \qrep{C'}[\varrone] \cup \qrep{C'}[\ngrr[\gone]] \cup \qrep{S''}$.

1982: If $C'$ is of type C2 or C3 then the first statement holds.

1983: Otherwise $C'$ is  of type C1 and the second statement holds.

1984: \end{itemize}

1985: 

1986: \item We do resolution between a clause $C_1 = C'_1 \lor D_1

1987: \lor \pm P(s)$ and a clause $C_2 = \mp P(s) \lor C'_2 \lor D_2$, 

1988: both ground clauses of type C3 from $S$, 

1989: and the resolvent is $C = C'_1 \lor C'_2\lor  D_1 \lor D_2$. 

1990: No replacement or splitting rules

1991: apply and we have ${S'} = S \cup \{C\}$. 

1992: $\inst(S) \supseteq \{\qrep{C_1},\qrep{C_2}\} \pmodels \instthree(\qrep C)

1993: = \{\qrep{C}\}$.  If $C'_1$ or $C'_2$ is non-empty then $C$ is of type C3,

1994:  and the first statement holds.

1995: If $C'_1$ and $C'_2$ are empty then $C$ is of type C1 and the second

1996: statement holds.

1997: 

1998: \item

1999: We do resolution between a ground clause $C_1 = C'_1 \lor D_1 \lor \pm P(s)$ of

2000: type C3, and a clause $C_2[\varone,\ldots,\varr] = \mp P(f(x_1,\ldots,x_n)) 

2001: \lor C'_2[\varone,\ldots,\varr] \lor D_2$ of type C4,

2002: both from $S$ upto renaming, and $\pm P(s)$ and $\mp

2003: P(f(x_1,\ldots,x_n))$ are the literals resolved upon from the respective

2004: clauses. We know that $s\in  \ngrone[\ngrr[\gone]]$. 

2005: Hence we have the following two cases for $s$.

2006: \begin{itemize}

2007: \item $s \in \ngrone[\ngrr[\gone]] \setminus \gone$. 

2008: Hence $s$ must be of the form

2009: $f(s_1,\ldots,s_n)[g]$ for some $f(s_1,\ldots,s_n)\in \ngrone$ and some 

2010: $g \in \ngrr[\gone]$ (The symbol $f$ is same as in the literal 

2011: $\mp P(f(x_1,\ldots,x_n))$ otherwise this resolution step would not be 

2012: possible). We have each $s_i \in \ngrr \cup \g$. The mgu $\sigma$ of $s$ and 

2013: $f(x_1,\ldots,x_n)$ is such that $x_i\sigma = s_i[g]\in \ngrr[\ngrr[\gone]]$.

2014: The resolvent $C = C'_1 \lor C'_2[\varone,\ldots,\varr]\sigma\lor  D_1 \lor D_2$

2015: is a ground clause. All literals in $C'_1$ are of the

2016: form $\pm' Q(t)$ with $t\in \ngrone[\ngrr[\gone]]$ hence no replacement

2017: rules apply on them.  The literals in $C'_2[\varone,\ldots,\varr]\sigma$ are of the form $\pm' Q(t)$

2018: where the following cases are possible:

2019: \begin{itemize}

2020: \item $t = f'(x_{i_1},\ldots,x_{i_m})\sigma$ where $\{x_{i_1},\ldots,x_{i_m}\}

2021: = \{x_1,\ldots,x_n\}$. Then $f'\allowbreak (\allowbreak s_{i_1}\allowbreak ,\allowbreak \ldots\allowbreak ,\allowbreak s_{i_m}\allowbreak ) \in \ngrone$. Hence

2022: $t \in \ngrone[\ngrr[\gone]]$. No replacement rules apply on such a literal.

2023: \item $t = x_i\sigma \in \ngrr[\ngrr[\gone]]$ for some

2024: $1\le i\le n$. If $t\in \ngrone[\ngrr[\gone]]$ then no replacement rules  apply

2025: on this literal. Otherwise suppose $t\in \ngrr[\ngrr[\gone]]\setminus

2026: \ngrone[\ngrr[\gone]]$. We have $t=t_1[\ldots[t_p[t']]\ldots]$ for some

2027: reduced non-trivial non-ground terms $t_1,\ldots,t_p\in \ngr$ with $p\ge 0$

2028: such that $t_1[\ldots[t_p[y]]] \in \ngrr$ and $t'\in \ngrr[\gone]$, and the

2029: replacement strategy replaces this literal by the literal 

2030: $\pm' Qt_1\ldots t_{p-1}(t_p[t'])$, and we know that

2031: $t_p\in \ngr \subseteq \ngrone$ so that $t_p[t']\in \ngrone[\ngrr[\gone]]$. 

2032: This new clause can be

2033: obtained by propositional resolution between the former clause and  clauses

2034: from $cl(\mathcal R)[\ngrr[\ngrr[\gone]]]$ 

2035: \end{itemize}

2036: We conclude that after zero or more replacement rules, we obtain a ground

2037: clause $C'$, all of whose non-splitting 

2038: literals are of the form $\pm' Q(t)$ with

2039: $t\in \ngrone[\ngrr[\gone]]$, and which is obtained by propositional resolution 

2040: from $\{C\} \cup cl(\mathcal R)[\ngrr[\ngrr[\gone]]]$. No splitting rules

2041: apply and ${S'} = S \cup \{C'\}$.  

2042: $\{\qrep{C_1}\} \cup \qrep{C_2}[\ngrr[\ngrr[\gone]]] \pmodels \qrep{C}$ hence

2043: $\inst(S) \supseteq \instthree(\qrep{C_1})\cup\instfour(\qrep{C_2}) \cup

2044: cl(\mathcal R)[\ngrr[\ngrr[\gone]]] \pmodels \instthree(\qrep{C'}) 

2045: = \{\qrep{C'}\}$.  If $C'_1$ or $C'_2$ is non-empty then

2046: $C$ is of type C3, and the first statement holds.

2047: If $C'_1$ and $C'_2$ are empty then $C$ is 

2048: of type C1 and the second statement holds.

2049: 

2050: \item $s \in \gone$. For the resolution step to be possible we must have

2051: $s = f(s_1,\ldots,s_n)$. Each $s_i \in \g$.

2052:  The mgu $\sigma$ of $s$ and 

2053: $f(x_1,\ldots,x_n)$ is such that each $x_i\sigma = s_i$.

2054: The resolvent $C = C'_1 \lor C'_2[\varone,\ldots,\varr]\sigma\lor  D_1 \lor D_2$ is a ground clause.

2055: All literals in $C'_1$ are of the

2056: form $\pm' Q(t)$ with $t\in \ngrone[\ngrr[\gone]]$.

2057:  The literals in $C'_2[\varone,\ldots,\varr]\sigma$ are of the form $\pm' Q(t)$

2058: where the following cases are possible:

2059: \begin{itemize}

2060: \item $t = f'(x_{i_1},\ldots,x_{i_m})\sigma$ where $\{x_{i_1},\ldots,x_{i_m}\}

2061: = \{x_1,\ldots,x_n\}$. Then $t = f'(s_{i_1},\ldots,s_{i_m}) \in \gone

2062: \subseteq \ngrone[\ngrr[\gone]]$.

2063: \item $t = x_i\sigma = s_i \in \g \subseteq \ngrone[\ngrr[\gone]]$ for some

2064: $1\le i\le n$.  

2065: \end{itemize}

2066: Hence all non-splitting

2067: literals in $C$ are of the form $\pm' Q(t)$ with $t\in 

2068: \allowbreak \ngrone\allowbreak [\allowbreak \ngrr\allowbreak [\allowbreak \gone\allowbreak ]\allowbreak ]$.

2069: No replacement rules or splitting rules apply and

2070: ${S'} = S \cup \{C\}$. 

2071: $\{C_1\} \cup C_2[\g] \pmodels C$ hence

2072: $\inst(S) \pmodels \instthree(\qrep C) = \{\qrep{C}\}$. 

2073: If $C'_1$ or $C'_2$ is non-empty then

2074: $C$ is of type C3 and the first statement holds.

2075: If $C'_1$ and $C'_2$ are empty then $C$ is

2076: of type C1 and the second statement holds.

2077: \end{itemize}

2078: 

2079: 

2080: 

2081: 

2082: 

2083: 

2084: \item We do resolution between two clauses $C_1[\varone,\ldots,\varr]$ and 

2085: $C_2[\varone,\ldots,\varr]$, both of type C4,

2086: and both from $S$ upto renaming. First we rename the second clause as 

2087: $C_2[\varrone,\ldots,\varrr]$ by applying the renaming $\sigma_0 =

2088: \{\varone\mapsto\varrone,\ldots,\varr\mapsto\varrr\}$.

2089: By ordering constraints, $C_1[\varone,\ldots,\varr] 

2090: = C'_1\allowbreak [\allowbreak \varone\allowbreak ,\allowbreak \ldots\allowbreak ,\allowbreak \varr\allowbreak ] \allowbreak \lor \allowbreak D_1

2091: \allowbreak \lor \allowbreak P(\allowbreak f(\allowbreak x_1,\allowbreak \ldots,\allowbreak x_n\allowbreak ))$

2092: and $C_2[\varrone,\ldots,\varrr] = - P(f(y_1,\ldots,y_n)) \lor C'_2[\varrone,\ldots,\varrr] \lor D_2$ and the resolvent is

2093: $C[\varone,\ldots,\varr] = C'_1[\varone,\ldots,\varr]\sigma \lor C'_2[\varrone,\ldots,\varrr]\sigma

2094: \lor D_1 \lor D_2$ 

2095: where, by Lemma~\ref{lemma:sequnif}, $\sigma$ is such that

2096: $\{x_1,\ldots,x_n\}\sigma \subseteq \{x_1,\ldots,x_n\}$ and 

2097: $y_i\sigma = x_i$ for $1\le i\le n$.

2098: $\proj(C_1) \cup \proj(C_2) \pmodels C[\varone,\ldots,\varr]$.

2099: Hence $\inst(S) \supseteq \instfour(\qrep{C_1}[\varone,\ldots,\varr]) \cup

2100: \instfour\allowbreak (\allowbreak \qrep{C_2}\allowbreak [\varone\allowbreak ,\allowbreak \ldots\allowbreak ,\allowbreak \varr\allowbreak ]\allowbreak ) =

2101: \proj(\qrep{C_1}[\varone,\ldots,\varr]) \allowbreak \cup \allowbreak \qrep{C_1}[\ngrr \allowbreak \cup \allowbreak \ngrr[\ngrr[\allowbreak \gone]]]

2102: \cup \proj(\qrep{C_2}[\varone,\ldots,\allowbreak \varr\allowbreak ]) \allowbreak \cup\allowbreak  \qrep{C_2}[\allowbreak \ngrr\allowbreak  \cup \allowbreak \ngrr[\allowbreak \ngrr[\allowbreak \gone]]]

2103: \allowbreak  \pmodels \allowbreak  \proj(\qrep{C}[\varone,

2104: \allowbreak  \ldots,\allowbreak  \varr]) \cup \qrep{C}[\ngrr\cup\ngrr[\ngrr[\gone]]] = \instfour(\qrep{C}[\varone,\ldots,\varr])$.

2105: \begin{itemize}

2106: \item Suppose $C'_1$ or $C'_2$ has a non-trivial literal. Then $C$ is of type

2107: C4, no replacement or splitting rules apply, 

2108: $S' = S \cup \{C\}$ and the first statement holds.

2109: \item Suppose $C'_1$ and $C'_2$ contain no non-trivial literal. Then $C[\varone,\ldots,\varr] = 

2110: B_1[\varione] \sqcup \ldots \sqcup B_k[\varik]\lor D_1 \lor D_2$ 

2111: with $1\le i_1,\ldots,i_k\le r$, each $B_i$ being an $\epsilon$-block. 

2112: No splitting or replacement rules apply ($\epsilon$-splitting is forbidden

2113: by $\phi_0$), and $S' = S \cup \{C\}$. The second statement holds.

2114: \end{itemize}

2115: 

2116: \item We do a resolution step in which one of the premises is a clause from

2117: $cl(\mathcal R)$. Every clause in $cl(\mathcal R)$ is of type C2.

2118: Also trivially $\insttwo(C) \subseteq \inst(T)$.

2119: Hence this case can be dealt with in the same way

2120: as in the case  where one of the premises of resolution is a clause

2121: of type C2.

2122: \end{enumerate}

2123: 

2124: Next we consider factoring steps.

2125: Factoring on a clause of type C1 or C3 is possible only if the two

2126: involved literals are the same, hence this is equivalent to doing nothing.

2127: 

2128: \begin{enumerate}

2129: \item We do factoring on a clause $C_1[\varrone] = C'_1[\varrone] 

2130: \lor \pm P(s[\varrone])\lor \pm P(t[\varrone])$

2131: of type C2, and from $S$ upto renaming. 

2132: We know that $s[\varrone],t[\varrone]\in \ngrone$, and by 

2133: ordering constraints $s$ and $t$ are non trivial. 

2134: The clause obtained is

2135: $C[\varrone] = C'_1[\varrone]\sigma \lor \pm P(s[\varrone])\sigma$ 

2136: where $\sigma$ is a unifier of $s[\varrone]$ and $t[\varrone]$.

2137: If $s[\varrone]\neq t[\varrone]$ 

2138: then by Lemma~\ref{lemma:sxtx} 

2139: $\varrone\sigma$ is a ground strict subterm of $s$ or $t$, 

2140: hence $\varrone\sigma \in \g

2141: \subseteq \ngrr[\gone]$. Each literal in $C$ is of the form $\pm' Q(t')$ where

2142: $t'\in \ngrone[\ngrr[\gone]]$. Hence $C$ is of type C3. No splitting or

2143:  replacement rules apply and ${S'} = S \cup \{C\}$.

2144: We have $C \in C_1[\ngrr[\gone]]$.

2145: $\inst(S) \supseteq \insttwo(\qrep{C_1}[\varrone])

2146: \supseteq\qrep{C_1}[\varrone][\ngrr[\gone]] \supseteq\instthree(C)=\{\qrep C\}$.

2147: The first statement holds.

2148: 

2149: \item We do factoring on a clause $C_1[\varone,\ldots,\varr]$

2150: of type C4, and from $S$ upto renaming, 

2151: to obtain the clause $C[\varone,\ldots,\varr]$.

2152: By ordering constraints non-trivial literals must be chosen for factoring.

2153: Then $C[\varone,\ldots,\varr]$ is again of type C4 and $C[\varone,\ldots,\varr]

2154: \in \proj(C_1)$.

2155: $\inst(S) \supseteq \instfour(\qrep{C_1}) = 

2156: \proj(\qrep{C_1}) \cup \qrep{C_1}[\ngrr\cup

2157: \ngrr[\ngrr[\gone]]] \pmodels \instfour(\qrep{C})$. 

2158: The first statement holds.

2159: \qed

2160: \end{enumerate}

2161: \endproof 

2162: \restorelemmacounter

2163: 

2164: The alternative resolution procedure for testing unsatisfiability by using

2165: succinct representations of tableaux is now defined by the rule:

2166: $\mathcal T \mid S \absres \mathcal T \mid S \cup \{B_1 \sqcup D\} 

2167: \mid S\cup\{B_2\}\mid\ldots \mid S \cup \{B_k\}$ 

2168: whenever $\inst(S) \pmodels B_1\sqcup \ldots

2169: \sqcup B_k \sqcup \qrep{D}$, each $B_i$ is an $\epsilon$-block, 

2170: $1\le i_1,\ldots,i_k \le r$ and $D \subseteq \pm\sspreds$.

2171: The simulation property now states:

2172: 

2173: 

2174: 

2175: \newcounter{lemnhsimul}

2176: \namelem{lemnhsimul}

2177: \def\lemnhsimulstatement{

2178: If $S \abss T$ and $S\subordselfssplreplres{\mathcal T}$ then 

2179: $T \absres^* {\mathcal T}'$ for some ${\mathcal T}'$ such that $\mathcal T \abss

2180: \mathcal T'$.

2181: }

2182: \begin{lemma}

2183: \label{lemma:nhsimul}

2184: \lemnhsimulstatement

2185: \end{lemma}

2186: \proof

2187: As $S\subordselfssplreplres{\mathcal T}$, we have some $S'$ such that

2188: $S\subordselnosplreplres S'$ and $\mathcal T$ is obtained from $S'$ by

2189: $\epsilon$-splitting steps.  From Lemma~\ref{lemma:nhresol},

2190: one of the following cases holds.

2191: \begin{itemize}

2192: \item   $S' \abss S$. Then $S'$ contains only clauses of type

2193: C1-C4 and no $\epsilon$-splitting is applicable. Hence $\mathcal T = S'

2194: \abss S$. As $\mathcal T \abss S$ and $S \abss T$ hence

2195: $\mathcal T \abss T$ because of transitivity of $\abss$. 

2196: Thus $T$ is the required $\mathcal T'$.

2197: \item  $S' = S \cup \{C\}\cup S''$, $C$ is a renaming of

2198: $B_1[\varione] \sqcup \ldots\sqcup B_k[\varik] \sqcup D$ where each

2199: $B_i$ is an $\epsilon$-block, $1\le i_1,\ldots,i_k\le r$, $D \subseteq\pm

2200: \sspreds$, $\inst(S) \pmodels \qrep C$ and $S''$ is a set of clauses of type

2201: C3 and $\emptyset \pmodels \qrep{S''}$. We have $\mathcal T =

2202: S \cup S'' \cup \{B_1 \sqcup D\} 

2203: \mid S\cup S'' \cup \{B_2\}\mid\ldots\mid S \cup S'' \cup \{B_k\}$.

2204: We have $S \cup S'' \cup \{B_1\sqcup D\} \abss T \cup \{B_1 \sqcup D\}$ and

2205: $S \cup S'' \cup \{B_i\} \abss T \cup \{B_i\}$ for $1\le i\le k$.

2206: We show that the required $\mathcal T'$ is $T \cup \{B_1\sqcup D\} \mid

2207: T \cup \{B_1\} \mid \ldots \mid S \cup S'' \cup \{B_k\}$.

2208: As $S \abss T$ hence $\inst(T) \pmodels \inst(S)\pmodels \qrep C$. 

2209: Hence $T \absres \mathcal T'$.\qed

2210: \end{itemize}

2211: \endproof

2212: 

2213: 

2214: Hence as for flat clauses we obtain:

2215: 

2216: \newcounter{thcsat}

2217: \nameth{thcsat}

2218: \def\thcsatstatement{

2219: Satisfiability for  the class $\c$ is NEXPTIME-complete.

2220: }

2221: \savethcounter

2222: \putth{thcsat}

2223: \begin{theorem}

2224: \label{theorem:csat}

2225: \thcsatstatement

2226: \end{theorem}

2227: \proof 

2228: Let $S$ be a finite set in $\c$ whose satisfiability we want to show.

2229: We proceed as in the proof of Theorem~\ref{theorem:flatsat}. Wlog if $C\in S$

2230: then $C$ is either a complex clause or

2231: a one-variable clause. Clearly

2232: $S$ is satisfiable iff $S \cup cl(\mathcal R)$ is satisfiable. At the beginning

2233: we apply 

2234: the replacement steps using $\mathcal R$ as long as  possible and then

2235: $\grpreds$-splitting as long as possible.

2236: Hence wlog all clauses in $S$ are of type C1-C4.

2237: Then we non-deterministically add a certain number of clauses

2238: of type C1 to S. Then we check that the resulting set  $S'$

2239: does not contain $\empcl$, and is saturated in the sense

2240: that: if $C = B_1[\varione]\sqcup \ldots \sqcup

2241: B_k[\varik]\sqcup D$, each $B_i$

2242: is an $\epsilon$-block, $1\le i_1,\ldots,i_k\le r$, $D\subseteq\pm\grpreds$,

2243:  and $B_j[\varrone]

2244: \notin S'$ for $1\le j\le k$, then $\inst(S') \pnmodels \qrep{C}$.

2245: There are exponentially many such $C$ to check for since the number of

2246: splitting literals in polynomially many. The size of

2247: $\inst(S')$ is exponential.\qed

2248: \endproof 

2249: 

2250: 

2251: 

2252: 

2253: \section{The Horn Case}

2254: \label{sec:horn}

2255: 

2256: We show that in the Horn case, the upper bound can be improved to DEXPTIME.

2257: The essential idea is that propositional satisfiability of Horn clauses is

2258: in PTIME instead of  NPTIME. But now we need to eliminate the 

2259: use of tableaux altogether. 

2260: To this end, we replace the $\epsilon$-splitting rule of 

2261: Section~\ref{sec:nh} by splitting-with-naming. Accordingly we instantiate the

2262: set $\sspreds$ used in Section~\ref{sec:nh} as 

2263: $\sspreds = \grpreds \cup\epspreds$ where

2264: $\epspreds = \{\ssp{C} \mid C \textrm{ is a non-empty negative 

2265: $\epsilon$-block with predicates from }\mathbb P\}$. 

2266: We know that binary resolution and factorization on Horn clauses produces 

2267: Horn clauses.  Replacements on Horn clauses

2268: using the rules from $\mathcal R$ produces Horn clauses.

2269: $\epspreds$-splitting on Horn clauses produces Horn clauses. E.g. clause

2270: $P(\varone) \lor -Q(\varone) \lor -R(\vartwo)$ produces

2271: $P(\varone) \lor -Q(\varone) \lor -\ssp{-R(\vartwo)}$ and $\ssp{-R(\vartwo)}

2272: \lor - R(\vartwo)$.

2273: $\grpreds$-splitting on $P(f(x)) \lor -Q(a)$ produces

2274: $P(f(\varone)) \lor -\ssp{-Q(a)}$ and $\ssp{-Q(a)} \lor -Q(a)$ which are Horn.

2275: However $\grpreds$-splitting on $C = -P(f(\varone)) \lor Q(a)$ produces

2276: $C_1 = -P(f(\varone)) \lor -\ssp{Q(a)}$ and $C_2 = \ssp{Q(a)} \lor Q(a)$. $C_2$

2277: is not Horn. However $\qrep{C_1} = C$ and $\qrep{C_2} = -Q(a)\lor Q(a)$ are

2278: Horn. Finally, as $\epspreds$ has exponentially many atoms, 

2279: we must restrict their occurrences in clauses. Accordingly, for $1\le i\le4$,

2280: define clauses of type C$i$' to be clauses $C$ of the type C$i$, 

2281: such that $\qrep{C}$ is Horn and has at most $r$ negative literals 

2282: from $\epspreds$.

2283: ($\qrep{C}$ is defined as before, hence it leaves atoms from $\epspreds$ 

2284: unchanged).  Now the $\sspreds$-splitting-replacement strategy $\phi_h$ 

2285: first applies

2286: the replacement steps of Section~\ref{sec:nh} as long as possible, then applies

2287: $\grpreds$-splitting as long as possible and then applies 

2288: $\epspreds$-splitting as long as possible.

2289: Succinct representations are now defined as: $S \absh T$ iff for each

2290: $C\in S$, $C$ is of type C$i$' and satisfies P$i_T$ for some $1\le i\le 4$.

2291: The abstract resolution procedure is defined as:

2292: $T \absresh T \cup \{B_1\lor -q_2\lor \ldots \lor -q_k 

2293: \sqcup D\sqcup E\} \cup \{\ssp{B_i} \lor B_i \mid 2\le i\le k\}$ whenever

2294: $\inst(T) \pmodels \qrep{C}$,

2295: $C = B_1[\varione] \sqcup \ldots \sqcup B_k[\varik]\sqcup D\sqcup E$,

2296: $\qrep{C}$ is Horn, $1\le i_1,\ldots,i_k\le r$,

2297: $B_1$ is an $\epsilon$-block, $B_i$ is a negative $\epsilon$-block and

2298: $2\le i\le k$, $D \subseteq \pm \grpreds$

2299: and $E\subseteq \pm\epspreds$ such that if $k=1$ then $E$ has at most 

2300: $r$ negative literals, and if $k>1$ then $E$ has no negative literal.

2301: The $\abss$ and $\absres$ relations are as in Section~\ref{sec:nh}.

2302: 

2303: 

2304: \newcounter{lemhresol}

2305: \namelem{lemhresol}

2306: \def\lemhresolstatement{

2307: If $S \absh T$ and $S \subordselfssplreplresh S_1$ then

2308: $T \absresh^* T_1$ and $S_1\absh T_1$ for some $T_1$.

2309: }

2310: \begin{lemma}

2311: \label{lemma:hresol}

2312: \lemhresolstatement

2313: \end{lemma}

2314: \proof

2315: Let $\phi_0$ be as in Section~\ref{sec:nh}.

2316: As $S \subordselfssplreplresh S_1$ hence we have some $S'$ such that 

2317: $S \subordselnosplreplres S'$ and

2318: $S_1$ is obtained from $S'$ by applying $\epspreds$-splitting steps.

2319: As discussed above, all clauses $C\in S_1\cup S'$ 

2320:  are such that $\qrep{C}$ is also Horn.

2321: If $S'$ is obtained by resolving upon splitting literals, 

2322: then one of the premises must

2323: be just a positive splitting literal. The other premise has at most

2324: $r$ literals of the form $-q$ with $q\in\epspreds$, 

2325: hence the resolvent has at most $r$  literals of the form $-q$ with

2326: $q\in\epspreds$. In case non-splitting literals are resolved upon then the

2327: premises cannot have any negative splitting literal and the resolvent has

2328: no negative splitting literal.  $\grpreds$-splitting does not create

2329: literals from $\pm\epspreds$. Hence all clauses in $S'$ have at most $r$

2330: literals of the form $-q$ with $q\in\epspreds$.

2331: Now by Lemma~\ref{lemma:nhresol}, one of the following conditions holds.

2332: \begin{itemize}

2333: \item $S'\abss S$. Then $\epspreds$-splitting is not applicable on clauses in

2334: $S'$ and $S_1 = S' \abs S$. From transitivity of $\abs$ we have

2335: $S_1 \abs T$.  Then from the above discussion we conclude that $S_1 \absh T$.

2336: 

2337: \item $S' = S \cup \{C\} \cup S''$, $C$ is a renaming of

2338: $B_1[\varione]\sqcup \ldots \sqcup

2339: B_k[\varik]\sqcup D$, each $B_i$ is an $\epsilon$-block, 

2340: $1\le i_1,\ldots,i_k\le r$, $D \subseteq\pm\sspreds$,

2341: $\inst(S) \pmodels \qrep C$, and $S''$ is a set of clauses of type C3 and

2342: $\emptyset \pmodels \qrep{S''}$. Also if $k\ge 2$ then $D$ has no 

2343: literals $-q$ with  $q\in \epspreds$.  As $C$ is Horn,

2344: wlog $B_i$ is negative for $i\ge 2$. Hence

2345: $S_1 = S' \cup \{B_1 \lor -q_2\lor \ldots \lor -q_k\sqcup D\} \cup 

2346: \{\ssp{B_i} \cup B_i \mid 2\le i\le k\}$.

2347: We show that the required $T_1$ is $T \cup 

2348: \{B_1 \lor -q_2\lor \ldots \lor -q_k\sqcup D\} \cup \{\ssp{B_i} \cup B_i \mid

2349: 2\le i\le k\}$. Each $\ssp{B_i} \cup B_i$ is of type C1'. 

2350: As $C \in S'$ hence $D$ has at most $r$ literals $-q$ with

2351: $q\in\epspreds$.  Hence if $k=1$ then

2352: $B_1 \lor -q_2\lor \ldots \lor -q_k\sqcup D$ is also of type C1'.

2353: If $k\ge 2$ then $D$ has no negative literals $-q$ with $q\in\epspreds$,

2354: and $B_1 \lor -q_2\lor \ldots \lor -q_k\sqcup D$ is again of type C1' since

2355: $k\le r$.  As $S \absh T$ we have $\inst(T) \pmodels \inst(S) \pmodels \qrep C$.

2356: Hence $T \absresh T_1$. Finally, clearly $S_1 \abss T_1$ hence

2357: $S_1 \abss_h T_1$.\qed

2358: \end{itemize}

2359: \endproof

2360: 

2361: Now for deciding satisfiability of a set of flat and one-variable clauses we 

2362: proceed as in the non-Horn case. But now instead of 

2363: non-deterministically adding clauses,

2364: we compute a sequence $S = S_0 \absresh S_1 \absresh S_2 \ldots$ starting from 

2365: the given set $S$, and proceeding don't care non-deterministically, till no more clauses can be 

2366: added, and then check whether

2367: $\empcl$ has been generated.

2368: The length of this sequence is at most exponential.

2369: Computing $S_{i+1}$ from $S_i$ requires at most exponential time because

2370: the number of possibilities for $C$ in the definition of $\absres$ above

2371: is exponential.

2372: (Note that this idea of 

2373: $\epspreds$-splitting would not have helped in the non-Horn 

2374: case because we cannot

2375: bound the number of positive splitting literals in a clause in the

2376: non-Horn case, whereas Horn clauses by definition have at most one positive 

2377: literal).  Also note  that APDS can be encoded using flat Horn clauses. Hence:

2378: 

2379: \begin{theorem}

2380: \label{theorem:chsat}

2381: Satisfiability for the classes $\ch$ and $\flath$ is DEXPTIME-complete.

2382: \end{theorem}

2383: 

2384: 

2385: Together  with Theorem~\ref{th:hardness}, this gives us optimal complexity for

2386: protocol verification:

2387: \begin{theorem}

2388: Secrecy of cryptographic protocols with single blind copying, with bounded

2389: number of nonces but unbounded number of sessions is DEXPTIME-complete.

2390: \end{theorem}

2391: 

2392: 

2393: \subsection{Alternative Normalization Procedure} 

2394: 

2395: While 

2396: Theorem~\ref{theorem:chsat} gives us the optimum complexity for the Horn case,

2397: we outline here an alternative normalization procedure for deciding 

2398: satisfiability in the Horn case, in the style of~\cite{seidl:h1}. 

2399: Our goal is to show that the Horn case can be dealt with using simpler 

2400: techniques. This may also be interesting for implementations, since it avoids 

2401: exhaustive generation of instantiations of clauses. 

2402: Since we already have the optimum complexity from 

2403: Theorem~\ref{theorem:chsat}, we restrict ourselves to giving only the

2404: important ideas here.  Define 

2405: {\em normal} clauses to be clauses which have no function symbol in the

2406: body, have no repetition of variables in the body, and have no variables in the

2407: body other than those in the head. Sets of normal definite

2408: clauses involving unary predicates can be thought of

2409: as generalizations of tree automata, by adopting the convention that term $t$ is

2410: {\em accepted} at {\em state} $P$ iff atom $P(t)$ is reachable.

2411: I.e. states are just unary predicates. {\em (Intersection-)emptiness}

2412: and {\em membership} properties are defined as usual.

2413: 

2414: \begin{lemma}

2415: Emptiness and membership properties are decidable in polynomial time for 

2416: sets of normal definite clauses.

2417: \end{lemma}

2418: \proof

2419: Let $S$ be the set of clauses.

2420: To test emptiness of a state $P$, we remove arguments of predicate symbols

2421: in clauses, and treat predicates as proposition symbols. Then we add the clause

2422: $- P$ and check satisfiability of the resulting propositional Horn clause set.

2423: 

2424: To test if $t$ is accepted at $P$, 

2425: let $T$ be the set of subterms of $t$.

2426: Define a set $S'$ of clauses as follows. If $Q(s)\lor -Q_1(x_1)\lor \ldots \lor

2427: -Q_n(x_n) \in S$ and $s\sigma \in T$ for some substitution $\sigma$ then

2428: we add the Horn clause $Q(s\sigma) \lor -Q_1(x_1\sigma) \lor \ldots \lor

2429: -Q_n(x_n\sigma)$   to $S'$. Finally we add $- P(t)$ to $S'$

2430: and test its unsatisfiability.  $S'$ is computable in polynomial time. 

2431: Also $S'$ has only ground clauses, hence satisfiability is equivalent to

2432: propositional unsatisfiability, by treating each ground literal as a 

2433: propositional symbol.\\

2434: \strut \hfill  \qed

2435: \endproof

2436: 

2437: The intuition behind the normalization procedure is as follows. 

2438: We use new states which are sets $\{P_1,P_2,\ldots,\}$, where $P_1,P_2,\ldots$

2439: are states in the given clauses set.

2440: The state $\{P_1,P_2,\ldots,\}$ represents intersection of the states

2441: $P_1,P_2,\ldots$. These new states are denoted by $p,q,p_1,\ldots$.

2442: The states $P$ in clauses are replaced by $\{P\}$.  We try to make

2443: non-normal clauses redundant by resolving them with normal clauses.

2444: Hence a clause $C \lor -p(t)$, where $t$ has some function symbol, is resolved

2445: with a normal clause $p(s) \lor D$ to obtain a clause $C\sigma \lor D\sigma$ 

2446: where $\sigma=mgu(s,t)$. Normal clauses $p(s) \lor C$ and $p(t) \lor D$ are

2447: used to produce clause $(p\cup q)(s\sigma) \lor C\sigma \lor D\sigma$ where

2448: $\sigma = mgu (s,t)$. In this process if we get a clause $C \lor -p(t)$

2449: where $t$ is ground, then either $t$ is accepted at $p$ using the normal 

2450: clauses and we remove the literal $-p(t)$ from the clause, or $t$ is not 

2451: accepted at $p$ using the normal clauses, and we reject the clause.

2452: From clauses $C \lor -p(x) \lor -q(x)$ we derive the clause 

2453: $C \lor -(p\lor q)(x)$. If a clause $p(x_1) \lor -q(x_1) \lor -q_1(x_2)\lor 

2454: \ldots\lor -q_n(x_n)$ is produced where the $x_i$ are mutually distinct, then

2455: either each $q_i$ is non-empty using the normal clauses and we replace this

2456: clause by $p(x) \lor -q(x)$, or we reject this clause.  The normal clauses

2457: $p(x) \lor -q(x)$ and $q(t) \lor C$ produce the clause $q(t) \lor C$.

2458: Replacement rules are also applied as in the non-Horn case. We continue this

2459: till no more new clauses can be produced. Then we remove all non-normal

2460: clauses. We claim that this process takes exponential time and 

2461: each state $p$ in the resulting clause set accepts exactly the terms accepted

2462: by each $P\in p$ in the original clause set. This also gives us a DEXPTIME

2463: algorithm for the satisfiability problem for the class $\c$.

2464: 

2465: 

2466: 

2467: \begin{example}

2468: Consider the set $S = \{C_1,\ldots,C_5\}$ of clauses where

2469: $$\begin{array}{l r l}

2470: C_1 = & P (a) & \\

2471: C_2 = & Q (a) & \\

2472: C_3 = & P(f(g(\varone,a),g(a,\varone),a)) & \lor -P (\varone)\\

2473: C_4 = & P(f(g(\varone,a),g(a,\varone),b)) & \lor -P (\varone)\\

2474: C_5 = & R (\varone) & \lor -P (f(\varone,\varone,\vartwo)) \lor -Q(\vartwo)

2475: \end{array}$$

2476: We first get the following normal clauses.

2477: $$\begin{array}{l r l}

2478: C'_1 = & \{P\} (a) & \\

2479: C'_2 = & \{Q\} (a) & \\

2480: C'_3 = & \{P\}(f(g(\varone,a),g(a,\varone),a)) & \lor -\{P\} (\varone)\\

2481: C'_4 = & \{P\}(f(g(\varone,b),g(a,\varone),b)) & \lor -\{P\} (\varone)\\

2482: \end{array}$$

2483: The clause

2484: $$C'_5=\{R\}(\varone)  \lor -\{P\} (f(\varone,\varone,\vartwo)) \lor -\{Q\}(\vartwo)$$

2485: is not normal. Resolving it with $C'_3$ gives the clause

2486: $$\{R\}(g(a,a)) \lor -\{P\}(a) \lor -\{Q\}(a)$$ 

2487: As $a$ is accepted at $\{P\}$ and $\{Q\}$ using the

2488: normal clauses $C'_1$ and $C'_2$, hence we get a new normal clause 

2489: $$C_6 = \{R\}(g(a,a))$$

2490: Resolving $C'_5$ with $C'_4$ gives 

2491: $$\{R\}(g(a,a)) \lor -\{P\}(a) \lor -\{Q\}(b)$$

2492: But $b$ is not accepted at $\{Q\}$ using the normal clauses hence this clause

2493: is rejected. Finally $C'_1$ and $C'_2$ also give the normal clause

2494: $$C_7 = \{P,Q\}(a)$$

2495: The resulting set of normal clauses is $\{C'_1,\ldots,C'_4,C_6,C_7\}$.

2496: 

2497: \end{example}

2498: 

2499: 

2500: %\def\bigp{\mathcal P}

2501: %The normalization procedure works as follows. We start with a set of flat

2502: %and one-variable clauses on set of states $\mathbb P$. We define the sets

2503: %$\mathbb Q, \ngr,\ngrr$ etc as in the non-Horn case.

2504: %For simplicity we assume that no clause has a negative ground literal. This will

2505: %be true also of new clauses generated.  Define $\bigp = 2^{\mathbb P}$ be a

2506: %set of fresh states. Initially we replace each state $P\in\mathbb P$ 

2507: %in clauses by the state $\{P\}\in\bigp$. For a clause set $\mathcal A$ we denote

2508: %by $\mathcal{A}_{norm}$ the set of normal clauses in $\mathcal A$. 

2509: %Initially we add to the given set $\mathcal A$, a set of flat clauses so that

2510: %the state $\{\}\in\bigp$ accepts all terms.  We add to $\mathcal A$ the clauses

2511: %of $cl(\mathcal R)$ as in Section~\ref{sec:nh}. Hence wlog we assume that all 

2512: %non-ground literals in one-variable clauses have only reduced arguments.

2513: %We then apply

2514: %the following steps to add new clauses to the set $\mathcal A$.

2515: %\noindent

2516: %\begin{enumerate}

2517: %\item 

2518: %\label{norm:union}

2519: %Given clauses $p(s) \lor C_1, q(t) \lor C_2\in\mathcal{A}_{norm}$, 

2520: %renamed apart, we

2521: %create the clause $C = (p\cup q)(s\sigma) \lor C_1\sigma \lor C_2\sigma$ where

2522: %$\sigma = mgu(s,t)$. We have the following cases.

2523: %\begin{itemize}

2524: %\item $C$ is a flat clause. Then we add it to $\mathcal A$.

2525: %\item $C$ is (a renaming of) a clause $p(\varone) \lor \bigvee_{1\le i\le n}

2526: %\bigvee_{1\le j\le k_i}-p^j_i(\vari)$ and the state $\bigcup p^j_i$ is non-empty

2527: %in $\mathcal{A}_{norm}$ for $2\le i\le n$ then we add the clause

2528: %$p(\varone) \lor -(\bigcup_{1\le j\le k_1}p^j_i)(\varone)$ to $\mathcal A$. 

2529: %\item Suppose $C$ is a one-variable clause $C' \lor -p_1(t_1)\lor \ldots\lor 

2530: %-p_n(t_n)$ where $C$ has no ground negative literals, each $t_i$ is ground

2531: %and is accepted at $p_i$ in $\mathcal{A}_{norm}$. Each literal 

2532: %$\pm \{P_1,\ldots,P_k\}(t_1[\ldots[t_p[x]]ldots])$ in $C'$, 

2533: %where each $t_i$ is reduced,

2534: %is replaced by the literal $\pm \{P_1t_1\ldots t_{p-1},\ldots,

2535: %P_kt_1\ldots t_{p-1}\}(t_p[x])$. The resulting clause $C''$ is added to 

2536: %$\mathcal A$.

2537: %\item In all other cases the clause $C$ is not added to $\mathcal A$.

2538: %\end{itemize}

2539: %\item

2540: %\label{norm:propogate}

2541: %Given clauses $p(x) \lor -q(x), q(t) \lor C\in\mathcal A$ we add the clause

2542: %$p(t) \lor C$ to $\mathcal A$.

2543: %\item

2544: %\label{norm:resolve}

2545: %Given clauses $C \lor -p(t)$

2546: %

2547: %\end{enumerate}

2548: 

2549: 

2550: 

2551: 

2552: \section{Conclusion}

2553: 

2554: We have proved DEXPTIME-hardness of  secrecy for cryptographic 

2555: protocols with single blind copying,

2556: and have improved the upper bound from 3-DEXPTIME to DEXPTIME.  

2557: We have improved the 3-DEXPTIME upper bound for satisfiability for the class 

2558: $\c$ to

2559: NEXPTIME in the general case and DEXPTIME in the Horn case, which match

2560: known lower bounds. For this we have

2561: invented new resolution techniques like ordered resolution with 

2562: splitting modulo propositional reasoning, ordered literal replacements and

2563: decompositions of one-variable terms. As byproducts we obtained optimum

2564: complexity for several fragments of $\c$ involving flat and one-variable

2565: clauses. Security for several other decidable classes of protocols 

2566: with unbounded number of sessions and bounded number of nonces

2567: is in DEXPTIME, suggesting that 

2568: DEXPTIME is a reasonable 

2569: complexity class for such  classes of protocols.

2570: 

2571: \bibliographystyle{abbrv}

2572: \bibliography{fov}

2573: 

2574: 

2575: 

2576: 

2577: 

2578: 

2579: 

2580: 

2581: 

2582: 

2583: \appendix

2584: 

2585: 

2586: \section{Proofs of Section~\ref{sec:onevar}}

2587: \label{appone}

2588: 

2589: We use the following unification algorithm, due to

2590: Martelli and Montanari.

2591:   It is described by the

2592:   following rewrite rules on finite multisets of equations between terms; we

2593:   let $M$ be any such multiset, and comma denote multiset union:

2594:   \begin{description}

2595:   \item[(Delete)] $M, u \doteq u \to M$

2596:   \item[(Decomp)] $M, f (u_1, \ldots, u_n) \doteq f (v_1, \ldots, v_n) \to M,

2597:     u_1\doteq v_1, \ldots, u_n\doteq v_n$

2598:   \item[(Bind)] $M, x \doteq v \to M [x:=v], x \doteq v$ provided $x$ is not

2599:     free in $v$, but is free in $M$.

2600:   \item[(Fail1)] $M, x \doteq v \to \bot$ provided $x$ is free in $v$ and

2601: $x\neq v$.

2602:    \item[(Fail2)] $M, f(u_1,\ldots,u_m) \doteq g(v_1,\ldots,v_n) \to \bot$

2603: provided $f\neq g$.

2604:   \end{description}

2605:   We consider that equations $u \doteq v$ are unordered pairs of terms $u, v$,

2606:   so that in particular $u \doteq v$ and $v \doteq u$ are the same equation.

2607:   $\bot$ represents failure of unification.

2608:   If $s$ and $t$ are unifiable, then this rewrite process terminates, starting

2609:   from $s\doteq t$, on a so-called solved form $z_1 \doteq u_1, \ldots, z_k

2610:   \doteq u_k$; then $\sigma = \{z_1\mapsto u_1, \ldots, z_k\mapsto u_k\}$ 

2611:   is an mgu of $s\doteq t$.

2612: 

2613: 

2614:  

2615: \begin{lemma}

2616: \label{lemma:sxty}

2617: Let $s[x]$ and $t[y]$ be two non-ground non-trivial

2618: one-variable terms, and $x\neq y$.

2619: Let $U$ be the set of non-ground strict subterms of $s$ and $t$ and

2620: let $V$ be the set of ground strict subterms of $s$ and $t$. 

2621: If $s[x]$ and $t[y]$ are unifiable then they have a mgu $\sigma$ such that

2622: one of the following is true:

2623: \begin{itemize}

2624: \item $\sigma = \{x\mapsto u[y]\}$ where $u\in U$.

2625: \item $\sigma = \{y\mapsto u[x]\}$ where $u\in U$.

2626: \item $\sigma = \{x\mapsto u, y\mapsto v\}$ where $u,v\in U[V]$.

2627: \end{itemize}

2628: \end{lemma}

2629: \proof 

2630: Note that $V \subseteq U[V]$ since $U$ contains the trivial terms also.

2631: We use the above unification algorithm.

2632: We start with the multiset $M_0 = s\doteq t$. We claim that if $M_0 \to^+ M$

2633: then $M$ is of one of the following forms:

2634: \begin{enumerate}

2635: \item $s_1[x]=t_1[y],\ldots,s_n[x]=t_n[y]$, where each $s_i,t_i\in U\cup V$,

2636: some $s_i \in U$ and some $t_j\in U$. 

2637: \item $s_1[u[y']]=t_1[y'],\ldots,s_n[u[y']]=t_n[y'],x'=u[y']$ where $u\in U$,

2638: each $s_i,t_i\in U\cup V$, 

2639: $x'\in\{x,y\}$ and $y'\in\{x,y\}\setminus\{x'\}$.

2640: \item $s_1[u]=t_1[y'],\ldots,s_n[u]=t_n[y'],x'=u$ where $u \in V$,

2641: each $s_i,t_i\in U\cup V$, some $t_i\in U$,

2642: $x'\in\{x,y\}$ and $y'\in\{x,y\}\setminus\{x'\}$.

2643: \item $M', x = u, y=v$ where $u,v\in U[V]$, and no variables occur in $M'$.

2644: \item  $\bot$.

2645: \end{enumerate}

2646: 

2647: As $s$ and $t$ are non-trivial, and $x$ and $y$ are distinct, hence 

2648: (Delete) and (Bind)  don't apply on $M_0$. Applying (Decomp)

2649: on $M_0$ leads us to type (1).

2650: Applying (Fail1) or (Fail2) on any $M$ leads us to $\bot$.

2651: Applying (Delete) and (Decomp)  on type (1) keeps us in type (1).

2652: Applying (Bind) on type (1) leads to type (2) or (3) depending on whether

2653: the concerned variable is replaced by a non-ground or ground term.

2654: Applying (Delete) on type (2) leads to type (2) itself. Applying (Decomp)

2655: on type (2) leads to type (2) itself. (Bind) applies on $M$ of type (2) only

2656: if $M$ contains some $y'\doteq v$ where $v$ is ground. We must have

2657: $v \in V$. The result is of type (4).

2658: Applying (Delete) and (Decomp) rules on type (3) leads to type (3) itself.

2659: (Bind) applies on $M$ of type (3) only if $M$ contains some $y'\doteq v$

2660: where $v$ is ground. We must have $v\in U[V]$. 

2661: The result is of type (4).

2662: Applying (Delete) and (Decomp) on type (4) leads to type (4) itself, and

2663: (Bind) does not apply.

2664: 

2665: Now we look at the solved forms. Solved forms of type (1) are of the

2666: form either $x\doteq u[y]$ with $u\in U$, or $y\doteq u[x]$ with $u\in U$,

2667: or $x\doteq u,y\doteq v$ with $u,v\in V\subseteq U[V]$.

2668: $M$ of type (2) is in solved form only if $n=0$. Hence the solved forms

2669: are again of the form $x\doteq u[y]$ or $y\doteq u[x]$ with $u\in U$.

2670: $M$ of type (3) is in solved form only if $n=1$, hence $M$ is of the form

2671: $x\doteq u,y\doteq v$ with $u,v\in U[V]$. Solved forms of type (4) are again of

2672: type $x\doteq u,y\doteq v$ with $u,v\in U[V]$ (i.e. $M'$ is empty).

2673: \qed

2674: \endproof 

2675: 

2676: 

2677: \savelemmacounter

2678: \putlem{lemsxtyred}

2679: \begin{lemma}

2680: \lemsxtyredstatement

2681: \end{lemma}

2682: \proof 

2683: By Lemma~\ref{lemma:sxty}, $s[x]$ and $t[y]$ have a mgu $\sigma'$ such that

2684: one of the following is true:

2685: \begin{itemize}

2686: \item $\sigma' = \{x\mapsto u[y]\}$ where $u\in U$. We have $s[u[y]] = t[y]$.

2687: As $t$ is reduced, this is possible only if $u$ is trivial. Hence

2688: $s[y] = t[y]$, so $s[x] = t[x]$. This is a contradiction.

2689: \item $\sigma' = \{y\mapsto u[x]\}$ where $u\in U$. This case is similar to the

2690: previous case.

2691: \item $\sigma' = \{x\mapsto u, y\mapsto v\}$ where $u,v\in U[V]$.

2692: As $\sigma'$ is the  mgu and maps $x$ and $y$ to ground terms, hence

2693: $\sigma=\sigma'$.\qed

2694: \end{itemize}

2695: \endproof 

2696: \restorelemmacounter

2697: 

2698: \savelemmacounter

2699: \putlem{lemsxtx}

2700: \begin{lemma}

2701: \lemsxtxstatement

2702: \end{lemma}

2703: \proof 

2704: We use the above unification algorithm. We start with the multiset $M_0

2705: = s[x]=t[x]$. If $M_0 \to^+ M$ then $M$ is of one of the following forms: 

2706: \begin{enumerate}

2707: \item $s_1[x]=t_1[x],\ldots,s_n[x]=t_n[x]$ where each $s_i$ is a strict

2708: subterm of $s$ and each $t_i$ is a strict subterm of $t$

2709: \item $M, x = u$ where $u$ is a ground strict subterm of $s$ or $t$, and no

2710: variables occur in $M$

2711: \item $\bot$.

2712: \end{enumerate}

2713: 

2714: Then it is easy to see that the only possible solved form is $x\doteq u$

2715: where $u$ is a ground strict subterm of $s$ or $t$.\qed

2716: \endproof 

2717: \restorelemmacounter

2718: 

2719: %\savelemmacounter

2720: %\putlem{lemdecomp}

2721: %\begin{lemma}

2722: %\lemdecompstatement

2723: %\end{lemma}

2724: %\restorelemmacounter

2725: 

2726: 

2727: 

2728: %\savelemmacounter

2729: %\putlem{lemovresol}

2730: %\begin{lemma}

2731: %\lemovresolstatement

2732: %\end{lemma}

2733: %\restorelemmacounter

2734: 

2735: 

2736: %\section{Proofs of Section~\ref{sec:flat}}

2737: 

2738: %\savelemmacounter

2739: %\putlem{lemabsimulate}

2740: %\begin{lemma}

2741: %\lemabsimulatestatement

2742: %\end{lemma}

2743: %\restorelemmacounter

2744: 

2745: \section{Proofs of Section~\ref{sec:nh}}

2746: \label{apptwo}

2747: 

2748: \savethcounter

2749: \putth{thcompl}

2750: \begin{theorem}

2751: \thcomplstatement

2752: \end{theorem}

2753: \proof 

2754: A {\em standard Herbrand interpretation} is a Herbrand interpretation

2755: $\mathcal H$ such that $\ssp{C} \in \mathcal H$ iff $\mathcal H$ does not

2756: satisfy $C$. This leads us to the notion of {\em standard satisfiability}

2757: as expected. The given set $S$ of $\mathbb P$-clauses is satisfiable iff

2758: it is standard-satisfiable. Ordered resolution, 

2759: factorization and splitting preserve satisfiability in any given Herbrand

2760: interpretation, and $\sspreds$-splitting preserves satisfiability in any

2761: given standard-Herbrand interpretation. Also

2762: if $T \replres T'$ then $T \cup cl(\mathcal R)$ is satisfiable in a 

2763: Herbrand interpretation iff

2764: $T'\cup cl(\mathcal R)$ is satisfiable in that interpretation. 

2765: This proves correctness: if

2766: $S\atordselfssplreplres^* \mathcal T$ and $\mathcal T$ is closed then

2767: $S\cup cl(\mathcal R)$ is unsatisfiable.

2768: 

2769: For completeness

2770: we replay the proof of~\cite{JGL:SOresol} for

2771: ordered resolution with selection specialized to our

2772: case, and insert the arguments required for the replacement rules.

2773: %%%%% TODO State the derived resolution rule which combines resolution and factoring}

2774: %%%%% Jean's lecture notes: how to find the right enumeration for showing

2775: %%%%%  completeness of ordered resolution with  splittingless splitting.

2776: %Then a finite set $S_0$ of ground instances of

2777: %clauses in $S$ is unsatisfiable. Let $\mathcal A$ be the set of atoms occurring %in $S_0$. $S_0$ is finite hence $\mathcal A$ is finite. Since

2778: %$\mathbb P$ is finite and since $\atlt$ has the 

2779: %finite-descendants property hence the set $\mathcal B = \{B \mid \exists 

2780: %A\in\mathcal A \cdot B \atle A\} \cup \{C \mid C \textrm{ is a } \mathbb 

2781: %P-\textrm{clause and} \epsilon-\textrm{ block}\}

2782: %\supseteq \mathcal A$ is finite. 

2783: Since $\atlt$ is enumerable, hence we

2784: have an enumeration $A'_1,A'_2,\ldots$ of all ground

2785: atoms such that if $A'_i \atlt A'_j$ then $i < j$. 

2786: Also there are only finitely many splitting atoms in

2787: $\sspreds$, all of which are smaller

2788: than non-splitting atoms. Hence

2789: the set of all (splitting as well as non-splitting) atoms

2790: can be enumerated as $A_1,A_2,\ldots$ such that if $A_i\atltss A_j$ then $i<j$.

2791: Clearly all the splitting atoms occur

2792: before the non-splitting atoms in this enumeration.

2793: Consider the infinite binary tree $\mathbb T$ whose nodes are

2794: literal sequences of the form 

2795: $\pm_1 A_1 \pm_2 A_2 \ldots \pm_k A_k$ for $k\ge0$. 

2796: The two successors of the node $N$

2797: are $N+A_{k+1}$ (the left child) and $N-A_{k+1}$ (the right child). 

2798: If $k=0$ then $N$ is a root node. Furthermore we write

2799: $-N = \mp_1 A_i \mp_2 A_2 \ldots \mp_k A_k$. A clause {\em fails} at a node

2800: $N$ if there is some ground substitution $\sigma$ such that for every literal

2801: $L \in C$, $L \sigma$ is in $-N$.

2802: For any set $T$ of clauses define $\mathbb T_T$ as the tree obtained from

2803: $\mathbb T$ by deleting the subtrees below all nodes of $\mathbb T$ where

2804: some clause of $T$ fails. 

2805: %$\mathbb T_T$ is called {\em closed}

2806: %if at each leaf node of $\mathbb T_T$, some clause of $T$ fails.

2807: %(This happens iff at every leaf node of $\mathbb T$ some clause of $\mathbb T$

2808: %fails). 

2809: A failure-witness for a set $T$ of clauses 

2810: is a tuple $(\mathbb T',C_\bullet,\theta_\bullet)$ such that 

2811: $\mathbb T' = \mathbb T_T$ is finite, $C_N$ is a clause for each leaf node $N$ 

2812: of $\mathbb T'$, and $\theta_N$ is a ground substitution for each leaf node $N$

2813: of $\mathbb T'$ such that for $-N$  contains every 

2814: $L\in C_N\theta_N$. We define $\nu(\mathbb T')$ as the number of nodes

2815: in $\mathbb T'$.  For any failure witness of the form

2816: $(\mathbb T',C_\bullet,\theta_\bullet)$ and for any leaf node 

2817: $N=\pm_1 A_1 \pm_2 A_2 \ldots \pm_k A_k$ of 

2818: $\mathbb T'$, define $\mu_1 (C_N,\theta_N)$ as follows:\\

2819: -- If $C_N \notin cl(\mathcal R)$ then $\mu_1(C_N,\theta_N)$ is

2820: the multiset of integers which contains the integer $i$ as 

2821: many times as there are literals 

2822: $\pm A'\in C_N$ such that $A'\theta_N = A_i$.\\

2823: -- If $C_N \in cl(\mathcal R)$ then $\mu_1(C_N,\theta_N)$ is the

2824: empty multiset.\\

2825:  We define

2826: $\mu^-(\mathbb T',C_\bullet,\theta_\bullet)$ as the multiset of

2827: the values $\mu_1 (C_N,\theta_N)$ where $N$ ranges over all leaf nodes of 

2828: $\mathbb T'$. We define $\mu (\mathbb T',C_\bullet,\theta_\bullet) =

2829: (\nu(\mathbb T'),\mu^-(\mathbb T',C_\bullet,\theta_\bullet))$. We consider the

2830: lexicographic ordering on pairs, i.e. $(x_1,y_1)< (x_2,y_2)$ iff either

2831: $x_1 < x_2$, or $x_1=x_2$ and $y_1< y_2$.

2832: Since $S \cup cl(\mathcal R)$ is unsatisfiable, from K\"onig's Lemma: 

2833: \begin{lemma}

2834: $S\cup cl(\mathcal R)$ has a failure witness.

2835: \end{lemma}

2836: 

2837: \begin{lemma}

2838: If $T$ has a failure witness $(\mathbb T_T, C_\bullet,\theta_\bullet)$ 

2839: such that $\mathbb T_T$ is not just the root node, then there is some $T'$

2840: with a failure witness $(\mathbb T_{T'},C'_\bullet,\theta'_\bullet)$ such that

2841: $T \atordselres T'$ and $\mu(\mathbb T_{T'},C'_\bullet,\theta'_\bullet) <

2842: \mu(\mathbb T_T, C_\bullet,\theta_\bullet)$. 

2843: \end{lemma}

2844: \proof 

2845: %This is well known. The proof below is adapted from~\cite{JGL:SOresol}.

2846: In the following the notion of mgu is  generalized and we write

2847: $mgu(s_1\doteq \ldots \doteq s_n)$ for the most general substitution which

2848: makes $s_1,\ldots,s_n$ equal.

2849: We iteratively define a sequence $R_0,R_1,\ldots$ of nodes, none of which is a

2850: leaf node. $R_0$ is the empty sequence which is not a leaf node.

2851: Suppose we have already defined $R_i$. As $R_i$ is not a leaf node, $R_i$

2852: has a descendant $N_i$ such that $N_i - B_i$ is rightmost leaf node in the

2853: subtree of $\mathbb T_T$ rooted at $R_i$. 

2854: \begin{itemize}

2855: \item[(1)] If $B_i$ is a non-splitting atom then stop the iteration.

2856: \item[(2)] Otherwise $B_i$ is a splitting atom.

2857: \begin{itemize}

2858: \item[(2a)]

2859:  If the subtree rooted at $N_i + B_i$ has some leaf node $N$ such that

2860:  $- B_i \in C_N$ then stop the iteration.

2861: \item[(2b)] Otherwise $N_i + B_i$ cannot be a leaf node. 

2862: Define $R_{i+1} = N_i + B_i$ and continue the iteration.

2863: \end{itemize}

2864: \end{itemize}

2865: 

2866: $\mathbb T_T$ is finite hence the iteration terminates. Let $k$ be the

2867: largest integer for which $R_k$, and hence $N_k$ and $B_k$ are defined.

2868: For $0\le i\le k-1$, $B_i$ is a splitting literal. The only positive

2869: literals in the sequence $N_k$ are from the set $\{B_0,\ldots,B_{k-1}\}$.

2870: $N_k-B_k$ is a leaf node of $\mathbb T_T$.

2871: % By construction,

2872: % for any leaf node $N$ of

2873: %$\mathbb T_T$ which is a descendant of $N_k$, $C_N$ cannot contain any  

2874: %negative splitting literal other than $-B_k$.

2875: 

2876: %From the definition of our

2877: %iteration, $-B_i \notin C_{N_k-B_k}$ for $1\le i\le k-1$.

2878: %Hence $C_{N_k-B_k}$ has no negative literal.

2879: %%Also $B_k \in C_{N_k+B_k}$. $B_k$ is the maximal literal in $C_{N_k+B_k}$ and

2880: %%thus this can be chosen for resolution.

2881: %$C_{N_k-B_k}$ is of the form $C_1 \lor B'_1 \lor \ldots \lor B'_m (m\ge 1)$ 

2882: %such that $B'_1\theta_{N_k-B_k} = \ldots = B'_m\theta_{N_k-B_k} = B_k$

2883: %and each literal in $C_1\theta_{N_k-B_k}$ is present in

2884: %$-N_k$. The literals $B'_1,\ldots,B'_m$ are them maximal in $C_{N_k-B_k}$ 

2885: %and can be selected for resolution.

2886: 

2887: Suppose the iteration stopped in case (1) above. Then $N_k$ has some descendant

2888: $N$ such that its two children $N-B$ and $N+B$ are leaf nodes of $\mathbb T_T$,

2889: and $B$ is a non-splitting literal. As $B_k$ is a non-splitting literal,

2890: no negative splitting literals are present in $C_{N-B}$ or $C_{N+B}$.

2891: $C_{N-B}$ is of the form $C_1 \lor B'_1 \lor \ldots \lor B'_m (m\ge 1)$

2892: such that $B'_1\theta_{N-B} = \ldots = B'_m\theta_{N-B} = B$

2893: and each literal in $C_1\theta_{N-B}$ is present in

2894: $-N$. The literals $B'_1,\ldots,B'_m$ are then maximal in $C_{N-B}$

2895: and can be selected for resolution.

2896: $C_{N+B}$ is of the form $C_2 \lor -B''_1 \lor \ldots \lor -B''_n (n\ge 1)$

2897: such that $B''_1\theta_{N+B} = \ldots = B''_n\theta_{N+B} = B$

2898: and each literal in $C_2\theta_{N+B}$ is present in

2899: $-N$. The literals $B''_1,\ldots,B''_n$ are then maximal in $C_{N+B}$

2900: and can be selected for resolution. 

2901: We assume that $C_{N-B}$ and $C_{N+B}$ 

2902: are renamed apart so as not to share variables.

2903: Let $\theta$ be a ground substitution which maps each

2904: $x\in \fv(C_{N-B})$ to $x\theta_{N-B}$ and $x\in \fv(C_{N+B})$ to $x\theta_{N+B}$.

2905: We have $B'_1\theta = \ldots = B'_m\theta = B''_1\theta = \ldots = B''_n\theta$.

2906: Then $\sigma = mgu (B'_1\doteq \ldots \doteq B'_m\doteq B''_1 \doteq \ldots 

2907: \doteq B''_n)$ exists. Hence we have some ground substitution $\theta'$ such that

2908: $\sigma\theta'=\theta$.

2909: %%%% TODO state derived resolution rule.

2910: Hence by repeated applications of the ordered factorization and ordered binary

2911: resolution rule, 

2912: %%%%% by the above derived resolution rule, 

2913: we obtain the resolvent

2914: $C = C_1\sigma \lor C_2\sigma$, and $T \atordselres T' = T \cup \{C\}$.

2915: We have $C\theta' = C_1\theta \lor

2916: C_2\theta$. Hence $C$ fails at node $N$. 

2917: Then $\mathbb T_{T'}$ is finite

2918: and $\nu(\mathbb T_{T'}) < \nu(\mathbb T_{T})$. Hence by choosing 

2919: any $C'_\bullet$ and $\theta'_\bullet$ such that $(\mathbb T_{T'},C'_\bullet,

2920: \theta'_\bullet)$ is a failure witness for $T'$, we have

2921: $\mu(\mathbb T_{T'},C'_\bullet,\theta'_\bullet) < 

2922: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$.

2923: 

2924: 

2925: If the iteration didn't stop in  case (1) but in case (2a)

2926: then it means that $B_k$

2927: is a splitting literal. Then $C_{N_k-B_k} = C_1 \lor +B_k$ (with

2928: $B_k \notin C_1$).

2929: $C_1$ has no negative splitting literals. Hence the only literals in $C_1$ 

2930: are positive splitting literals. Hence the literal $B_k$ can be chosen from

2931: $C_{N_k-B_k}$ for resolution.  The subtree rooted at $N_k + B_k$ has some

2932: leaf node $N$ such that $-B_k \in C_N$. Then $C_N = C_2 \lor -B_k$ 

2933: (and $-B_k\notin C_2$).  Hence

2934: $-B_k$ can be selected from $C_N$ for resolution. We obtain the resolvent

2935: $C_2 \lor C_1$ which fails at $N$. Let $T' = T \cup \{C_1 \lor C_1\}$.

2936: We have $\nu(\mathbb T_{T'}) \le \nu(\mathbb T_T)$.

2937: If $N'$ is the highest ancestor of $N$ where $C_2 \lor C_1$ fails then

2938: $N'$ is a leaf of $\mathbb T_{T'}$ and we define $C'_{N'} = C_2 \lor C_1$

2939: and $\theta'_{N'} = \theta_N$. We have 

2940: $\mu_1(C'_{N'},\theta'_{N'}) < \mu_1(C_N,\theta_N)$ since all 

2941: literals in $C_1$ are splitting literals $\pm q$ such that $q$ occurs strictly

2942: before $B_k$ in the enumeration $A_1,A_2,\ldots$. (Also note that

2943: $C_N \notin cl(\mathcal R)$ because $C_N$ contains a splitting literal). 

2944: All other leaf nodes

2945: $N''$ of $\mathbb T_{T'}$ are also leaf nodes of $\mathbb T_T$ and we define

2946: $C'_{N''} = C_{N''}$ and $\theta'_{N''} = \theta_{N''}$.

2947: Then $(\mathbb T_{T'},C'_\bullet,\theta'_\bullet)$ is a failure witness for

2948: $T'$ and we have $\mu^-(\mathbb T_{T'},C'_\bullet,\theta'_\bullet) <

2949: \mu^-(\mathbb T_{T},C_\bullet,\theta_\bullet)$. 

2950: Hence we have $\mu(\mathbb T_{T'},C'_\bullet,\theta'_\bullet) <

2951: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$.

2952: \qed

2953: \endproof 

2954: 

2955: \begin{lemma}

2956: If $T$ has a failure witness $(\mathbb T_T,C_\bullet,\theta_\bullet)$ 

2957: and $T \predssplres T'$ then $T'\cup cl(\mathcal R)$ has a failure witness

2958: $(\mathbb T_{T'\cup cl(\mathcal R)},C'_\bullet,\theta'_\bullet)$ with

2959: $\mu(\mathbb T_{T'\cup cl(\mathcal R)},C'_\bullet,\theta'_\bullet) \le

2960: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$.

2961: \end{lemma}

2962: \proof 

2963: %%% TODO Jean's lecture notes: page 23 replace \mu by \mu_1

2964: Let $C = C_1 \sqcup C_2 \in T$, $C_2$ is a non-empty $\mathbb P$-clause,

2965: $C_1$ has at least one non-splitting literal, and

2966: $T \predssplres T' = (T \setminus \{C\}) \cup \{C_1 \lor  - \ssp{C_2},

2967: \ssp{C_2} \lor C_2\}$. 

2968: If $C \neq C_N$ for any leaf node $N$ of $\mathbb T_T$ then there is nothing

2969: to show.

2970: Now suppose $C = C_N$ where $N$ is a leaf node of $\mathbb T_T$. If

2971: $C_N \in cl(\mathcal R)$ then there is nothing to prove. Now suppose

2972: $C_N \notin cl(\mathcal R)$.

2973: As $C$ is constrained to contain at least one non-splitting literal, hence

2974: the literal sequence $N$ has at least one non-splitting literal. By the

2975: chosen enumeration $A_1,A_2,\ldots$, 

2976: either $\ssp{C_2}$ or $-\ssp{C_2}$ occurs in the literal sequence $N$.

2977: \begin{itemize}

2978: \item If $\ssp{C_2}$ occurs in $N$ then $C_1 \lor  - \ssp{C_2}$ fails at

2979: $N$. Let $N'$ be the highest ancestor of $N$ where it fails. 

2980: $N'$ is a leaf node of $\mathbb T_{T'}$. We define

2981: $C''_{N'} = C_1 \lor  - \ssp{C_2}$ and $\theta''_{N'} = \theta_N$. All other

2982: leaf nodes $N''$ of $\mathbb T_{T'}$ are also leaf nodes of $\mathbb T_T$

2983: and we define $C''_{N''} = C_{N''}$ and $\theta''_{N''} = \theta_{N''}$.

2984: $(\mathbb T_{T'},C''_\bullet,\theta''_\bullet)$ is a failure witness

2985: for $T'$. As $C_2$ has at least one non-splitting literal, we have

2986: $\mu_1(C''_{N'},\theta''_{N'}) < \mu_1(C_N,\theta_N)$ 

2987: (recall that $C_N\notin cl(\mathcal R)$) so that

2988: $\mu(\mathbb T_{T'},C''_\bullet,\theta''_\bullet) \le

2989: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$. As $T'\subseteq T'\cup

2990:  cl(\mathcal R)$ hence the result follows.

2991: \item

2992: If $-\ssp{C_2}$ occurs in $N$ then $C_2 \lor \ssp{C_2}$ fails at

2993: $N$. Since $C_1$ has at least one non-splitting literal, as in the previous

2994: case, we obtain a failure witness $(\mathbb T_{T'},C''_\bullet,\theta''_\bullet)$

2995: such that $\mu(\mathbb T_{T'},C''_\bullet,\theta''_\bullet) \le

2996: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$.\qed

2997: \end{itemize}

2998: \endproof 

2999: 

3000: \begin{lemma}

3001: If $T$ has a failure witness $(\mathbb T_T,C_\bullet,\theta_\bullet)$ 

3002: and $T \splres T_1\mid T_2$ then $T_1\cup cl(\mathcal R)$ and

3003: $T_2 \cup cl(\mathcal R)$ have failure witnesses

3004: $(\mathbb T_{T_1\cup cl(\mathcal R)}\allowbreak ,\allowbreak  C'_\bullet\allowbreak ,\allowbreak  \theta'_\bullet\allowbreak )$ 

3005: and $(\mathbb T_{T_2\cup cl(\mathcal R)},C''_\bullet,\theta''_\bullet)$ such that

3006: $\mu(\mathbb T_{T_1 \cup cl(\mathcal R)},C'_\bullet,\theta'_\bullet) \le

3007: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$

3008: and $\mu(\mathbb T_{T_2 \cup cl(\mathcal R)},C''_\bullet,\theta''_\bullet) \allowbreak  \le\\

3009: \allowbreak  \mu\allowbreak (\mathbb T_T, C_\bullet,\theta_\bullet)$.

3010: \end{lemma}

3011: \proof 

3012: Let $C = C_1 \sqcup C_2 \in T$ such that $C_1$ and $C_2$ share no variables,

3013: and we have $T \splres T_1 \mid T_2$ where $T_i = T \cup \{C_i\}$.

3014: We prove the required result for $T_1$, the other part is symmetric.

3015: If 

3016: $C \neq C_N$ for any leaf node $N$ of $\mathbb T_T$ then there is nothing to 

3017: show. Now suppose $C = C_N$ for some leaf node $N$ of $\mathbb T_T$.

3018: If $C_N \in cl(\mathcal R)$  then there is nothing to show.

3019: Now suppose $C_N \notin cl(\mathcal R)$. 

3020: Since $C_1 \subseteq C$, hence $C_1$ also fails at $N$.

3021: Let $N'$ be the highest ancestor of $N$ where $C_1$ fails. $N'$ is a leaf

3022: node of $\mathbb T_{T_1}$. We define $C'''_{N'} = C$ and $\theta'''_{N'} = \theta$.

3023: All other leaf nodes $N''$ of $\mathbb T_{T_1}$ are also leaf nodes of

3024: $\mathbb T_T$, and we define $C'''_{N''} = C_{N''}$ and $\theta'''_{N''}

3025: = \theta_{N''}$. $(\mathbb T_{T_1},C'''_\bullet,\theta'''_\bullet)$ is a failure

3026: witness for $T_1$. Also $\mu_1(C'''_{N'},\theta'''_{N'}) \le 

3027: \mu_1(C_N,\theta_N)$ (recall that $C_N \notin cl(\mathcal R)$). Hence

3028: $\mu(\mathbb T_{T'},C'''_\bullet,\theta'''_\bullet) \le

3029: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$. As $T_1\subseteq T_1\cup

3030: cl(\mathcal R)$, hence the result follows.

3031: \endproof 

3032: 

3033: 

3034: The following arguments are the ones that take care of replacement steps.

3035: \begin{lemma}

3036: If $T$ has a failure witness $(\mathbb T_T,C_\bullet,\theta_\bullet)$ 

3037: and $T \replres T'$ then $T'\cup cl(\mathcal R)$ has a failure witness

3038: $(\mathbb T_{T'\cup cl(\mathcal R)},C'_\bullet,\theta'_\bullet)$ with

3039: $\mu(\mathbb T_{T'\cup cl(\mathcal R)},C'_\bullet,\theta'_\bullet) \le

3040: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$.

3041: \end{lemma}

3042: \proof 

3043: Let $C_1 = C'_1 \lor \pm A\sigma \in T$, $R = A \repl B \in \mathcal R$,

3044: and $T \replres T' = (T \setminus \{C_1\})

3045: \cup \{C\}$ where $C= C'_1 \lor \pm B\sigma$. 

3046: If $C_1 \neq C_N$ for any leaf node of $\mathbb T_T$ then there is nothing to

3047: prove. Now suppose that $C_1 = C_N$ for some leaf node $N$ of $\mathbb T_T$.

3048: Let $N = \pm_1 A_1 \ldots \pm_k A_k$. If $C_1 \in cl(\mathcal R)$ then 

3049: $T \subseteq T' \cup cl(\mathcal R)$, and there is nothing to prove. Now

3050: suppose $C_1 \notin cl(\mathcal R)$.

3051: We have a ground substitution $\theta$ such that

3052: $C_1 \theta = C'_1\theta \lor \pm A\sigma\theta

3053: \subseteq \{\mp_1 A_1, \ldots, \mp_k A_k\}$.

3054: As $R$ is ordered we have $A \atge B$. Hence 

3055: $A\sigma\theta \atge B\sigma\theta$.

3056: Hence  either

3057: $\pm B\sigma\theta \in \{\mp_1 A_1, \ldots, \mp_k A_k\}$ or

3058: $\mp B\sigma\theta \in \{\mp_1 A_1, \ldots, \mp_k A_k\}$. 

3059: \begin{itemize}

3060: \item

3061: Suppose $\pm B\sigma\theta \in \{\mp_1 A_1, \ldots, \mp_k A_k\}$.

3062: Since $C_1 \theta = C'_1\theta \lor \pm A\sigma\theta

3063: \subseteq \{\allowbreak \mp_1 \allowbreak A_1, \allowbreak \ldots,\allowbreak  \mp_k\allowbreak  A_k\allowbreak \}$, hence

3064: $C \theta = C'_1\theta \lor \pm B\sigma\theta

3065: \subseteq \{\mp_1 A_1, \ldots, \mp_k A_k\}$. Hence $C$ fails at $N$.

3066: Let $N'$ be the highest ancestor of $N$ where $C$ fails. $N'$ is a leaf

3067: node of $\mathbb T_{T'}$. We define $C''_{N'} = C$ and $\theta''_{N'} = \theta$.

3068: All other leaf nodes $N''$ of $\mathbb T_{T'}$ are also leaf nodes of

3069: $\mathbb T_T$, and we define $C''_{N''} = C_{N''}$ and $\theta''_{N''}

3070: = \theta_{N''}$. $(\mathbb T_{T'},C''_\bullet,\theta''_\bullet)$ is a failure

3071: witness for $T'$. Also $\mu_1(C''_{N'},\theta''_{N'}) \le 

3072: \mu_1(C_N,\theta_N)$ (recall that $C_N \notin cl(\mathcal R)$). Hence

3073: $\mu(\mathbb T_{T'},C'_\bullet,\theta'_\bullet) \le

3074: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$. As $T'\subseteq T'\cup

3075: cl(\mathcal R)$, hence the result follows.

3076: \item Suppose $\mp B\sigma\theta \in \{\mp_1 A_1, \ldots, \mp_k A_k\}$.

3077: Since $\pm A\sigma\theta = \in 

3078: \{\mp_1 A_1, \ldots, \mp_k A_k\}$, hence the clause $\mp A \lor \pm B 

3079: \in cl(\mathcal R)$ fails at $N$. 

3080: Let $N'$ be the highest ancestor of $N$ where $\mp A \lor \pm B$ fails.

3081: $N'$ is a leaf node of $\mathbb T_{T'\cup\{\mp A \lor \pm B\}}$.

3082: We define $C''_{N'} = C$ and $\theta''_{N'} = \theta$.

3083: All other leaf nodes $N''$ of $\mathbb T_{T'\cup\{\mp A \lor \pm B\}}$

3084: are also leaf nodes of

3085: $\mathbb T_T$, and we define $C''_{N''} = C_{N''}$ and $\theta''_{N''}

3086: = \theta_{N''}$. $(\mathbb T_{T'\cup\{\mp A \lor \pm B\}},C''_\bullet,

3087: \theta''_\bullet)$ is a failure

3088: witness for $T'\cup\{\mp A \lor \pm B\}$. Also $\mu_1(C''_{N'},\theta''_{N'}) \le

3089: \mu_1(C_N,\theta_N)$ since $\mu_1(C''_{N'},\theta''_{N'})$ is the empty

3090: multiset. Hence

3091: $\mu(\mathbb T_{T'\cup\{\mp A \lor \pm B\}},C''_\bullet,\theta''_\bullet) \le

3092: \mu(\mathbb T_T,C_\bullet,\theta_\bullet)$. As $T'\cup\{\mp A \lor \pm B\}

3093: \subseteq T'\cup

3094: cl(\mathcal R)$, hence the result follows.

3095: \qed

3096: \end{itemize}

3097: \endproof 

3098: 

3099: For a tableaux $\mathcal T = S_1 \mid \ldots \mid S_n$, define

3100: $\mathcal T \cup S = S_1 \cup S \mid \ldots \mid S_n \cup S$. We define

3101: a failure witness for such a $\mathcal T$ to be a multiset

3102: $\{(\mathbb T_{S_1},C^1_\bullet,\theta^1_\bullet),\ldots,

3103: (\mathbb T_{S_n},C^1_\bullet,\theta^n_\bullet)\}$ where

3104: each $(\mathbb T_{S_i},C^i_\bullet,\theta^i_\bullet)$ is a failure

3105: witness of $S_i$. We define\\ 

3106: \strut \hfill $\mu(\{\mathbb T_{S_1},C^1_\bullet,\theta^1_\bullet),\ldots,

3107: (\mathbb T_{S_n},C^1_\bullet,\theta^n_\bullet\}) = 

3108: \{\mu(\mathbb T_{S_1},C^1_\bullet,\theta^1_\bullet),\ldots,

3109: \mu(\mathbb T_{S_n},C^1_\bullet,\theta^n_\bullet)\}$.\hfill\ \\

3110: Then it is clear that $S\cup cl(\mathcal R)$ 

3111: has a failure witness and whenever any $\mathcal T$

3112: has a failure witness in which one of the trees has at least two nodes,

3113: then $\mathcal T \atordselfssplreplres \mathcal T'$ for some 

3114: $\mathcal T'$ such that

3115: $\mathcal T'\cup cl(\mathcal R)$ has a strictly smaller failure witness.

3116: Hence we have some $\mathcal T$ such that

3117: $S \atordselfssplreplres^* \mathcal T$ and $\mathcal T\cup cl(\mathcal R)$ 

3118: has a failure witness

3119: in which each tree is a root node. Then $\mathcal T \cup cl(\mathcal R)$

3120: is closed. Hence $\mathcal T$ is closed.

3121: \qed

3122: \endproof 

3123: \restorethcounter

3124: 

3125: %\savelemmacounter

3126: %\putlem{lemnhresol}

3127: %\begin{lemma}

3128: %\lemnhresolstatement

3129: %\end{lemma}

3130: %\restorethcounter

3131: 

3132: 

3133: 

3134: \end{document}

3135: