1: % de definitieve versie voor lpar (dd. 9 augustus 2002)

2: \documentclass{llncs}

3: 

4: \title{First-order Logic as a Constraint Programming Language}

5: 

6: \author{K. R. Apt\inst{1,2} and C. F. M. Vermeulen\inst{1}}

7: \institute{CWI, P.O. Box 94079, 1090 GB Amsterdam, the Netherlands\\

8: \and

9: University of Amsterdam, the Netherlands}

10: 

11: \usepackage{amsfonts}

12: \usepackage{latexsym}

13: \usepackage{alltt}

14: 

15: \hyphenation{para-digms}

16: 

17: %\newcommand{\notext}[1]{\mbox{}}

18: 

19: \newcommand{\tupel}[1]{\langle #1 \rangle} 

20: \newcommand{\verz}[1]{\{ #1\} } 

21: \newcommand{\pow}[1]{\mbox{\sc pow}( #1 )}

22: \newcommand{\jsub}[0]{\mbox{\it Subs}} 

23: \newcommand{\jsubs}[0]{\mbox{\it Subs}} 

24: \newcommand{\infer}[0]{\mbox{\it infer}} 

25: \newcommand{\infaux}[0]{\mbox{\it inf}} 

26: \newcommand{\simp}[0]{\mbox{\it simp}} 

27: \newcommand{\elim}[0]{\mbox{\it elim}} 

28: \newcommand{\solve}[0]{\mbox{\it solve}} 

29: \newcommand{\myerror}[0]{\mbox{\sc error}} 

30: \newcommand{\states}[0]{\mbox{\sc states}} 

31: \newcommand{\fail}[0]{\mbox{\it fail}} 

32: \newcommand{\dbar}[0]{|\! |} 

33: \newcommand{\perm}[1]{\mbox{\it perm}( #1 )}

34: \newcommand{\sh}[1]{\mbox{\it sh}( #1 )}

35: \newcommand{\weg}[0]{\mbox{\sc drop}}

36: \newcommand{\comp}[0]{\mbox{\it comp}}

37: \newcommand{\prop}[0]{\mbox{\it prop}}

38: \newcommand{\comment}[1]{\mbox{(\footnotesize{#1})}}

39: 

40: \newcommand{\mysem}[1]{[\! [#1 ]\!]}

41: \newcommand{\mycons}[0]{\mbox{\it cons}}

42: 

43: \newcommand{\CSP}[0]{{\cal CSP}}

44: \newcommand{\csp}[0]{{\cal C}}

45: 

46: \newcommand{\sm}[0]{\mbox{\footnotesize sm}}

47: 

48: %\include{cmds}

49: \newcommand{\inv}{\invisible}

50: \newcommand{\IF}{\mbox{{\bf if}\ }}

51: \newcommand{\FI}{\mbox{{\bf fi}}}

52: \newcommand{\DO}{\mbox{{\bf do}\ }}

53: \newcommand{\OD}{\mbox{{\bf od}}}

54: \newcommand{\WHILE}{\mbox{{\bf while}\ }}

55: \newcommand{\END}{\mbox{{\bf end}}}

56: \newcommand{\THEN}{\mbox{\ {\bf then}\ }}

57: \newcommand{\ELSE}{\mbox{\ {\bf else}\ }}

58: \newcommand{\T}{\mbox{{\bf true}}}

59: \newcommand{\F}{\mbox{{\bf false}}}

60: \newcommand{\FAIL}{{\bf fail}}

61: \newcommand{\ES}{\mbox{$\emptyset$}}

62: 

63: \newcommand{\la}{\mbox{$\:\leftarrow\:$}}

64: \newcommand{\ra}{\mbox{$\:\rightarrow\:$}}

65: \newcommand{\da}{\mbox{$\:\downarrow\:$}}

66: \newcommand{\ua}{\mbox{$\:\uparrow\:$}}

67: \newcommand{\La}{\mbox{$\:\Leftarrow\:$}}

68: \newcommand{\Ra}{\mbox{$\:\Rightarrow\:$}}

69: \newcommand{\tra}{\mbox{$\:\rightarrow^*\:$}}

70: \newcommand{\lra}{\mbox{$\:\leftrightarrow\:$}}

71: \newcommand{\bu}{\mbox{$\:\bullet \ \:$}}

72: \newcommand{\up}{\mbox{$\!\!\uparrow$}}

73: 

74: \newcommand{\A}{\mbox{$\ \wedge\ $}}

75: \newcommand{\bigA}{\mbox{$\bigwedge$}}

76: \newcommand{\Or}{\mbox{$\ \vee\ $}}

77: \newcommand{\U}{\mbox{$\:\cup\:$}}

78: \newcommand{\I}{\mbox{$\:\cap\:$}}

79: \newcommand{\sse}{\mbox{$\:\subseteq\:$}}

80: 

81: \newcommand{\po}{\mbox{$\ \sqsubseteq\ $}}

82: \newcommand{\spo}{\mbox{$\ \sqsubset\ $}}

83: \newcommand{\rpo}{\mbox{$\ \sqsupseteq\ $}}

84: \newcommand{\rspo}{\mbox{$\ \sqsupset\ $}}

85: 

86: 

87: \newcommand{\Mo}{\mbox{$\:\models\ $}}

88: \newcommand{\mtwo}{\mbox{$\:\models_{\it 2}\ $}}

89: \newcommand{\mthree}{\mbox{$\:\models_{\it 3}\ $}}

90: \newcommand{\Mf}{\mbox{$\:\models_{\it f\!air}\ $}}

91: \newcommand{\Mt}{\mbox{$\:\models_{\it tot}\ $}}

92: \newcommand{\Mwt}{\mbox{$\:\models_{\it wtot}\ $}}

93: \newcommand{\Mp}{\mbox{$\:\models_{\it part}\ $}}

94: 

95: \newcommand{\PR}{\mbox{$\vdash$}}

96: 

97: \newcommand{\fa}{\mbox{$\forall$}}

98: \newcommand{\te}{\mbox{$\exists$}}

99: \newcommand{\fai}{\mbox{$\stackrel{\infty}{\forall}$}}

100: \newcommand{\tei}{\mbox{$\stackrel{\infty}{\exists}$}}

101: 

102: \newcommand{\calA}{\mbox{$\cal A$}}

103: \newcommand{\calG}{\mbox{$\cal G$}}

104: \newcommand{\calB}{\mbox{$\cal B$}}

105: 

106: \newcommand{\LLn}{\mbox{$1,\ldots,n$}}

107: \newcommand{\LL}{\mbox{$\ldots$}}

108: 

109: \newcommand{\WP}{deterministic program}

110: \newcommand{\WPs}{deterministic programs}

111: \newcommand{\AW}{\mbox{{\bf await}-statement}}

112: \newcommand{\AWs}{\mbox{{\bf await}-statements}}

113: 

114: \newcommand{\IFP}{\mbox{$\IF B_1 \ra S_1 \Box \LL \Box B_n \ra S_n\ \FI$}}

115: \newcommand{\DOP}{\mbox{$\DO B_1 \ra S_1 \Box \LL \Box B_n \ra S_n\ \OD$}}

116: \newcommand{\DIP}{\mbox{$[S_1 \| \LL \| S_n]$}}

117: \newcommand{\IFPa}{\mbox{$\IF \Box^n_{i=1}\ B_i \ra S_i\ \FI$}}

118: \newcommand{\DOPa}{\mbox{$\DO \Box^n_{i=1}\ B_i \ra S_i\ \OD$}}

119: 

120: \newcommand{\MS}[1]{\mbox{${\cal M}[\![{#1}]\!]$}}

121: \newcommand{\newMS}[1]{\mbox{$[\![{#1}]\!]$}}

122: \newcommand{\newhat}[1]{\langle {#1} \rangle}

123: \newcommand{\M}[2]{\mbox{${\cal M}[\![{#1},{#2}]\!]$}}

124: \newcommand{\MF}[1]{\mbox{${\cal M}_{{\it f\!air}}[\![{#1}]\!]$}}

125: \newcommand{\MT}[1]{\mbox{${\cal M}_{{\it tot}}[\![{#1}]\!]$}}

126: \newcommand{\MP}[1]{\mbox{${\cal M}_{{\it part}}[\![{#1}]\!]$}}

127: \newcommand{\MWT}[1]{\mbox{${\cal M}_{{\it wtot}}[\![{#1}]\!]$}}

128: \newcommand{\NS}[1]{\mbox{${\cal N}[\![{#1}]\!]$}}

129: 

130: \newcommand{\ITE}[3]{\mbox{$\IF {#1} \THEN {#2} \ELSE {#3}\ \FI$}}

131: \newcommand{\IT}[2]{\mbox{$\IF {#1} \THEN {#2}\ \FI$}}

132: \newcommand{\WD}[1]{\mbox{$\WHILE {#1}\ \DO$}}

133: \newcommand{\WDD}[2]{\mbox{$\WHILE {#1}\ \DO {#2}\ \OD$}}

134: \newcommand{\W}[1]{\mbox{${\bf wait}\ {#1}$}}

135: \newcommand{\AT}[1]{\mbox{${\bf await}\ {#1}\ {\bf then}$}}

136: \newcommand{\ATE}[2]{\mbox{${\bf await}\ {#1} \THEN {#2}\ \END$}}

137: \newcommand{\ATOM}[1]{\mbox{$\langle {#1} \rangle$}}

138: \newcommand{\RU}[2]{\mbox{${\bf repeat}\ {#1}\ {\bf until}\ {#2}$}}

139: 

140: \newcommand{\TF}[1]{\mbox{$T_{{\it f\!air}}({#1})$}}

141: \newcommand{\TFn}{\mbox{$T_{{\it f\!air}}$}}

142: 

143: \newcommand{\HT}[3]{\mbox{$\{{#1}\}\ {#2}\ \{{#3}\}$}}

144: 

145: \newcommand{\sg}{{\mbox{$\sigma$}}}

146: \newcommand{\Sg}{{\mbox{$\Sigma$}}}

147: \newcommand{\om}{{\mbox{$\omega$}}}

148: \newcommand{\al}{{\mbox{$\alpha$}}}

149: \newcommand{\ba}{{\mbox{$\beta$}}}

150: 

151: \newcommand{\B}[1]{\mbox{$[\![{#1}]\!]$}}       % brackets

152: \newcommand{\C}[1]{\mbox{$\{{#1}\}$}}           % curly braces

153: 

154: \newcommand{\UPDATE}{\mbox{$U\!P\!D\!AT\!E$}}

155: \newcommand{\INIT}{\mbox{$I\!N\!IT$}}

156: \newcommand{\SCH}{\mbox{$SC\!H$}}

157: \newcommand{\FAIR}{\mbox{$F\!AI\!R$}}

158: \newcommand{\RORO}{\mbox{$RO\!RO$}}

159: \newcommand{\QUEUE}{\mbox{$QU\!EU\!E$}}

160: \newcommand{\INV}{\mbox{$IN\!V$}}

161: \newcommand{\VAR}{\mbox{\it Var}}

162: \newcommand{\unfold}{\mbox{\it unfold}}

163: \newcommand{\fold}{\mbox{\it fold}}

164: \newcommand{\ol}[1]{\mbox{$\overline{{#1}}$}}

165: \newcommand{\NI}{\noindent}

166: \newcommand{\HB}{\hfill{$\Box$}}

167: \newcommand{\VV}{\vspace{5 mm}}

168: \newcommand{\III}{\vspace{3 mm}}

169: \newcommand{\II}{\vspace{2 mm}}

170: \newcommand{\PP}{\mbox{$[S_1 \| \LL \| S_n]$}}

171: 

172: \newcommand{\X}[1]{\mbox{$\:\stackrel{{#1}}{\rightarrow}\:$}}

173: \newcommand{\lX}[1]{\mbox{$\:\stackrel{{#1}}{\longrightarrow}\:$}}

174: 

175: % \newcommand{\bold}[1]{{\bf #1}}  % for makeindex

176: % \newcommand{\see}[2]{{\it see\/} #1}  % for makeindex

177: 

178: %\newenvironment{myv}{\begin{verbatim} \small}{\normalsize \end{verbatim}} 

179: %for programs

180: 

181: \newcommand{\error}{{\bf error}}

182: \newcommand{\vect}[1]{{\bf #1}}

183: \newcommand{\D}[1]{\mbox{$|[{#1}]|$}}           % |[ ]| braces

184: \newcommand{\hb}[1]{{\Theta_{#1}}}

185: \newcommand{\hi}{{\cal I}}

186: \newcommand{\ran}{\rangle}

187: \newcommand{\lan}{\langle}

188: \newcommand{\dom}{{\it Dom}}

189: \newcommand{\var}{{\it Var}}

190: \newcommand{\pred}{{\it pred}}

191: \newcommand{\sem}[1]{{\mbox{$[\![{#1}]\!]$}}}

192: \newcommand{\false}{{\it false}}

193: \newcommand{\true}{{\it true}}

194: \newtheorem{Property}{Property}[section]

195: \newcommand{\hsuno}{\hspace{ .5in}}

196: \newcommand{\vsuno}{\vspace{ .25in}}

197: \newcommand{\cons}{$\! \mid $}

198: \newcommand{\nil}{[\,]}

199: \newcommand{\restr}[1]{\! \mid \! {#1}} 

200: \newcommand{\range}{{\it Ran}}

201: \newcommand{\Range}{{\it Range}}

202: \newcommand{\PC}{\mbox{$\: \simeq \:$}}

203: \newcommand{\TC}{\mbox{$\: \simeq_t \:$}}

204: \newcommand{\IO}{\mbox{$\: \simeq_{i/o} \:$}}

205: \newcommand{\size}{{\rm size}}

206: \newcommand{\Der}[2]

207:         {\; |\stackrel{#1}{\!\!\!\longrightarrow _{#2}}\; }

208: 

209: \newcommand{\Sder}[2]

210:         {\; |\stackrel{#1}{\!\leadsto_{#2}}\; }

211: 

212: %\newcommand{\nat} { \mbox{\hspace{0.4ex}} {\rm N}

213: %                   \mbox{\hspace{-2.0ex}} {\rm I} \mbox{\hspace{0.8ex}}}

214: %

215: %\newcommand{\pif}{\leftarrow}

216: %\newcommand{\clause}[2]{#1 & \!\!\!\! \pif & \!\!\!\! #2} %\clause{head}{body}

217: %\newcommand{\comclause}[3]{\clause{#1}{#2}&\mbox{\% #3}}  %...{comment}

218: %

219: %\newenvironment{program}%                     % program with clauses numbered

220: %{\begin{eqnarray}\setcounter{equation}{1}}%   % C1,...Cn

221: %{\end{eqnarray}}

222: %\renewcommand{\theequation}{C\arabic{equation}}

223: %

224: %\newenvironment{ack}%

225: %{{\vspace{2ex}\par \noindent \bf

226: %\bf Acknowledgements.}}{\ignorespaces}

227: %

228: %\newcommand{\qed}{\hfill*$\quad\Box$}

229: %\newenvironment{Pf}{\par \noindent{\bf Proof.~}}{\qed }

230: %

231: 

232: \newcommand{\szkew}[1]{\relax \setbox0=\hbox{\kern -24pt $\displaystyle#1$\kern 0pt }%

233: %\advance\ht0 by 0pt %

234: %\advance\dp0 by -10pt %

235: \box0}

236: {\catcode`\@=11 \global\let\ifjusthvtest@=\iffalse}

237: %\definemorphism{dashto}\dashed\tip\notip

238: 

239: \newcommand{\iif}{\mbox{$\longrightarrow$}}

240: \newcommand{\longra}{\mbox{$\longrightarrow$}}

241: \newcommand{\Longra}{\mbox{$\Longrightarrow$}}

242: \newcommand{\res}[3]{\mbox{$#1\stackrel{\textstyle #2}{\Longra}#3$}}

243: \newcommand{\reso}[4]{\mbox{

244: $#1 \stackrel{#2}{\Longra}_{\hspace{-4mm}_{#3}} \hspace{2mm} #4$}}

245: \newcommand{\nextres}[2]{\mbox{$\stackrel{\textstyle #1}{\Longra}#2$}}

246: \newcommand{\preres}[2]{\mbox{$#1\stackrel{\textstyle #2}{\Longra}$}}

247: \newcommand{\Preres}[2]{\mbox{$#1\stackrel{\textstyle #2}{\longra}$}}

248: 

249: %just deleted old in 4 lines below and commented three lines below

250: \newcounter{oldmycaption}

251: \newcommand{\oldmycaption}[1]

252: {\begin{center}\addtocounter{oldmycaption}{1}

253: {{\bf Program \theoldmycaption} : #1}\end{center}} 

254: 

255: \newcommand{\mycite}[1]

256: {\cite{#1} \glossary{#1}}

257: 

258: \newcommand{\mycaption}[1]

259: {\begin{center}{{\bf Program:} $#1$}

260: \index{#1} \end{center}} 

261: 

262: \newcommand{\ass}{{\cal A}}

263: \newcommand{\defi}{{\stackrel{\rm def}{=}}}

264: 

265: %\newcommand{\textbf}[1]{{\bf #1}}

266: 

267: % from art/at.tex

268: 

269: \newcommand{\Seq}[1]{{\bf #1}}

270: \newcommand{\BSeq}[2]{{{#1}_1},\ldots,{{#1}_{#2}}}

271: \newcommand{\OSeq}[2]{{{#1}_0},\ldots,{{#1}_\alpha},\ldots}

272: \newcommand{\Var}[1]{{\it Var}({#1})}

273: \newcommand{\FreeVar}[1]{{\it FreeVar}({#1})}

274: \newcommand{\Dom}[1]{{\it Dom}({#1})}

275: \newcommand{\Ran}[1]{{\it Ran}({#1})}

276: \newcommand{\Neg}{\neg}

277: \newcommand{\Fail}{{\it fail}}

278: \newcommand{\Success}{\Box}

279: \newcommand{\Flounder}{{\it flounder}}

280: \newcommand{\Error}{{\it error}}

281: \newcommand{\Prune}{{\it prune}}

282: \newcommand{\cut}{\mbox{\it cut}}

283: % from art/at.tex

284: 

285: \newcommand{\p}[2]{\langle #1 \ ; \ #2 \rangle}

286: 

287: \newcommand{\ceiling}[1]{\lceil #1 \rceil}

288: \newcommand{\floor}[1]{\lfloor #1 \rfloor}

289: 

290: %%%%%%%%%%% for color slides

291: 

292: \newcommand{\mytitle}[1]

293: {\begin{center}\begin{Sbox} {\bf #1}\end{Sbox}\shadowbox{\TheSbox}\end{center}}

294: 

295: \newcommand{\myctitle}[1]

296: {\textRed\begin{center}\begin{Sbox} {\bf #1}\end{Sbox}\shadowbox{\TheSbox}\end{center}\textBlack}

297: 

298: %\newcommand{\blue}[1]

299: %{\textBlue#1\textBlack}

300: 

301: %\newcommand{\red}[1]

302: %{\textRed#1\textBlack}

303: 

304: %\newcommand{\brown}[1]

305: %{\textBrown#1\textBlack}

306: 

307: \newcommand{\bblue}[1]

308: {\textBlue{\bf#1}\textBlack}

309: 

310: \newcommand{\bred}[1]

311: {\textRed{\bf#1}\textBlack}

312: 

313: \newcommand{\bbrown}[1]

314: {\textBrown{\bf#1}\textBlack}

315: 

316: \newenvironment{page}{\newpage \Huge}{}

317: %%%%%%%%%%% for color slides

318: % end cmds.tex

319: 

320: 

321: \newcommand{\almazero}{{\sf Alma-0}}

322: \parindent0em

323: 

324: \pagestyle{plain}

325: 

326: \begin{document}

327: \date{}

328: \maketitle

329: 

330: 

331: \begin{abstract}

332:   We provide a denotational semantics for first-order logic that

333:   captures the two-level view of the computation process typical for

334:   constraint programming.  At one level we have the usual program

335:   execution.  At the other level an automatic maintenance of the

336:   constraint store takes place.

337:   

338:   We prove that the resulting semantics is sound with respect to the

339:   truth definition. By instantiating it by specific forms of

340:   constraint management policies we obtain several sound evaluation

341:   policies of first-order formulas.  This semantics can also be used a

342:   basis for sound implementation of constraint maintenance in presence

343:   of block declarations and conditionals.

344: 

345: \end{abstract}

346: 

347: \section{Introduction}

348: \label{sec:introduction}

349: 

350: By the celebrated result of Turing first-order logic is undecidable.

351: In particular, the question of determining for an interpretation

352: whether a first-order formula is satisfiable and finding a satisfying

353: substitution if it is, is undecidable.  Still, for many formulas this

354: question can be answered in a straightforward way.  Take for instance

355: the following simple formula interpreted over the standard

356: interpretation for arithmetics:

357: \begin{equation}

358:   \label{formula1}

359: y < z \A y = 1 \A z = 2  

360: \end{equation}

361: It is easy to see that it is satisfied by the substitution

362: $\C{y/{\bf 1}, z/{\bf 2}}$.  Similarly, it is easy to see that the

363: formula

364: \begin{equation}

365:   \label{formula2}

366: \neg (x = 1) \A x = 0  

367: \end{equation}

368: is satisfied by the substitution $\C{x/{\bf 0}}$. 

369: 

370: The question is whether we can capture this concept of

371: ``straightforwardness'' in a natural way. Our first attempt to answer

372: this question was given in Apt and Bezem \cite{AB99} by providing a

373: natural operational semantics for first-order logic which is

374: independent of the underlying interpretation for it.  It captures the

375: computation process as a search for a satisfying substitution for the

376: formula in question.  Because the problem of finding such a substitution

377: is in general undecidable, we introduced in it the possibility of a

378: partial answers in the form of a special $\error$ state indicating a

379: run-time error.  In Apt \cite{Apt00} we slightly extend this

380: approach by explaining how more general equalities can be handled and

381: formulate it in the form of a denotational semantics for first-order

382: logic.  Unfortunately, both semantics are too weak to deal properly

383: with formulas (\ref{formula1}) and (\ref{formula2}): for both of them

384: the $\error$ state is generated.

385: 

386: In this paper we try to overcome these limitations by providing a

387: computational interpretation of first-order logic in the spirit of

388: constraint programming. According to this view the computation process

389: takes place on two levels. At one level we have the usual program

390: execution.  At the other level, in the ``background'' inaccessible to

391: the user, an automatic maintenance of the constraint store takes

392: place.

393: The problem we tackle is undecidable, so we introduce the possibility

394: of partial answers. They are modeled now by a non-empty

395: constraint store or the $\error$ state.

396: 

397: The automatic maintenance of the constraint store is modeled by a

398: parametric \emph{infer} operation that acts on states.  The idea of

399: an abstract \emph{infer} operation is due to Jaffar and Maher

400: \cite{jaffar-survey}. Here we consider it in presence of arbitrary

401: first-order formulas.  Because of this generality we can obtain

402: various sound realizations of the constraint store management by

403: appropriately instantiating \emph{infer}.  The correctness of this

404: approach is formalized in the form of an appropriate soundness result.

405: To establish it we need to assume some properties of the \emph{infer}

406: operation. They are formulated as five ``healthiness'' conditions. 

407: 

408: To illustrate the benefits of this view of first-order logic and to

409: show the scope of the soundness result, we discuss several ways of

410: instantiating the $\infer$ parameter to specific constraint management

411: policies.  Examples include admission of a constraint store consisting

412: of arbitrary first-order formulas, restriction to a constraint store

413: consisting only of atomic constraints, and restriction to a constraint

414: store consisting only of arbitrary first-order positive formulas.  We

415: can also discuss in this framework in a uniform way unification, an

416: algorithm for solving equations and disequations over the Herbrand

417: algebra, and Gaussian elimination in presence of arithmetic

418: constraints.

419: 

420: On the more practical side, these considerations lead to specific

421: implementation proposals of the constraint store in presence of block

422: declarations and conditionals, here modeled, respectively, by means

423: of existential quantification and of negation, conjunction and

424: disjunction.

425: 

426: To clarify these issues we return to formula

427: (\ref{formula1}).  If we do not admit a constraint store, as in the

428: semantics of \cite{AB99} and \cite{Apt00}, its evaluation yields the

429: $\error$ state, since we cannot evaluate $y < z$ without knowing the

430: values for $y$ and $z$.  But if we do allow atomic constraints in the

431: store, we can postpone the evaluation of $y < z$ and the evaluation

432: yields the substitution $\C{y/{\bf 1}, z/{\bf 2}}$.

433: 

434: Next, let us reconsider formula (\ref{formula2}).  If only atomic

435: formulas are allowed as constraints, the evaluation of this formula

436: yields the $\error$ state, since we can neither evaluate $\neg (x =

437: 1)$ nor add this formula to the constraint store. If, however, negated

438: formulas are allowed in the constraint store the substitution

439: $\C{x/{\bf 0}}$ is an answer.  The soundness theorem states that each

440: computed substitution satisfies the evaluated formula.

441: 

442: The question of providing an appropriate semantics for first-order

443: logic in the spirit of constraint programming could be approached by

444: taking for a formula $\phi(\bar{x})$ a clause $p(\bar{x}) \la

445: \phi(\bar{x})$, where $p$ is a new relational symbol and by applying

446: to it a transformation in the style of Lloyd and Topor \cite{LT84}.

447: The outcome would be a constraint logic program that uses negation.

448: After clarifying how to deal properly with negation this could yield a

449: rather indirect answer to the question we study. In contrast, our

450: approach, expressed in the form of a denotational semantics, is much

451: more direct and conceptually transparent: the meaning of each formula

452: is expressed directly in terms of the meaning of its constituents and

453: it is parametrized in a simple way by the \emph{infer} operation.

454: 

455: The rest of the paper is organized as follows.

456: In Section \ref{sec:general} we introduce the $\infer$ operation and

457: discuss in detail the requirements we impose on it. The main

458: difficulty has to do with the appropriate treatment of existential

459: variables.  In Section \ref{sec:sem} we define our denotational

460: semantics.  Next, in Section \ref{sec:apt} we show that the proposed

461: semantics subsumes the denotational semantics provided in

462: \cite{Apt00}.  Then in Section \ref{sec:specifi} we discuss various

463: increasingly powerful forms of constraint store management, each

464: modeled by means of a particular $\infer$ operation.

465: Finally, in Section \ref{sec:related} we discuss related work.

466: 

467: \section{Towards the denotational semantics}

468: \label{sec:general}

469: 

470: Below we work our way towards our proposal for the

471: denotational semantics in several steps,

472: first introducing the basic semantic ingredients, then discussing

473: the crucial conditions on the $\infer$ parameter and finally

474: presenting the denotational semantics for first order

475: logic with $\infer$ parameter.

476: In the next section we will then state the soundness result

477: for the semantics. The proof details are referred to the appendix.

478: We discuss several ways of instantiating the $\infer$ parameter

479: to show the scope of the soundness result.

480: In the final section we review the goals and results and look ahead

481: to further developments.

482: 

483: \paragraph{{\bf Preliminaries}}

484: \label{sub:prelim}

485: 

486: Let's assume that an algebra ${\cal J}$ is given over which we want to perform

487: computations.

488: The basic ingredient of the semantic universe will be the set of states,

489: $\states$. States come

490: in two kinds. First we have an $\myerror$ state, which remains unanalyzed.

491: All other states consist of two components: one component is a constraint 

492: store $\csp$, the other a substitution $\theta$. Such a state is then written 

493: $\tupel{\csp ;\theta}$. As always, a substitution 

494: $\theta$ is a mapping from variables to terms. It assigns a term 

495: $x\theta$ to each variable $x$, but there are only finitely many variables 

496: for which $x\neq x\theta$. These variables form $dom(\theta )$, the 

497: domain of $\theta$. 

498: The application of a substitution $\theta$ to a term $t$, written 

499: $t\theta$, is defined as usual. We denote the empty substitution by

500: $\epsilon$.

501: 

502: A constraint store $\csp$, 

503: is simply a finite set of formulas of first order logic. In many applications

504: there are extra requirements on the syntactic form of a constraint store,

505: but for now we keep things as general as possible. $\bot$ is a special

506: formula which is always false.

507: 

508: Throughout the paper we try to limit the number of brackets 

509: and braces

510: as much as possible. In particular, for a finite set $\verz{A_1,\ldots,A_n}$

511: we will often write $A_1, \ldots,A_n$. Also, 

512: we write $\infer\tupel{\csp ;\theta }$ instead  of 

513: $\infer(\tupel{\csp  ;\theta})$, etc.

514: 

515: \paragraph{{\bf The treatment of local variables: dropping things}}

516: \label{sub:local}

517: 

518: An important ingredient of the set up is

519: the ${\it DROP}_u$ mapping on states. It is the way we deal with

520: local variables. This works in two steps: first

521: we define the substitution {\it DROP}$_u(\theta )$ for each 

522: variable $u$ and substitution $\theta$, as in \cite{Apt00}:\\

523: 

524: \begin{tabular}{ll}

525: $u {\it DROP}_u(\theta )$ $=\; u$\\

526: $x {\it DROP}_u(\theta )$ $=\; x\theta$ \mbox{for all other variables $x$}\\

527: \end{tabular}\\

528: 

529: So, ${\it DROP}_u$ makes the current value of $u$ disappear,

530: thus capturing the idea of a local variable to the substitutions.

531: But we also have another component in states: the constraint

532: store. Dropping $u$ from such a set of formulas 

533: compares to existential quantification over $u$. 

534: There is one little extra point to take care of, however: in a state

535: $\tupel{\csp  ;\eta}$ the information that $\eta$ provides about the value

536: of $u$ is implicitly available  to $\csp$. Therefore, we perform the 

537: quantification $\exists u$ only

538: after adding the information about the value of $u$ explicitly to $\csp$.

539: Also the values $y\eta$ in which $u$ appears have to be kept in mind.

540: We take the conjunction of the equations $y=y\eta$ for all such

541: variables $y$ and write it as ${\bf y}={\bf y}\eta$. 

542: This leads us to the following formula that takes care of

543: the local variables in $\csp$. 

544: 

545: \begin{quote}

546: $\exists u\; (u=u\eta \;\wedge\; {\bf y}={\bf y}\eta\;\wedge\; \bigwedge\csp )$

547: \end{quote}

548: 

549: Note that this formula depends both

550: on $u$ and $\eta$. So, we cannot define a drop$_u$-mapping on constraint

551: stores alone: we have to know $\eta$ as well.

552: 

553: This formula expresses the information we are after in a uniform way,

554: but in `borderline cases' the syntactic format is awkward. For example,

555: if $\csp =\emptyset$, we get a trivial existential quantification

556: over the first two conjuncts. This existential quantifier is 

557: semantically harmless, but specific constraint propagation formalisms

558: simply do not work on existentially quantified formulas. Therefore we

559: rather adopt a format in which

560: the quantifier only appears if it is really necessary.

561: 

562: This is done in two steps:

563: first, the quantification over $u$ only matters for the

564: formulas in $\csp$ in which $u$ actually occurs. We make this explicit

565: in the definition by distinguishing  $\csp (u)$, the subset

566: of $\csp$ that contains exactly the formulas with the free variable 

567: $u$.

568: In the formula we use for the drop$_u$-mapping we can then always take

569: $\csp -\csp (u)$ outside the scope of the quantifier. This gives:

570: \begin{quote}

571: $\csp -\csp (u)\; ,\; \exists u\;

572:         (u=u\eta \;\wedge\; {\bf y}={\bf y}\eta\;\wedge\; \bigwedge\csp (u))$

573: \end{quote}

574: Finally, in the special case $\csp (u) =

575: \emptyset$, we leave out the existentially quantified formula altogether.

576: 

577: For the $\myerror$-state we simply set: 

578: $\mbox{\sc drop}_u\myerror =\myerror$.

579: To summarize, the  mapping $\mbox{\sc drop}_u$ is defined on states by 

580: the following cases:\\

581: 

582: \begin{tabular}{|llll|}

583: \hline

584: &&&\\

585: $\;\mbox{\sc drop}_u\tupel{\csp  ;\eta}$ & $=$&$ \tupel{\csp  ;

586:         \mbox{\it DROP}_u (\eta ) }$ & if $\csp (u)=\emptyset\;\;$\\[2mm]

587: $\;\mbox{\sc drop}_u\tupel{\csp  ;\eta}$ & $=$&

588:         $ \langle\;\exists u\; (u=u\eta \;\wedge\; {\bf y}={\bf y}\eta

589:         \;\wedge\; \bigwedge\csp (u)),$&\\

590: $\;$ & &        \hspace{2cm}$\; \csp -\csp (u);\;\;\;\;\;\;

591:                 \mbox{\it DROP}_u (\eta )\rangle$ 

592:         & if $\csp (u)\neq\emptyset\;\;$\\[2mm]

593: $\;\mbox{\sc drop}_u \myerror $ & $=$ & $\myerror$ &\\

594: $\;$&&&\\

595: \hline

596: \end{tabular}

597: 

598: 

599: \paragraph{{\bf Conditions on infer}}

600: \label{sub:conditions}

601: 

602: Another important ingredient of the framework is the $\infer$ mapping.

603: $\infer$ maps a state to a set of states.

604: The $\infer$ mapping is the basic notion of computation in the semantics:

605: we do not specify what happens `within' the $\infer$ mapping.

606: This makes the set up extremely general: the $\infer$ steps can consist of 

607: calls to a constraint 

608: solver, like a unification algorithm or an algorithm for solving linear

609: equations over reals, calls to a constraint propagation algorithm,

610: or other atomic computation steps.

611: Several instances of

612: the $\infer$ mapping will be discussed in more detail later on.

613: 

614: We can almost get away with 

615: complete generality regarding $\infer$. To make sure that

616: the formalism respects first order logic, we have to make a few modest

617: requirements. 

618: Let us write $\tupel{\csp  ;\theta}\models_{\cal J}\phi$ for

619: $\csp\theta\models_{\cal J}\phi\theta$. In particular 

620: $\tupel{\emptyset ;\theta}

621: \models_{\cal J}\phi$ iff $\models_{\cal J}\phi\theta$.

622: Then the restrictions that we need in the soundness proof below,

623: read as follows:

624: 

625: \begin{description}

626: \item[(1) Equivalence:] 

627:         if $\tupel{\csp '  ;\theta '}\in \infer\tupel{\csp  ;\theta} $, then

628:         $\tupel{\csp  ;\theta}\models_{\cal J}\phi$ iff

629:         $\tupel{\csp ';\theta '}\models_{\cal J}\phi $ 

630: \item[(2) Renaming:] 

631:         if $\tupel{\csp '  ;\theta '}\in \infer\tupel{\csp  ;\theta} $, then

632:         also $\tupel{\csp '_v ;\theta '_v} \in \infer \tupel{\csp  ;\theta}$,

633: 

634:         where $\tupel{\csp '_v ;\theta '_v}$ is obtained from 

635:         $\tupel{\csp ' ;\theta '}$ by replacing all occurrences

636:         of $u$ by $v$ for a variable $u$ that is fresh w.r.t. 

637:         $\tupel{\csp  ;\theta}$ and a variable $v$ that is fresh w.r.t. both

638:         $\tupel{\csp  ;\theta}$ and $\tupel{\csp ' ;\theta '}$ 

639: \item[(3) Inconsistency:] if $\infer\tupel{\csp  ;\theta}=\emptyset$, then 

640:         $\tupel{\csp  ;\theta}\models_{\cal J}\bot$

641: \item[(4) Error:] $\infer\;\myerror =\verz{\myerror}$

642: \item[(5) Identity:] $\infer\tupel{\emptyset ;\theta}=

643:         \verz{\tupel{\emptyset ;\theta}}$

644: \end{description}

645: 

646: So, the $\infer$ mapping should respect logical equivalence,

647: i.e., the state $\tupel{\csp ' ;\theta '}$ that we reach starting 

648: from $\tupel{\csp  ;\theta}$, should still make the same formulas true.

649: Furthermore, the $\infer$ mapping should not be sensitive to the choice of

650: fresh variables: if $\infer$ works for $u$, 

651: it should also work for an alternative fresh variable $v$.

652: Finally, $\infer$ should respect falsity and the $\myerror$ state.\footnote{The

653: Identity requirement is not necessary for the proof of the soundness 

654: theorem, but it seems too natural to leave it out. Renaming is used only

655: in the proof of the Preservation/Persistence Lemma in

656: the case of the existential formula.}

657: When we talk about the consistency of states, we are dealing with

658: a three way distinction. We say that a state $\sigma$ is:

659: %\begin{tabular}{ll}

660: ${\cal J}$-consistent,  if $\sigma \neq\myerror$ and 

661:         $\sigma \not\models_{\cal J}\bot$;

662: ${\cal J}$-inconsistent, if $\sigma \neq\myerror$ and 

663:         $\sigma \models_{\cal J}\bot$;

664: error, if $\sigma =\myerror$.

665: %\end{tabular}\\

666: For a set of states $\Sigma\subseteq\states$ we then distinguish:

667: %\begin{tabular}{ll}

668: $\mycons_{\cal J} (\Sigma )$ $=\; \verz{\sigma\in\Sigma:\; \sigma\mbox{ is

669:         $\cal J$-consistent} }$ and

670: $\mycons_{\cal J}^+ (\Sigma )$  $=\; \verz{\sigma\in\Sigma:\; \sigma\mbox{ is

671:         not $\cal J$-inconsistent} }$.

672: %\end{tabular}\\

673: Usually it is clear to which ${\cal J}$ we refer and

674: we omit ${\cal J}$ from the notation.\\

675: 

676: \section{Denotational semantics}

677: \label{sec:sem}

678: 

679: We now define a denotational semantics for first order logic 

680: in which the $\infer$ mapping is a parameter. The parameter can be

681: set to give the semantics from Apt \cite{Apt00}, for example, but many 

682: other settings are available, as we will see below. This way

683: we obtain general results, that apply uniformly to various 

684: forms of constraint store management.

685: 

686: We define the mapping 

687: $\mysem{\phi}:\; \states\rightarrow\states$, using 

688: postfix notation.\footnote{We also sneak in the notation: 

689: $\Sigma\mysem{\phi}$ for 

690: $\bigcup_{\sigma\in\Sigma}\verz{\sigma\mysem{\phi}}$.}\\

691: 

692: \begin{tabular}{|ll|}

693: \hline

694: &\\ $\;\tupel{\csp  ;\theta}\mysem{A}\; $&

695: 	$=\; \infer \tupel{\csp ,{A}  ;\theta}$

696:         \hspace{.8cm} for an atomic formula $A$

697: \\[2mm] $\;\tupel{\csp  ;\theta}\mysem{\phi_1\vee\phi_2}\;$&$ =\; 

698:         \tupel{\csp  ;\theta}\mysem{\phi_1}\; \cup\; 

699:         \tupel{\csp  ;\theta}\mysem{\phi_2}$

700: \\[2mm] $\;\tupel{\csp  ;\theta}\mysem{\phi_1\wedge\phi_2}\;$&$ =\;

701:         (\tupel{\csp ;\theta}\mysem{\phi_1})\mysem{\phi_2}$

702: %       \tupel{ X,\theta}\mysem{\phi_1}}$

703: \\[2mm] $\;\tupel{\csp  ;\theta}\mysem{\neg\phi}\;$&$ =

704:         \left\{

705:         \begin{tabular}{ll}

706:         $\infer\tupel{\csp  ;\theta}$ &

707: %       \mbox{if } every $\tupel{\csp ' ;\theta '}\in\tupel{\csp 

708: %               ,\theta}\mysem{\phi}$\\

709: %       \mbox{if } every $\sigma\in\tupel{\csp 

710: %               ,\theta}\mysem{\phi}$\\

711: %       & \mbox{is inconsistent}\\ 

712:         \mbox{if } $\mycons^+ (\tupel{\csp  ;\theta}\mysem{\phi})=\emptyset$\\

713:         

714: %%      $\verz{\tupel{X,\theta}}$ &

715: %       $\verz{\tupel{X',\theta}:\; X\infer_{\theta}X'}$ &

716: %%      \mbox{if } $\tupel{X,\theta}\mysem{\phi}\; =\; \emptyset$\\

717: %       \mbox{if } $\tupel{X'',\theta ''}\in\tupel{X,\theta}\mysem{\phi}$\\

718: %       & \mbox{only occurs for inconsistent $X''\theta ''$}\\[2mm]

719:         $\emptyset$ &

720: %       $\infer(\tupel{\verz{\bot},\theta})$ &

721:         \mbox{if }$\tupel{\csp ' ;\theta '}\in

722:                 \mycons(\tupel{\csp  ;\theta}\mysem{\phi})$

723:         \mbox{ for}\\ &

724:         \mbox{some $\tupel{\csp ' ;\theta '}$ equivalent to

725:         $\tupel{\csp  ;\theta}$} \\[2mm]

726:         $\infer\tupel{\csp ,{\neg\phi}  ;\theta}$ &

727: %       $\{\tupel{X',\theta}:\; $&\\

728: %       $\;\; (X\cup\verz{\neg\phi})\infer_{\theta}\; X'\}$ &

729:         \mbox{otherwise}

730:         \end{tabular}

731:         \right.$\\[2mm]

732: $\;\tupel{\csp  ;\theta}\mysem{\exists x\; \phi}\;$&$ =\;

733: %       \bigcup_{\tupel{\csp ',\eta}}\verz{\infer({\mbox{\sc drop}_u

734: %               (\tupel{\csp ',\eta})})}$

735: %

736: %       where $\tupel{\csp ',\eta}$ ranges over the consistent states

737: %       in $\tupel{\csp ,\theta}\mysem{\phi\verz{x/u}}$ (for some fresh $u$)

738:         \bigcup_{\sigma}\verz{\infer{\;\mbox{\sc drop}_u

739:                 (\sigma )}}$

740: 

741:         where, for some fresh $u$,\\

742:         & \hspace{1.6cm} $\sigma$ ranges over $\mycons^+ (

743:         \tupel{\csp  ;\theta}\mysem{\phi\verz{x/u}})$ 

744: \\[2mm] $\;\myerror \mysem{\phi} \;$&$=\; \verz{\myerror}$  

745: 		\mbox{ for all $\phi$}\\

746: &\\ \hline

747: \end{tabular}

748: 

749: \vspace{2mm}

750: 

751: 

752: The definition relies heavily on the notation that was introduced before. But

753: it is still quite easy to see what goes on. The atomic formulas are

754: handled by means of the 

755: $\infer$ mapping. Then, disjunction is interpreted as nondeterministic

756: choice,

757: and conjunction as sequential composition. For existential quantification

758: we use the $\weg _u$ mapping (for a fresh variable $u$). The $\myerror$ clause

759: says that there is no recovery from $\myerror$. In the case for negation,

760: three contingencies are present: first, the case where $\phi$ is 

761: inconsistent. Then we

762: continue with the input state $\tupel{\csp  ;\theta}$.

763: Secondly, the case where $\phi$ is already true in (a state 

764: equivalent to)

765: the input state. Then we conclude that $\neg\phi$ yields 

766: inconsistence, i.e., we get $\emptyset$. Finally, we add $\neg\phi$

767: to the constraint store $\csp$ if it is impossible at this point to reach

768: a decision about  the status of $\neg\phi$.

769: 

770: 

771: %\paragraph{{\bf Respecting first order logic: soundness}}

772: \label{sec:sound}

773: 

774: Next we show that the denotational

775: semantics with the $\infer$ parameter is sound. This 

776: amounts to two things:

777: %\begin{tabular}{ll}

778: {\it 1.}  successful

779: computations of $\phi$ result in states in which $\phi$ holds;

780: {\it 2.}  if no 

781: successful computation of $\phi$ exists, $\phi$ is false in 

782: the initial state.

783: %\end{tabular}

784: \begin{theorem}[Soundness]

785: Let $\tupel{\csp ;\theta}$ and $\phi$ be given. Then we have:

786: 

787: %\begin{enumerate}

788: %\item If $\tupel{\csp' ;\theta '}\in\tupel{\csp ;\theta}\mysem{\phi}$, then

789: %        $\csp'\theta '\models_{\cal J}\phi\theta '$

790: %\item If $\tupel{\csp',\theta '}\in\tupel{\csp,\theta}\mysem{\phi}$ occurs

791: %        only with inconsistent $\csp'\theta '$,

792: %        then $\csp\theta\models_{\cal J}\neg\phi\theta$.

793: %\end{enumerate}

794: \begin{enumerate}

795: \item If $\tupel{\csp' ;\theta '}\in\tupel{\csp ;\theta}\mysem{\phi}$, then

796:         $\tupel{\csp'  ;\theta '}\models_{\cal J}\phi$

797: \item If $\mycons^+ (\tupel{\csp ;\theta}\mysem{\phi})=\emptyset$ ,

798:         then $\tupel{\csp  ;\theta}\models_{\cal J}\neg\phi$.

799: \end{enumerate}

800: \end{theorem}

801: 

802: The proof of the theorem is by

803: a simultaneous induction on the structure of the formula $\phi$.

804: In the proof we need a preservation/persistence result, that we give

805: as a separate lemma.

806: 

807: \begin{lemma}[Preservation/Persistence]

808: \mbox{}

809: 

810: %\begin{enumerate}

811: %\item  If $\csp \theta\models_{\cal J}\phi_1\theta$ and 

812: %$\tupel{\csp '',\theta ''}\in \tupel{\csp ,\theta}\mysem{\phi_2}$, then

813: %$\csp ''\theta ''\models_{\cal J}\phi_1\theta ''$ \hfill{(validity)}

814: %\item If $\csp \theta$ and $(\phi_1\wedge\phi_2)\theta$ 

815: %are consistent 

816: %(in ${\cal J}$)

817: %and $\tupel{\csp ',\theta '}\in \tupel{\csp ,\theta}\mysem{\phi_2}$ is

818: %a consistent state, then 

819: %$\csp '\theta '$ and $(\phi_1\wedge\phi_2)\theta '$

820: %are consistent

821: %(in ${\cal J}$).

822: %\hfill{(consistency)}

823: %\end{enumerate}

824: \begin{enumerate}

825: \item  If $\tupel{\csp  ;\theta}\models_{\cal J}\phi_1$ and 

826: %$\tupel{\csp '' ;\theta ''}\in \tupel{\csp  ;\theta}\mysem{\phi_2}$, then

827: $\tupel{\csp ' ;\theta '}\in \tupel{\csp  ;\theta}\mysem{\phi_2}$, then

828: %$\tupel{\csp '' ;\theta ''}\models_{\cal J}\phi_1$ \hfill{(validity)}

829: $\tupel{\csp ' ;\theta '}\models_{\cal J}\phi_1$ \hfill{(validity)}

830: \item If $\csp \theta$ and $(\phi_1\wedge\phi_2)\theta$ 

831: are mutually consistent 

832: (in ${\cal J}$) and 

833: 

834: $\tupel{\csp ' ;\theta '}\in \mycons (\tupel{\csp  ;\theta}\mysem{\phi_2})$, 

835: 

836: then $\csp '\theta '$ and $(\phi_1\wedge\phi_2)\theta '$

837: are mutually consistent

838: (in ${\cal J}$).

839: \hfill{(consistency)}

840: \end{enumerate}

841: \end{lemma}

842: 

843: The lemma says that computations of $\mysem{\phi_2}$ will not disturb

844: the status of $\mysem{\phi_1}$: the computation preserves validity and 

845: consistency.

846: The proof of the lemma is by a 

847: simultaneous induction  on the structure of $\phi_2$.

848: Some proof details are given in the appendix. 

849: Here we continue by considering several instantiations of the general format.

850: 

851: 

852: \section{Modeling the denotational semantics of Apt \cite{Apt00}}

853: \label{sec:apt}

854: 

855: We start our analysis by recalling the semantics provided in

856: \cite{Apt00}.  The idea of this semantics is to provide a uniform

857: computational meaning for the first-order formulas independent of the

858: underlying interpretation and without a constraint store. This yields a

859: limited way of processing formulas in the sense that occasionally an

860: $\myerror$ may arise.  After we have reintroduced this semantics we shall

861: discuss a number of its extensions, all involving a specific

862: constraint store management.  So, let us recall the relevant

863: definitions.

864: 

865: \begin{definition} 

866:   Assume a language of terms $L$ and an algebra ${\cal J}$ for it.

867: 

868: 

869: \begin{itemize}

870: \item Consider a term of $L$ in which we replace some of the variables

871: by the elements of the domain $D$. We call the resulting object

872: a {\em generalized term}.

873: 

874: \item Given a generalized term $t$ we define its {\em ${\cal

875:       J}$-evaluation\/} as follows.  Each ground term of $s$ of $L$

876:   evaluates to a unique value in ${\cal J}$. Given a generalized term

877:   $t$ replace each maximal ground subterm of $t$ by its value in

878:   ${\cal J}$.  We call the resulting generalized term a {\em ${\cal

879:       J}$-term} and denote it by $\B{t}_{\cal J}$.

880:   

881: \item By a {\em ${\cal J}$-substitution\/} we mean a finite mapping

882: from variables to ${\cal J}$-terms which assigns to each variable $x$

883: in its domain a ${\cal J}$-term different from $x$.  We write it as

884: $\C{x_1/h_1,\dots,x_n/h_n}$.  

885: We define the notion of an application of a ${\cal J}$-substitution

886: $\theta$ to a generalized term $t$ in the standard way and denote it

887: by $t \theta$.  

888: 

889: \item A {\em composition of two ${\cal J}$-substitutions $\theta$

890: and $\eta$}, written as $\theta \eta$, is defined as the unique

891: ${\cal J}$-substitution $\gamma$ such that for each variable $x$

892: \[

893: x \gamma = \B{(x \theta) \eta}_{\cal J}. 

894: \]

895: %\HB

896: \end{itemize}

897: \end{definition}

898: 

899: The ${\cal J}$-substitutions generalize both the usual substitutions

900: and the valuations, which assign domain values to variables.

901: After these introductory definitions we recall the semantics

902: $\newMS{\cdot}$ of an equation between

903: two generalized terms (so {\it a fortiori}, between two terms).

904: Here and elsewhere we do not indicate the dependency of the semantics

905: on the underlying interpretation or algebra.

906: 

907: \begin{eqnarray*}

908: \begin{array}{lll}

909: \newMS{s=t}(\theta) & :=  &

910: \left\{

911: \begin{array}{ll}

912: \C{\theta \C{s\theta/\B{t\theta}_{\cal J}}} &  

913: \mbox{if $s\theta$ is a variable 

914: that does not occur in $t\theta$,} \\

915: \C{\theta \C{t\theta/\B{s\theta}_{\cal J}}} &  

916: \mbox{if $t\theta$ is a variable 

917: that does not occur in $s\theta$} \\

918:                                            &   

919: \mbox{and $s\theta$ is not a variable,} \\

920: \C{\theta} &  

921: \mbox{if $\B{s\theta}_{\cal J}$ and $\B{t\theta}_{\cal J}$ are identical,} \\

922: \ES &  \mbox{if $s\theta$ and $t\theta$ are ground and 

923: $\B{s\theta}_{\cal J} \neq \B{t\theta}_{\cal J}$,} \\

924: \C{\myerror} &  \mbox{otherwise.}

925: \end{array}

926: \right.

927: \end{array}

928: \end{eqnarray*}

929: 

930: Consider now an interpretation ${\cal I}$ based on an algebra ${\cal J}$.

931: Given an atomic formula $p(t_1, \LL, t_n)$  different from $s=t$ and a ${\cal

932:   J}$-substitution $\theta$ we denote by $p_{\cal I}$ the

933: interpretation of $p$ in ${\cal I}$.

934: We say that

935: 

936: \begin{itemize}

937: 

938: \item $p(t_1, \LL, t_n)\theta$ is {\em true\/} if

939: $p(t_1, \LL, t_n)\theta$ is ground

940: and $(\B{t_{1}\theta}_{\cal J}, \LL, \B{t_{n}\theta}_{\cal J}) \in p_{\cal I}$,

941: 

942: \item $p(t_1, \LL, t_n)\theta$ is {\em false\/} if

943: $p(t_1, \LL, t_n)\theta$ is ground

944: and $(\B{t_{1}\theta}_{\cal J}, \LL, \B{t_{n}\theta}_{\cal J}) 

945: 	\not\in p_{\cal I}$.

946: 

947: \end{itemize}

948: 

949: To deal with the existential quantification we use the

950: $DROP_x$ operation defined in Section \ref{sub:local},

951: extended in the standard way to the

952: subsets of $Subs \cup \C{error}$.

953: Now $\newMS{\cdot}$ is defined by structural induction as follows.

954: $A$ is here an atomic formula different from $s=t$.

955: 

956: \begin{itemize}

957: 

958: \item $\newMS{A}(\theta) :=

959: \left\{

960: \begin{array}{ll}

961: \C{\theta} &  \mbox{if $A \theta$ is true,} \\

962: \ES &  \mbox{if $A \theta$ is false,} \\

963: \C{\myerror} &  \mbox{otherwise, that is if $A \theta$ is not ground,}

964: \end{array}

965: \right.

966: $

967: 

968: \item $\newMS{\phi_1 \A \phi_2}(\theta) 

969: 	:=\newMS{\phi_2}(\newMS{\phi_1}(\theta))$,

970: 

971: \item $\newMS{\phi_1 \Or \phi_2}(\theta) 

972: 	:=\newMS{\phi_1}(\theta) \cup \newMS{\phi_2}(\theta)$,

973: 

974: \item $\newMS{\neg \phi}(\theta) :=

975: \left\{

976: \begin{array}{ll}

977: \C{\theta} &  \mbox{if $\newMS{\phi}(\theta) = \ES$,} \\

978: \ES &  \mbox{if $\theta \in \newMS{\phi}(\theta)$,} \\

979: \C{\myerror} &  \mbox{otherwise,}

980: \end{array}

981: \right.

982: $

983: \item $\newMS{\te x \: \phi}(\theta) := DROP_{u}(\newMS{\phi\C{x/u}}(\theta))$,

984: where $u$ is a fresh variable.

985: 

986: \end{itemize}

987: 

988: The following example clarifies the way we interpret atoms and conjunction.

989: \begin{example} \label{exa:2a}

990:   

991: Assume the standard algebra for the language of arithmetic

992: with the set of integers as domain. 

993: We denote its elements by $\LL, \mathbf{-2,-1,0,1,2}, \LL$.

994: Each constant $i$ evaluates to the element {\bf i}.

995: We then have

996: \begin{enumerate}

997: %\smallromani

998: \item 

999: $\newMS{y = z-1 \A z = x+2}(\C{x/{\bf 1}}) = 

1000: \newMS{z = x+2}(\C{x/{\bf 1}, y/z-{\bf 1}}) =$

1001: 

1002: $ \C{\C{x/{\bf 1}, y/{\bf 2}, z/{\bf 3}}}, $

1003: 

1004: \item 

1005: $ \newMS{y = 1 \A z = 1 \A y-1 = z-1 }(\varepsilon) = 

1006: 	\C{\C{y/{\bf 1}, z/{\bf 1}}},$

1007: 

1008: \item 

1009: $\newMS{y = 1 \A z = 2 \A y < z }(\varepsilon) = \C{\C{y/{\bf 1}, z/{\bf 2}}},$

1010: 

1011: \item 

1012: $\newMS{x = 0 \A \neg (x =1)}(\varepsilon) = \C{\verz{x/{\bf 0}}},$

1013: 

1014: \item \label{item1}

1015: $\newMS{y-1 = z-1 \A y = 1 \A z = 1}(\varepsilon) = \C{\myerror},$

1016: 

1017: \item \label{item2}

1018: $\newMS{y < z \A y = 1 \A z = 2}(\varepsilon) = \C{\myerror},$

1019: 

1020: \item \label{item3}

1021: $\newMS{\neg (x = 1) \A x = 0}(\varepsilon) = \C{\myerror}.$

1022: \end{enumerate}

1023: %\HB

1024: \end{example}

1025: So in this semantics the conjunction is not commutative and consequently it

1026: is important

1027: in which order the formulas are processed.

1028: This semantics is a special case of the semantics provided in 

1029: Section \ref{sec:sem}.

1030: It is obtained by using the following $\infer$ relation:

1031: 

1032: \begin{itemize}

1033: \item $\infer \p{A}{\theta} := \verz{\p{\emptyset}{\eta}:\;

1034:         \eta \in\mysem{A}(\theta )}$ for an atomic formula $A$,

1035: where we identify $\p{\ES}{\myerror}$ with $\myerror$,

1036: %\item $\infer \p{\neg \phi}{\theta} := \verz{\myerror}$,

1037: \item $\infer \p{{\cal C}}{\theta} := \verz{ \myerror }$ 

1038: for all other states $\p{{\cal C}}{\theta}$.

1039: \end{itemize}

1040: 

1041: The relevant `embedding' theorem is the following one.

1042: \begin{theorem}[Embedding]\mbox{}

1043: 

1044: \begin{itemize}

1045: \item $\eta \in\mysem{\phi}(\theta )$ iff  

1046: 	$\p{\emptyset}{\eta} \in \p{\emptyset}{\theta}\mysem{\phi}$.

1047: 

1048: \item $\myerror \in\mysem{\phi}(\theta )$ iff  

1049: $\myerror \in \p{\emptyset}{\eta}\mysem{\phi}$.

1050: \end{itemize}

1051: \end{theorem}

1052: 

1053: 

1054: \section{Specific constraint store managements}

1055: \label{sec:specifi}

1056: 

1057: \newcommand{\aux}[0]{\mbox{\it aux}}

1058: \newcommand{\step}[0]{\mbox{\it step}}

1059: \newcommand{\split}[0]{\mbox{\it split}}

1060: \newcommand{\splitstep}[0]{\mbox{\it splitstep}}

1061: 

1062: We now illustrate the generality of our approach by presenting various

1063: increasingly powerful forms of constraint store management. Each of

1064: them is obtained by a particular propagation $\step$

1065: that works on {\it special states} and is executed 

1066: whenever and as-long-as it can be applied.

1067: $\aux$ is our name for the maximal repetition of the $\step$.\footnote{Note 

1068: that maximal 

1069: repetition of one $\step$ is just one strategy for constraint management.

1070: Already Jaffar and Maher \cite{jaffar-survey} mention other options, 

1071: distinguishing

1072: for example, {\it quick-checking}, {\it progressive} and {\it ideal} {\it CPL}

1073: systems. Of course, our set up can also accommodate such variations.} 

1074: So, 

1075: $\aux$ is a procedure on special states that is the least fixed point of

1076: $\aux = \step\circ\aux$.

1077: %\footnote{Here we omit details about 

1078: %pointwise lifting of the procedures on special states to procudures on 

1079: %{\it sets} of special states.}

1080: %This auxiliary procedure on special states is then used to define the 

1081: Then we can define the

1082: $\infer$ mapping as follows:

1083: 

1084: \begin{tabular}{ll}

1085: $\infer\; \error$ & $=\; \verz{\error}$\\

1086: $\infer \tupel{\emptyset ;\theta }$ & $=\; \verz{\tupel{\emptyset ;\theta}}$\\

1087: $\infer \tupel{\csp ;\theta }$ & $=\; \aux\;\tupel{\csp ;\theta}\;\;\;$

1088:                 for a special state $\tupel{\csp ;\theta}$\\

1089: $\infer \tupel{\csp ;\theta }$ & $=\; \verz{\error} \;\;\;\;\;$ otherwise\\

1090: \end{tabular}

1091: 

1092: Now the examples are obtained by a specification of the special states and

1093: the $\step$ procedure.

1094: In each case it is then straightforward to check that

1095: the adopted definition of $\infer$ satisfies the 

1096: conditions we put on it in Section \ref{sub:conditions}.

1097: Consequently, in each case the Soundness Theorem holds.  Informally,

1098: in each case we provide a sound constraint store management.

1099: 

1100: \paragraph{{\bf Equations as active constraints}}

1101: \label{subsec:equations}

1102: 

1103: Below, following Jaffar and Maher \cite{jaffar-survey}, we make a

1104: distinction between \emph{active} and \emph{passive} constraints.  In

1105: our framework active constraints are the ones that are capable of

1106: changing the values of the variables, while the passive ones boil down

1107: to formulas that become tests after an appropriate instantiation. 

1108: 

1109: 

1110: As an example how active constraints can be modeled using the

1111: presented semantics consider unification as a way of

1112: solving equality constraints.  To model it we choose as the

1113: underlying algebra the Herbrand algebra, the universe of which

1114: consists of the set of all ground terms of the language $L$.

1115: 

1116: The constraint stores of special states only contain 

1117: equations.  The equations are active, and each step 

1118: consists of unification, whenever possible. So, we put:

1119: 

1120: \[

1121: \step \p{\emptyset}{\theta}:= \emptyset

1122: \]

1123: \[

1124: \step \p{{\cal C}, s = t}{\theta}

1125:  :=

1126: \left\{

1127: \begin{array}{ll}

1128: \C{\p{{\cal C}}{\theta\eta}} &  

1129: 	\mbox{if $\eta$ is an mgu of $s\theta$ and $t\theta$,} \\

1130: \ES                 &    \mbox{if $s\theta$ and $t\theta$ are not unifiable.}

1131: \end{array}

1132: \right.

1133: \]

1134: 

1135: Other specific forms of active constraints can be modeled

1136: in our framework in an equally straightforward way.

1137: 

1138: 

1139: \paragraph{{\bf Atoms as passive constraints}}

1140: 

1141: \label{subsec:atoms}

1142: 

1143: The drawback of the semantics defined in the previous

1144: section is that it yields $\error$ when

1145: a wrong order of conjuncts is accidentally chosen. A possible remedy is to use

1146: atoms as passive constraints, i.e., to move the atoms that currently 

1147: evaluate to $\error$ to the constraint store instead. 

1148: 

1149: For the handling of passive constraints we include a $\split$

1150: procedure on special states to isolate the passive constraints:

1151: $\split\tupel{\csp ;\theta}\; =\; \tupel{\csp_p,\csp_a ;\theta}$, where

1152: $\csp_p$ is a list of the constraints that are passive when evaluated 

1153: by $\theta$ and 

1154: $\csp_a$ is a list of the constraints that are active when evaluated 

1155: by $\theta$.

1156: When this is done, we perform a $\step$ on the  active constraints.

1157: Next we re-group the constraints to reconsider the

1158: active-passive $\split$ in the new state. So, the step

1159: we perform in the auxiliary procedure 

1160: is a composed action: $\aux = \splitstep \circ \splitstep$

1161: and  $\splitstep =\split\circ\step$.\footnote{We 

1162: ignore various implementation details regarding the particular

1163: choice of an active

1164: constraint and the distinction between lists and sets.}

1165: 

1166: In the current example we set the $\split$ procedure as

1167: indicated: we regard the atoms that would evaluate to

1168: $\error$ passive. Then the $\step$ works as follows:\\

1169: 

1170: \begin{tabular}{lll}

1171: $\step \tupel{\csp_p ;\theta}$

1172:         &  $= \; \verz{\tupel{\csp_p ;\theta}}$

1173:         & if no active constraints occur\\

1174: $\step \tupel{\csp_p,\csp_a, s=t ;\theta}$

1175:         & $=\; \verz{\tupel{\csp_p,\csp_a

1176:                  ;\theta\eta}}$

1177:         & if $\eta$ is an mgu of $s\theta ,\; t\theta$\\

1178: $\step \tupel{\csp_p,\csp_a, s=t ;\theta}$

1179:         & $=\;\emptyset$

1180:         & if $s\theta ,\; t\theta$ cannot be unified\\

1181: $\step \tupel{\csp_p,\csp_a, A ;\theta}$

1182:         & $=\;\verz{\tupel{\csp_p,\csp_a

1183:                  ;\theta}}$

1184:         & if $A\theta$ is true\\

1185: $\step \tupel{\csp_p,\csp_a, A ;\theta}$

1186:         & $=\; \emptyset $

1187:         & if $A\theta$ is false\\

1188: \end{tabular}\\

1189: 

1190: 

1191: Then the $\splitstep := \split\circ\step$ combines the two actions 

1192: and $\aux$ 

1193: repeats the $\splitstep$ until no more active constraints are left

1194: to remove.

1195: Reconsider now the formulas from items (\ref{item1}) and

1196:   (\ref{item2}) of Example \ref{exa:2a}.  We now have

1197: \begin{quote}$

1198: \p{\ES}{\varepsilon}\sem{y-1 = z-1 \A y = 1 \A z = 1} = $

1199: 

1200: $

1201: \p{y-1 = z-1}{\varepsilon}\sem{y = 1 \A z = 1} = $

1202: %\p{y-1 = z-1}{\C{y/{\bf 1}}}\sem{z = 1} = 

1203: $ \C{\p{\ES}{\C{y/{\bf 1}, z/{\bf 1}}}}$

1204: \end{quote}

1205: and

1206: \begin{quote}

1207: $

1208: \p{\ES}{\varepsilon}\sem{y < z \A y = 1 \A z = 2} = 

1209: \p{y < z}{\varepsilon}\sem{y = 1 \A z = 2} = $

1210: 

1211: $

1212: %\p{y < z}{\C{y/{\bf 1}}}\sem{z = 2} = 

1213: \C{\p{\ES}{\C{y/{\bf 1}, z/{\bf 2}}}}.$

1214: \end{quote}

1215: This shows the difference brought in by this

1216: $\infer$ procedure.

1217: However, in the case of the formula from item (\ref{item3}), we still have

1218: \[

1219: \p{\ES}{\varepsilon}

1220: \sem{\neg (x = 1) \A x = 0} = \C{\error}.

1221: \]

1222: 

1223: 

1224: 

1225: \paragraph{{\bf Equations as active and passive constraints}}

1226: \label{subsec:ac-pas}

1227: 

1228: In general, equations can be both active and passive constraints.  For

1229: example, linear equations over reals can be active and non-linear ones

1230: passive.  To model computation in their presence we choose as the

1231: underlying algebra the standard algebra for the language of arithmetic

1232: with the set of real numbers as the domain.

1233: The special states are the ones that just have equations

1234: in the constraint store.

1235: Next, we use a $\split$ procedure that regards the linear equations

1236: as active and the  non-linear ones as passive.

1237: Using standard arithmetic operations each linear equation can be

1238: rewritten into one of the following forms:\\

1239: 

1240: \begin{tabular}{ll}

1241: $\bullet$ & $0 = 0$, \\

1242: 

1243: $\bullet$ & $r = 0$, where $r$ is a non-zero real, and \\

1244: 

1245: $\bullet$ & $x = u$, where $x\in \var$ and $u$ a linear

1246: expression not containing $x$.  \\

1247: \end{tabular}\\

1248: 

1249: This leads to the following

1250: %case distinction in the recursive 

1251: definition of the propagation $\step$:

1252: \begin{quote}$

1253: \step  \p{{\csp_p,\emptyset}}{\theta} := \{\p{{\csp_p}}{\theta}\}

1254: $\end{quote}

1255: \begin{quote}$

1256: \step  \p{\csp_p,{\cal C}_a, s = t}{\theta}

1257:  :=

1258: \left\{

1259: \begin{array}{ll}

1260: \p{\csp_p,{\cal C}_a}{\theta} &  

1261:         \mbox{$s\theta = t\theta$ rewrites to $0 = 0$,} \\

1262: \ES                                      &    

1263:         \mbox{$s\theta = t\theta$ rewrites to $r = 0$,}\\

1264:                                          &    

1265:         \mbox{where $r$ is a non-zero real,} \\

1266: \p{\csp_p,{\cal C}_a}{\theta \C{x/u}} &  

1267:         \mbox{$s\theta = t\theta$ rewrites to $x = u$,} \\

1268: %\p{\csp_p,{\cal C}_a, s = t}{\theta} &  

1269: %       \mbox{$s\theta = t\theta$ is not a linear equation.} \\

1270: \end{array}

1271: \right.

1272: $\end{quote}

1273: The last clause models in effect the Gaussian elimination step, now in

1274: presence of linear and non-linear equations.

1275: 

1276: 

1277: \paragraph{{\bf Negative literals as passive constraints}}

1278: 

1279: \label{subsec:literals}

1280: 

1281: The $\infer$ methods introduced above allowed only atoms in the

1282: constraint store of special states, that is to say an occurrence of non-atomic

1283: formulas in the constraint store leads to an immediate error.  Let us

1284: extend the $\infer$ method to allow for negative literals in the 

1285: constraint store of special states. Now we can easily modify the 

1286: definitions from "Atoms as passive constraints":

1287: we regard states with finite sets of literals as special states

1288: and regard the literals that would evaluate to

1289: $\error$ as passive. Then the definition of the $\step$ is obtained

1290: by having a literal $L$ instead of an atom $A$.

1291: Now, in the case of 

1292: the formula from item (\ref{item3}) of Example \ref{exa:2a}

1293: we have

1294: \begin{quote}

1295: $

1296: \p{\ES}{\varepsilon}\sem{\neg (x = 1) \A x = 0} = 

1297: \p{\neg (x = 1)}{\varepsilon}\sem{x = 0} = 

1298: $

1299: 

1300: $\step \p{\neg (x = 1)}{\C{x/{\bf 0}}} = 

1301: \C{\p{\ES}{\C{x/{\bf 0}}}}.

1302: $

1303: \end{quote}

1304: 

1305: \paragraph{{\bf Equality and disequality constraints}}

1306: 

1307: We continue the previous example

1308: for the case of

1309: an arbitrary language of terms together

1310: with equality and disequality constraints.\footnote{We ignore

1311: the notational distinction between the disequation $s\neq t$ and the

1312: negation $\neg (s=t)$ for the moment.} 

1313: We adapt the definition by

1314: having as active constraints all equations as well as those

1315: disequations that are ground or of the form $t\theta\neq t\theta$.

1316: The $\split$ of $\tupel{\csp ; \theta}$ now produces 

1317: $\tupel{\csp_p,\csp_a ;\theta}$ with 

1318: $\csp_p \; =\; s_1\neq t_1,\ldots , s_n\neq t_n$, a list of all the 

1319: disequations $s_i\neq t_i\in\csp$ for which

1320: $(s_i\neq t_i)\theta$ is not ground and not of the form $t\neq t$. 

1321: The definition of the $\step$ then is:\\

1322: 

1323: \begin{tabular}{lll}

1324: $\step \tupel{\csp_p ;\theta}$

1325:         &  $= \; \verz{\tupel{\csp_p ;\theta}}$

1326:         & if no active constraints occur\\

1327: $\step \tupel{\csp_p,\csp_a, s=t ;\theta}$

1328:         & $=\; \verz{\tupel{\csp_p,\csp_a

1329:                  ;\theta\eta}}$

1330:         & if $\eta$ is an mgu of $s\theta ,\; t\theta$\\

1331: $\step \tupel{\csp_p,\csp_a, s=t ;\theta}$

1332:         & $=\;\emptyset$

1333:         & if $s\theta ,\; t\theta$ cannot be unified\\

1334: $\step \tupel{\csp_p,\csp_a, s\neq t ;\theta}$

1335:         & $=\;\verz{\tupel{\csp_p,\csp_a

1336:                  ;\theta}}$

1337:         & if $s\theta\neq t\theta$ is true\\

1338: $\step \tupel{\csp_p,\csp_a, s\neq t ;\theta}$

1339:         & $=\; \emptyset $

1340:         & if $s\theta \neq t\theta$ is false\\

1341: \end{tabular}\\

1342: 

1343: Then we get, for example

1344: 

1345: \begin{quote}

1346: $

1347: \p{\ES}{\varepsilon}\sem{f(x) \neq f(y) \A g(x,b) = g(a,y)} = $

1348: 

1349: $\step \p{ f(x) \neq f(y)}{\C{x/a, y/b}} = 

1350: \C{\p{\ES}{\C{x/a, y/b}}}$.

1351: \end{quote}

1352: 

1353: In general, if no $\error$ occurs, we can expect 

1354: $\tupel{\emptyset ,\; \epsilon}\sem{\phi}$

1355: to contain special states from which all active constraints are removed,

1356: i.e., states of the form 

1357: $\tupel{\csp ; \theta}$ where $\csp$ is a list of inequations $s\neq t$

1358: such that

1359: $s\theta \neq t\theta$ is passive. It follows from the

1360: independence of inequations of \cite{Col84} that over an infinite

1361: Herbrand Universe such a constraint store is consistent, i.e., has a grounding

1362: solution $\eta$. For such an $\eta$ we can then conclude: 

1363: $\models s_i\theta \neq t_i\theta$ 

1364: (for each $1\leq i\leq n$) and $\models \phi\theta\eta$.

1365: 

1366: The grounding solution $\eta$ can not be built up during the computation of 

1367: $\sem{\phi}$. This is clear from the example $x\neq y\; \wedge\; x=c$. If

1368: we make the choice $\verz{x/d ,x/c}$ as a grounding solution for 

1369: $x\neq y$ too soon,

1370: we are no longer able to deal with $x=c$ later on. Hence we can benefit

1371: from the independence of inequations only after the computation of 

1372: $\sem{ x\neq y\; \wedge\; x=c}$ has been completed.

1373: 

1374: \paragraph{{\bf Existential formulas as passive constraints}}

1375: 

1376: At this point only literals are allowed in the constraint store.

1377: We can easily extend the current store management to one

1378: in which also existential formulas are allowed in the constraint store.

1379: To this end we need some quantifier elimination procedure

1380: $\elim$ that is able to deal with at least

1381: some form of existential quantification. 

1382: Then we can have $\step := \elim$.

1383: 

1384: \paragraph{{\bf Arbitrary formulas as passive constraints}}

1385: 

1386: The previous constraint store management can be extended by allowing 

1387: arbitrary formulas in the constraint store. 

1388: This makes sense as soon as we have some decision procedure $\solve$

1389: that is able to deal with at least some type of negative formulas.

1390: Then we can have $\step := \solve$.

1391: 

1392: \section{Rationale and Related Work}

1393: 

1394: \label{sec:related}

1395: 

1396: As clarified in Section \ref{sec:apt} the soundness result established

1397: here generalizes the appropriate result provided in \cite{Apt00}. The

1398: drawback of this semantics was that it yielded error as answer for

1399: several clearly satisfiable formulas, like the ones considered in the

1400: introduction.

1401: 

1402: Our interest in a semantics that models constraint management in a

1403: sound way stems from our attempts to add constraints to the

1404: programming language \almazero{} of Apt et al.  \cite{ABPS98a}.

1405: \almazero{} extends imperative programming by features that support

1406: declarative programming. This language allows us to interpret the

1407: formulas of first-order logic (without universal quantification) as

1408: executable programs. In Apt and Schaerf \cite{AS99a} we proposed to

1409: extend \almazero{} by constraints but found that this led to situations

1410: in which the customary interpretation of the conditionals by means of the

1411: implication is unsound.

1412: 

1413: Using the above considerations we can provide a simple sound

1414: interpretation of the \texttt{IF B THEN S ELSE T END} statement.

1415: Namely, it is sufficient to interpret it in logic as $(B \A S) \Or

1416: (\neg B \A T)$, written in the \almazero{} syntax as \texttt{EITHER B;

1417:   S ORELSE (NOT B); T END}.  This interpretation requires that

1418: negative literals, here \texttt{NOT B}, are used as passive

1419: constraints. On the implementation level backtracking is then needed

1420: but the above interpretation can be reduced to the customary

1421: implementation of \texttt{IF B THEN S ELSE T END} if the condition

1422: \texttt{B} evaluates to {\bf true} or {\bf false} irrespectively of

1423: the constraint store.

1424: 

1425: As already mentioned in the introduction the modelling of the

1426: constraint store maintenance by means of an abstract $\infer$

1427: mechanism is due to Jaffar and Maher \cite{jaffar-survey}. In their

1428: framework the computation mechanism of constraint logic programming is

1429: modeled, so local variables (modeled by existential variables) and

1430: negation are absent but recursion is considered. Additionally, only

1431: conjunctions of atomic formulas are allowed as constraints.

1432: 

1433: In \cite{JMMS98} several semantics for constraint logic programming

1434: are compared. In this paper a mapping {\it solv} is used that allows for

1435: inconsistency checks during the computation. {\it solv} can vary with

1436: the intended application, just like our {\it infer} parameter, but,

1437: unlike {\it infer}, it cannot model arbitrary constraint propagation

1438: steps. In fact, in \cite{JMMS98} the constraint propagation steps take

1439: place only at the end of each the computation.

1440: 

1441: An alternative approach to model the essentials of constraint

1442: programming is provided by the concurrent constraint programming (ccp)

1443: approach pioneered by Saraswat \cite{saraswat-ccp-93} and Saraswat,

1444: Rinard and Panangaden \cite{saraswat-semantic}. In this scheme the programs can

1445: also be considered as formulas with the difference that the atomic

1446: \textbf{tell} and \textbf{ask} operations are present and that the

1447: parallel composition connective is present.  The idea captured by this

1448: model is that the processes interact by means of a constraint system

1449: using the \textbf{tell} and \textbf{ask} operations.  The constraint

1450: system is a set of constraints equipped with the entailment operation.

1451: 

1452: The ccp programs can be written in a logical way by dropping the

1453: ``\textbf{tell}'' context around a constraint and by interpreting the

1454: \textbf{ask}($c$) statement as the implication $c \ra$.  However, in

1455: spite of this logical view of ccp programs it is not clear how to

1456: interpret them as first-order formulas with the customary semantics.

1457: In Fages, Ruet and Soliman \cite{FRS01} a logical semantics of ccp

1458: programs is given by interpreting them in intuitionistic linear logic.

1459: Both the denotational semantics for this language and the correctness

1460: (in the assertional style) of ccp programs were considered in a

1461: number of papers, see, e.g., de Boer et al.  \cite{dBdPP95} and de Boer

1462: et al. \cite{dBGMP97}.  How to add to this framework in a

1463:   sound way negation was studied in Palamidessi, de Boer and Pierro

1464:   \cite{dBPdP97}.  By the nature of this approach the study of the

1465:   constraint store management captured here by means of the $\infer$

1466:   mechanism is absent in this framework.

1467: 

1468: 

1469: \section*{Acknowledgement}

1470: We thank Catuscia Palamidessi for helpful discussion on the subject 

1471: of ccp programs.

1472: 

1473: 

1474: \begin{thebibliography}{10}

1475: 

1476: \bibitem{AS99a}

1477: K.~R. Apt and A.~Schaerf.

1478: \newblock The {Alma} project, or how first-order logic can help us in

1479:   imperative programming.

1480: \newblock In E.-R. Olderog and B.~Steffen, editors, {\em Correct System

1481:   Design}, Lecture Notes in Computer Science 1710, pages 89--113, 1999.

1482: 

1483: \bibitem{Apt00}

1484: K.R. Apt.

1485: \newblock A denotational semantics for first-order logic.

1486: \newblock In {\em Proc. of the computational logic conference (CL2000)},

1487:   Lecture Notes in Artificial Intelligence 1861, pages 53--69. Springer Verlag,

1488:   2000.

1489: 

1490: \bibitem{AB99}

1491: K.R. Apt and M.A. Bezem.

1492: \newblock Formulas as programs.

1493: \newblock In K.R. Apt, V.W. Marek, M.~Truszcy\'nski, and D.S. Warren, editors,

1494:   {\em The Logic Programming Paradigm: A 25 Year Perspective}, pages 75--107,

1495:   1999.

1496: 

1497: \bibitem{ABPS98a}

1498: K.R. Apt, J.~Brunekreef, V.~Partington, and A.~Schaerf.

1499: \newblock {\sf Alma-0}: An imperative language that supports declarative

1500:   programming.

1501: \newblock {\em ACM Toplas}, 20(5):1014--1066, 1998.

1502: 

1503: \bibitem{dBGMP97}

1504: F.S.~De Boer, M.~Gabbrielli, E.~Marchiori, and C.~Palamidessi.

1505: \newblock Proving concurrent constraint programs correct.

1506: \newblock In {\em ACM Transactions on Programming Languages and Systems},

1507:   volume 19(5), pages 685--725, 1997.

1508: 

1509: \bibitem{Col84}

1510: A.~Colmerauer.

1511: \newblock Equations and inequations on finite and infinite trees.

1512: \newblock In John Lloyd, editor, {\em Proc. of International Conference of

1513:   Fifth Generation Computer Systems (FGCS'84)}, pages 85--99. OHMSHA Ltd. Tokyo

1514:   and North-Holland, 1984.

1515: 

1516: \bibitem{dBdPP95}

1517: F.S. de~Boer, A.~Di Pierro, and C.~Palamidessi.

1518: \newblock Nondeterminism and infinite computations in constraint programming.

1519: \newblock {\em Theoretical Computer Science}, 151(1):37--78, 1995.

1520: 

1521: \bibitem{FRS01}

1522: F.~Fages, P.~Ruet, and S.~Soliman.

1523: \newblock Linear concurrent constraint programming: Operational and phase

1524:   semantics.

1525: \newblock {\em Information and Computation}, 165(1):14--41, 2001.

1526: 

1527: \bibitem{jaffar-survey}

1528: J.~Jaffar and J.M. Maher.

1529: \newblock Constraint logic programming: a survey.

1530: \newblock {\em Journal of Logic Programming}, 19/20, 1994.

1531: 

1532: \bibitem{JMMS98}

1533: J.~Jaffar, J.M. Maher, K.~Marriott, and P.~Stuckey.

1534: \newblock The semantics of constraint logic programs.

1535: \newblock {\em Journal of Logic Programming}, 37(1):1--46, 1998.

1536: 

1537: \bibitem{LT84}

1538: J.W. Lloyd and R.W. Topor.

1539: \newblock Making {Prolog} more expressive.

1540: \newblock {\em Journal of Logic Programming}, 1:225--240, 1984.

1541: 

1542: \bibitem{dBPdP97}

1543: C.~Palamidessi, F.S. de~Boer, and A.~Di Pierro.

1544: \newblock An algebraic perspective of constraint logic programming.

1545: \newblock {\em Journal of Logic and Computation}, 7, 1997.

1546: 

1547: \bibitem{saraswat-semantic}

1548: V.~A. Saraswat, M.~Rinard, and P.~Panangaden.

1549: \newblock Semantic foundations of concurrent constraint programming.

1550: \newblock In {\em Conference Record of the Eighteenth Annual {ACM} Symposium on

1551:   Principles of Programming Languages}, pages 333--352, Orlando, Florida, 1991.

1552: 

1553: \bibitem{saraswat-ccp-93}

1554: Vijay Saraswat.

1555: \newblock {\em Concurrent Constraint Programming}.

1556: \newblock MIT Press, 1993.

1557: 

1558: \end{thebibliography}

1559: 

1560: 

1561: \section*{\bf Appendix: the proofs}

1562: \label{appie}

1563: 

1564: In this appendix we give proof details of the Soundness Theorem

1565: and Preservation/Persistence Lemma. 

1566: Both proofs are by 

1567: %the proof of soundness and persistence are 

1568: simultaneous inductions on the structure of the formula. 

1569: %Soundness is proved by induction on the complexity 

1570: %of the formula.

1571: %

1572: %The proof of the lemma also is a 

1573: %simultaneous induction, on the complexity of $\phi_2$.

1574: We focus on the existential quantification cases, which are the most subtle.

1575: We use the notation  $\models_{\cal J}\phi[\overline{a}]$

1576: to indicate the assignment of values $\overline{a}$ to (at least) 

1577: the free variables in $\phi$. In the case of the lemma it will be convenient

1578: to standardize this as follows: we are concerned with $\csp\theta$ and

1579: $\phi_i\theta$ (for $i=1,2$) and denote the values for the

1580: free variables shared by the $\phi_i\theta$ by $\overline{d}$. Then we use  

1581: the values

1582: $\overline{c}$ for the remaining free variables in $\phi_1\theta$ and 

1583: $\overline{e}$

1584: for the remaining free variables in $\phi_2\theta$. Finally, we denote the 

1585: values of the remaining free variables in $\csp\theta$ by $\overline{b}$.

1586: So, we will mostly use blocks of the form

1587: $[\overline{b},\overline{c},\overline{d}, \overline{e}]$.\\

1588: 

1589: \noindent{\bf Proof of Preservation/Persistence Lemma 1}:

1590: 

1591: \noindent{$\circ$ \bf{atoms}}: 

1592: In the atomic case $\phi_2 = A$ for some atom $A$ and 

1593: $\tupel{\csp '' ;\theta ''}\in\infer \tupel{\csp ,{A} ;\theta}$.

1594: Straightforward application of property (1) does the trick.

1595: 

1596: %\begin{enumerate}

1597: %\item We know that $\tupel{\csp ;\theta}\models_{\cal J}\phi_1$.

1598: %

1599: %So also 

1600: %$\tupel{\csp ,{A} ;\theta}\models_{\cal J}\phi_1$.

1601: %

1602: %By property (1) this gives

1603: %$\tupel{\csp '' ;\theta ''}\models_{\cal J}\phi_1$,

1604: %

1605: %as required.

1606: %\item

1607: %The assumption gives values 

1608: %$[\overline{b},\overline{c},\overline{d},\overline{e}]$ such that

1609: %

1610: %$\models_{\cal J} (\csp ,\; (\phi_1\wedge A))\theta

1611: %[\overline{b},\overline{c},\overline{d},\overline{e}]$. 

1612: %

1613: %So 

1614: %$\models_{\cal J} (\csp ,\; {A} ,\; \phi_1)\theta

1615: %[\overline{b},\overline{c},\overline{d},\overline{e}]$. 

1616: %

1617: %Now property (1) ensures that there are 

1618: %$[\overline{b'},\overline{c'},\overline{d'},\overline{e'}]$ such that

1619: %

1620: %$\models_{\cal J} (\csp '' ,\; \phi_1)\theta''

1621: %[\overline{b'},\overline{c'},\overline{d'},\overline{e'}]$. 

1622: %\end{enumerate}

1623: 

1624: \noindent{$\circ$ \bf{disjunction}}:

1625: In this case $\phi_2 = (\psi_1\vee\psi_2)$ and $\tupel{\csp '' ;\theta ''}\in

1626: \tupel{\csp ;\theta}\mysem{\psi_i}$ for some $i=1,2$. 

1627: In this situation the inductive hypotheses apply straightforwardly.

1628: 

1629: %\begin{enumerate}

1630: %\item By induction hypothesis (for the appropriate $i$) 

1631: %$\tupel{\csp '';\theta ''}\models_{\cal J}\phi_1$,

1632: %

1633: %as required. 

1634: %\item 

1635: %By assumption

1636: %$\models_{\cal J} (\csp\theta ,(\phi_1\wedge (\psi_1\vee\psi_2 ))\theta)

1637: %[\overline{b},\overline{c},\overline{d},\overline{e}]$.

1638: %

1639: %Hence

1640: %$\models_{\cal J} (\csp\theta ,(\phi_1\wedge \psi_i)\theta)

1641: %[\overline{b_i},\overline{c_i},\overline{d_i},\overline{e_i}]$.

1642: %

1643: %where $\overline{b_i},\overline{c_i},\overline{d_i},\overline{e_i}$ 

1644: %are obtained by reshuffling

1645: %$\overline{b},\overline{c},\overline{d},\overline{e}$ appropriately.

1646: %

1647: %Apply the induction hypothesis to get

1648: %

1649: %$\models_{\cal J} (\csp ''\theta '' ,(\phi_1\wedge \psi_i)\theta '')

1650: %[\overline{b_i ''},\overline{c_i ''},\overline{d_i ''},\overline{e_i ''}]$.

1651: %

1652: %From this conclude that

1653: %$\models_{\cal J}(\csp ''\theta '' ,(\phi_1\wedge (\psi_1\vee\psi_2))\theta '')

1654: %[\overline{b ''},\overline{c ''},\overline{d ''},\overline{e ''}]$

1655: %

1656: %for any completion 

1657: %$[\overline{b ''},\overline{c ''},\overline{d ''},\overline{e ''}]$

1658: %of

1659: %$[\overline{b_i ''},\overline{c_i ''},\overline{d_i ''},\overline{e_i ''}]$.

1660: %\end{enumerate}

1661: 

1662: \noindent{$\circ$ \bf{conjunction}}:

1663: In this case $\phi_2=(\psi_1\wedge\psi_2)$ and $\tupel{\csp '';\theta ''}\in

1664: \tupel{\csp ';\theta '}\mysem{\psi_2}$ for some 

1665: 

1666: \noindent$\tupel{\csp ';\theta '}\in \tupel{\csp ;\theta}\mysem{\psi_1}$. 

1667: Now two applications of the inductive hypothesis are required.

1668: For preservation of validity this is straightforward. For preservation

1669: of consistency it works as follows:

1670: %\begin{enumerate}

1671: %\item 

1672: %By induction hypothesis (for $\phi_1$ and $\psi_1$)

1673: %$\tupel{\csp ';\theta '}\models_{\cal J}\phi_1$.

1674: %

1675: %By a second application of the induction hypothesis

1676: %(to $\phi_1$ and $\psi_2$)

1677: %$\tupel{\csp '';\theta ''}\models_{\cal J}\phi_1$.

1678: %\item 

1679: by assumption

1680: $\models_{\cal J} (\csp\theta ,(\phi_1\wedge (\psi_1\wedge\psi_2 ))\theta )

1681: [\overline{b},\overline{c},\overline{d},\overline{e}]$.

1682: So,

1683: $\models_{\cal J} (\csp\theta ,(\phi_1\wedge \psi_1)\theta )

1684: [\overline{b},\overline{c_1},\overline{d_1},\overline{e_1}]$,

1685: restricting the $\overline{d}$ and $\overline{e}$ to the relevant variables

1686: and moving some of the $\overline{d}$ values to $\overline{c_1}$.

1687: By induction hypothesis we get

1688: $\models_{\cal J} (\csp '\theta ',(\phi_1\wedge \psi_1)\theta ')

1689: [\overline{b_1'},\overline{c_1'},\overline{d_1'},\overline{e_1'}]$.

1690: Next the induction hypothesis (for $\phi_1\wedge\psi_1$ and $\psi_2$)

1691: provides

1692: $\models_{\cal J} (\csp ''\theta '',

1693: ((\phi_1\wedge \psi_1)\wedge\psi_2)\theta '')

1694: [\overline{b''},\overline{c''},\overline{d''},\overline{e''}]$,

1695: as required.

1696: %\end{enumerate}

1697: 

1698: \noindent{$\circ$ \bf{negation}}:

1699: In this case $\phi_2=\neg \psi$. We have to distinguish cases

1700: 

1701: \begin{itemize}

1702: \item $\phi_2$ is 'true': $\tupel{\csp '';\theta ''}\in

1703: \infer \tupel{\csp ;\theta}$ (and 

1704: $\mycons^+ (\tupel{\csp ;\theta}\mysem{\psi})=\emptyset$. )

1705: Now property (1) gives the results.

1706: %\begin{enumerate}

1707: %\item $\tupel{\csp ;\theta}\models_{\cal J}\phi_1$ is given. Hence property (1)

1708: %gives us: $\tupel{\csp '' ;\theta ''}\models_{\cal J}\phi_1$.

1709: %\item $\models_{\cal J} (\csp\theta ,\; (\phi_1\wedge\neg\psi)\theta )

1710: %[\overline{b},\overline{c},\overline{d},\overline{e}]$ is assumed.

1711: %Hence the required assignment

1712: %$\models_{\cal J} (\csp ''\theta '',\; (\phi_1\wedge\neg\psi)\theta '')

1713: %[\overline{b ''},\overline{c ''},\overline{d ''},\overline{e ''}]$ 

1714: %is available by property (1).

1715: %\end{enumerate}

1716: \item $\phi_2$ is 'false': in this case $\tupel{\csp ;

1717: \theta}\mysem{\phi_2}=\emptyset$ and both (i) and (ii) are void.

1718: \item 'otherwise': we get $\tupel{\csp '';\theta ''}\in 

1719: \infer\tupel{\csp ,{\neg\psi};\theta}$.

1720: The results follow from first order logic and property (1).

1721: %\begin{enumerate}

1722: %\item 

1723: %By assumption $\tupel{\csp ;\theta}\models_{\cal J}\phi_1$.

1724: %From this first order logic gives

1725: %$\tupel{\csp ,{\neg\psi} ;\theta}\models_{\cal J} \phi_1$.

1726: %Now (1) ensures that

1727: %$\tupel{\csp '' ;\theta ''}\models_{\cal J} \phi_1$.

1728: %\item 

1729: %By assumption

1730: %$\models_{\cal J} (\csp\theta ,(\phi_1\wedge \neg\psi )\theta )

1731: %[\overline{b},\overline{c},\overline{d},\overline{e}]$.

1732: %We duplicate $\neg\psi$ and shuffle the values in the assignment to get

1733: %$\models_{\cal J} ((\csp ,{\neg\psi})\theta 

1734: %,(\phi_1\wedge \neg\psi ))\theta )

1735: %[\overline{b '},\overline{c '},\overline{d '},\overline{e '}]$.

1736: %From this (1) gives us the required result.

1737: %\end{enumerate}

1738: \end{itemize}

1739: 

1740: % new version, anticipating Apt:London

1741: 

1742: \noindent{$\circ$ \bf{existential quantification}}:

1743: Now $\phi_2=\exists x\; \psi$ for some $x$, $\psi$. So, consider

1744: $\infer \;\mbox{\sc drop}_u\tupel{\csp ';\eta}$

1745: for some consistent 

1746: $\tupel{\csp ';\eta}\in\tupel{\csp ;\theta}\mysem{\psi\verz{x/u}}$ ($u$ fresh).

1747: By property (1) it suffices to consider

1748: %\begin{quote}

1749: $\mbox{\sc drop}_u\tupel{\csp ';\eta}=$

1750: $\langle (\csp '-\csp '(u,{\bf y})) ,\;\exists u\; (u=u\eta\wedge {\bf y}=

1751: {\bf y}\eta \wedge \csp '(u,{\bf y})) 

1752: ;\;  \mbox{\it DROP}_{u}(\eta ) \rangle$.

1753: %\end{quote}

1754: We call ${\it DROP}_{u,{\bf y}}(\eta )=\theta ''$.

1755: \begin{enumerate}

1756: \item By assumption $\tupel{\csp ;\theta}\models_{\cal J}\phi_1$.

1757: By induction hypothesis 

1758: $\tupel{\csp ' ;\eta}\models_{\cal J} \phi_1$.

1759: From this 

1760: $(u=u\eta\wedge \csp ')\mbox{\it DROP}_u(\eta )\models_{\cal J} (u=u\eta\wedge

1761: \phi_1)\mbox{\it DROP}_u(\eta)$.

1762: So,

1763: $(u=u\eta\wedge \csp ')\mbox{\it DROP}_u(\eta )\models_{\cal J} 

1764: \phi_1\mbox{\it DROP}_u(\eta)$.

1765: Repeating this for the ${\bf y}$, we get

1766: $(u=u\eta\wedge{\bf y}={\bf y}\eta\wedge \csp ')\theta '' \models_{\cal J} 

1767: \phi_1\theta ''$.

1768: By (2) we may assume that this holds for some $u$ that does 

1769: not occur in $\phi_1\theta ''$.

1770: Hence the implicit overall universal quantification over $u$ can be

1771: replaced by an existential quantification over $u$ on the left hand side of

1772: the sequent. 

1773: %\footnote{In other words: we use that 

1774: %if $x$ is not free in $\chi$, then

1775: %$\models \forall x\; (\psi\rightarrow\chi ) \leftrightarrow

1776: %((\exists x\;\psi)\rightarrow \chi )$.}

1777: This gives

1778: \begin{quote}

1779: $((\csp '-\csp '(u,{\bf y}))\; \wedge\; 

1780: \exists u\; (u=u\eta\wedge{\bf y}={\bf y}\eta\wedge 

1781: \csp '(u,{\bf y})))\theta '' \models_{\cal J} 

1782: \phi_1\theta ''$.

1783: \end{quote}

1784: Now we can safely re-instantiate the values of the variables in

1785: {\bf y} to obtain the same for 

1786: ${\it DROP}_u(\eta)\; =\; \theta ''\cup\verz{{\bf y}/{\bf y}\eta}$

1787: \begin{quote}

1788: $((\csp ' -\csp '(u,{\bf y}))\; \wedge\; 

1789: \exists u\; (u=u\eta\wedge{\bf y}={\bf y}\eta\wedge 

1790: \csp '(u,{\bf y})))\mbox{\it DROP}_u(\eta ) \models_{\cal J} 

1791: \phi_1\mbox{\it DROP}_u(\eta )$.

1792: \end{quote}

1793: \item

1794: The assumption gives

1795: $\models_{\cal J}(\csp\theta,\; (\phi_1\wedge\exists x\;\psi))\theta )

1796: [\overline{b},\overline{c},\overline{d},\overline{e}]$.

1797: From the induction hypothesis we obtain

1798: $\models_{\cal J}(\csp '\eta,\; (\phi_1\;\wedge\;\psi\verz{x/u})\eta )

1799: [\overline{b'},\overline{c'},\overline{d'},\overline{e'},f]$

1800: where $f$ is the value of $u$. From this we conclude

1801: $\models_{\cal J}(\csp '\eta,\; (\phi_1\;\wedge\;\exists x\; \psi)\eta )

1802: [\overline{b'},\overline{c'},\overline{d'},\overline{e'},f]$.

1803: So, we can be sure that suitable values for all the variables in $\csp '$ and

1804: $(\phi_1\wedge\exists x\;\psi )$ are available, if we use the values in

1805: the block 

1806: $[\overline{b'},\overline{c'},\overline{d'},\overline{e'},f]$

1807: and the substitution $\eta$ as a middle man.

1808: But then we can also assign these values directly to the variable 

1809: $u$, eliminating the middle man $\eta$. This way we get 

1810: values 

1811: $[\overline{b''},\overline{c''},\overline{d''},\overline{e''}]$

1812: such that

1813: $\models_{\cal J}

1814: (((\csp '-\csp '(u,{\bf y}))\wedge 

1815: u=u\eta\wedge {\bf y}={\bf y}\eta\wedge \csp 

1816: '(u,{\bf y}))\mbox{\it DROP}_u(\eta ),$

1817: \hfill{$(\phi_1\wedge\exists x\;\psi)\mbox{\it DROP}_u (\eta ))

1818: [\overline{b''},\overline{c''},\overline{d''},\overline{e''}]$.}

1819: From this the consistency of $\mbox{\sc drop}_u \tupel{\csp ';\eta}$ and

1820: $(\phi_1\wedge\exists x\;\psi )\mbox{\it DROP}_u(\eta )$ is clear.\hfill{$\Box$}

1821: \end{enumerate}

1822: 

1823: %EOP: end of preservation

1824: 

1825: \noindent{\bf Proof of Soundness Theorem 1}:

1826: 

1827: \noindent{$\circ$ \bf{atoms}}:

1828: In case $\phi$ is an atomic formula $A$, $\tupel{\csp ;\theta}\mysem{\phi}

1829: =\infer\;\tupel{\csp ,{A} ;\theta}$.  

1830: Now straightforward applications of property (1) and (3) give the result.

1831: %\begin{enumerate}

1832: %\item Consider $\tupel{\csp ';\theta '}\in 

1833: %\infer\tupel{\csp ,{A} ;\theta}$. Now $\tupel{\csp ,{A} ;\theta}

1834: %\models_{\cal J} A$. So, by (1) also $\tupel{\csp ' ;\theta '}\models_{\cal J}

1835: %A$.

1836: %\item 

1837: %Suppose $\mycons^+(\infer\tupel{\csp ,{A} ;\theta})=\emptyset$. 

1838: %This can mean 

1839: %$\infer\tupel{\csp ,{A} ;\theta}=\emptyset$. In this case (3) implies

1840: %that 

1841: %

1842: %$\tupel{\csp ,{A} ;\theta}\models_{\cal J}\bot$. 

1843: %

1844: %Else we find some inconsistent 

1845: %$\tupel{\csp ';\theta '}\in\infer\tupel{\csp ,{A} ;\theta}$. Now 

1846: %(1) implies

1847: %that $\tupel{\csp ,{A} ;\theta}\models_{\cal J}\bot$. 

1848: %

1849: %Hence in both cases

1850: %$\tupel{\csp ;\theta}\models_{\cal J}\neg A$, as required.

1851: %\end{enumerate}

1852: 

1853: \noindent{$\circ$ \bf{disjunction}}:

1854: In case $\phi$ is a disjunction,  $\phi_1\vee\phi_2$ say, 

1855: $\tupel{\csp ;\theta}\mysem{\phi} = 

1856: \tupel{\csp ;\theta}\mysem{\phi_1}\cup\tupel{\csp ;\theta}\mysem{\phi_2}$.

1857: The induction hypotheses apply immediately.

1858: %

1859: %\begin{enumerate}

1860: %\item 

1861: %Let $\tupel{\csp ';\theta '}\in\tupel{\csp ;\theta}\mysem{\phi_1\vee\phi_2}$

1862: %be given. Then  

1863: %$\tupel{\csp ';\theta '}\in\tupel{\csp ;\theta}\mysem{\phi_i}$ for

1864: %one of $i=1,2$. Hence the induction hypothesis gives

1865: %$\tupel{\csp ';\theta '}\models_{\cal J}\phi_i$, from which

1866: %$\tupel{\csp ';\theta '}\models_{\cal J}(\phi_1\vee\phi_2) $ follows readily.

1867: %\item Let 

1868: %$\tupel{\csp ;\theta}\mysem{\phi_1\vee\phi_2}$

1869: %only contain inconsistent states. This means that

1870: %$\mycons^+ (\tupel{\csp ;\theta}\mysem{\phi_i})=\emptyset$.

1871: %% only contains inconsistent states

1872: %for both of $i=1,2$. By induction hypothesis we get

1873: %$\tupel{\csp ;\theta}\models_{\cal J}\neg\phi_i$ for both $i=1,2$.

1874: %Hence

1875: %$\tupel{\csp ;\theta}\models_{\cal J}\neg (\phi_1\vee\phi_2)$, as required. 

1876: %\end{enumerate}

1877: 

1878: \noindent{$\circ$ \bf{conjunction}}:

1879: In case $\phi$ is a conjunction, $\phi_1\wedge\phi_2$ say, 

1880: $\tupel{\csp ''; \theta ''}\in\tupel{\csp ;\theta}\mysem{\phi} $ iff

1881: $\tupel{\csp ''; \theta ''}\in\tupel{\csp ';\theta '}\mysem{\phi_2} $  for

1882: some

1883: $\tupel{\csp '; \theta '}\in\tupel{\csp ;\theta }\mysem{\phi_1} $.

1884: Part 1. of the theorem is a straightforward consequence of the 

1885: induction hypothesis and persistence. For part 2 we add some details.

1886: %\begin{enumerate}

1887: %\item The induction hypothesis gives

1888: %$\tupel{\csp '' ;\theta ''}\models_{\cal J}\phi_2$

1889: %and

1890: %$\tupel{\csp ' ;\theta '}\models_{\cal J}\phi_1$. 

1891: %By persistence (i) we may conclude

1892: %$\tupel{\csp '' ;\theta ''}\models_{\cal J}\phi_1$. 

1893: %So, first order logic now gives

1894: %$\tupel{\csp '' ;\theta ''}\models_{\cal J}(\phi_1\wedge\phi_2)$. 

1895: %\item 

1896: We have: if $\tupel{\csp ';\theta '}\in\tupel{\csp ;\theta}\mysem{\phi_1}$ 

1897: is consistent, 

1898: then $\tupel{\csp ';\theta '}\mysem{\phi_2}$ only contains inconsistent states.

1899: From this we may conclude by induction hypothesis that for each 

1900: $\tupel{\csp ';\theta '}\in\mycons (\tupel{\csp ;\theta}\mysem{\phi_1})$

1901: \begin{equation}

1902:   \label{eq:otimes}

1903: \tupel{\csp ' ;\theta '}\models_{\cal J}\neg \phi_2.  

1904: \end{equation}

1905: Now assume that for some\footnote{Notation for assignment of values as

1906: in the lemma.} $[\overline{b},\overline{c},\overline{d},

1907: \overline{e}]$,

1908: $\models_{\cal J} (\csp\theta\wedge\phi_1\theta\wedge\phi_2\theta)[b,c,d,e]$

1909: and that we have a 

1910: $\tupel{\csp ';\theta '}\in\mycons (\tupel{\csp ;\theta}\mysem{\phi_1})$.

1911: Then persistence (2) tells us that the consistency is preserved, i.e.,

1912: there are 

1913: $[\overline{b'},\overline{c'},\overline{d'},\overline{e'}]$ 

1914: such that

1915: $\models_{\cal J}

1916: (\csp '\theta '\wedge\phi_1\theta '\wedge\phi_2\theta ')

1917: [\overline{b'},\overline{c'},\overline{d'},\overline{e'}]$. 

1918: But this contradicts the statement (\ref{eq:otimes}). So, for no 

1919: $[\overline{b},\overline{c},\overline{d},\overline{e}]$, 

1920: $\models_{\cal J} (\csp\theta\wedge\phi_1\theta\wedge\phi_2\theta)

1921: [\overline{b},\overline{c},\overline{d},\overline{e}]$, 

1922: which is as required.

1923: %\end{enumerate}

1924: 

1925: \noindent{$\circ$ \bf{negation}}:

1926: In case of a negation $\neg\phi$, there are three situations to consider

1927: \begin{itemize}

1928: \item $\tupel{\csp ';\theta '}\in\infer\tupel{\csp ;\theta}$ and 

1929: $\mycons^+ (\tupel{\csp ;\theta}\mysem{\phi})=\emptyset$.

1930: %only contains inconsistent states. 

1931: Now case (1) of the theorem follows from the induction hypothesis for 

1932: case (2) and equivalence condition (1). Case (2) follows from 

1933: conditions (1) and (3).

1934: %\begin{enumerate}

1935: %\item By induction hypothesis (for (2))

1936: %$\tupel{\csp ;\theta}\models_{\cal J}\neg\phi$. Hence, by equivalence (1):

1937: %$\tupel{\csp ';\theta '}\models_{\cal J}\neg\phi$. 

1938: %\item Assume that 

1939: %%every state in 

1940: %$\mycons^+ (\infer\tupel{\csp ;\theta})=\emptyset$.

1941: %% is inconsistent.

1942: %Then (3) and (1) ensure that already

1943: %$\tupel{\csp ;\theta}\models_{\cal J}\bot$.

1944: %But then

1945: %$\tupel{\csp ;\theta}\models_{\cal J}\neg\phi$.

1946: %\end{enumerate}

1947: \item $\tupel{\csp ;\theta}\mysem{\neg\phi}=\emptyset$ and there is some

1948: $\tupel{\csp ';\theta '}\in\mycons (\tupel{\csp ;\theta}\mysem{\phi})$,

1949: which is equivalent  to $\tupel{\csp ;\theta}$. 

1950: Now case (1) is satisfied trivially and case (2) follows from the induction

1951: hypothesis for (1) and condition (1) on $\infer$.

1952: %\begin{enumerate}

1953: %\item is satisfied trivially. 

1954: %\item Consider the relevant $\tupel{\csp ';\theta '}$. By induction

1955: %hypothesis (for (i)), we get $\tupel{\csp ' ;\theta '}\models_{\cal J}\phi$.

1956: %Hence equivalence (1) gives 

1957: %$\tupel{\csp ;\theta}\models_{\cal J}\phi$.

1958: %From this first order logic gives

1959: %$\tupel{\csp ;\theta}\models_{\cal J}\neg\neg\phi$, as required.

1960: %\end{enumerate}

1961: \item $\tupel{\csp ;\theta}\mysem{\neg\phi}=

1962: \infer\tupel{\csp ,{\neg\phi};\theta}$.

1963: Let $\tupel{\csp ';\theta '}\in

1964: \infer\tupel{\csp ,{\neg\phi};\theta}$ be given.

1965: Now case (1) follows from condition (1) and case two relies on 

1966: conditions (1) and (3).

1967: %\begin{enumerate}

1968: %\item Clearly, $\tupel{\csp ,\neg\phi ;\theta}\models_{\cal J}\neg\phi\theta$.

1969: %Hence, by (1), $\tupel{\csp ';\theta '}\models \neg\phi$.

1970: %\item In case 

1971: %%all $\tupel{\csp ';\theta '}\in

1972: %$\mycons^+ (\infer \tupel{\csp ,{\neg\phi};\theta}) =\emptyset$, 

1973: %%are inconsistent, 

1974: %(1) and (3) give that $\tupel{\csp ,\neg\phi ;\theta}\models_{\cal J}\bot$.

1975: %So, $\tupel{\csp ;\theta}\models_{\cal J}\neg\neg\phi$, as required.

1976: %\end{enumerate}

1977: \end{itemize}

1978: 

1979: 

1980: \noindent{$\circ$ \bf{existential quantification}}:

1981: In case of an existential quantification $\exists x\;\phi$, we have to consider

1982: %\begin{quote}

1983: $\tupel{\csp '';\theta ''}\in 

1984: \infer\;\mbox{\sc drop}_u\tupel{\csp ';\eta}$,

1985: %\end{quote}

1986: \noindent for $\tupel{\csp ';\eta}\in \mycons (

1987: \tupel{\csp ;\theta}\mysem{\phi\verz{x/u}})$ (some fresh $u$). 

1988: Call $\mbox{\it DROP}_{u,{\bf y}}(\eta )=\theta '$.

1989: Below we use a crucial fact about first order logic:

1990: if $x$ is not free in $\chi$, then

1991: $\models\; \forall x\; (\psi\rightarrow\chi ) \;\leftrightarrow\;

1992: ((\exists x\;\psi)\rightarrow \chi )$. 

1993: 

1994: \begin{enumerate}

1995: \item 

1996: By induction hypothesis $\tupel{\csp ';\eta}\models_{\cal J}\phi\verz{x/u}$.

1997: By first order logic

1998: 

1999: $(\csp '-\csp'(u,{\bf y}))\eta\models_{\cal J}(\csp '(u,{\bf y})\;\rightarrow\;

2000: \phi\verz{x/u})\eta$.

2001: From this we conclude that

2002: $(\csp '-\csp'(u,{\bf y}))\eta\models_{\cal J}(\csp '(u,{\bf y})\;\rightarrow\;

2003: \exists x\; \phi)\eta$.

2004: $(\csp '-\csp '(u,{\bf y}))$ does not contain $u$ or ${\bf y}$, so:

2005: $(\csp '-\csp'(u,{\bf y}))\theta '\models_{\cal J}(\csp '(u,{\bf y})\wedge

2006: u=u\eta\wedge{\bf y}={\bf y}\eta\;\rightarrow\;

2007: \exists x\; \phi)\theta '$.

2008: As $u$ does not occur in $(\exists x\;\phi)\theta '$,

2009: we can apply the crucial fact to get

2010: 

2011: $(\csp '-\csp'(u,{\bf y}))\theta '\;\wedge\;\exists u\; 

2012: (\csp '(u,{\bf y})\;\wedge\;

2013: u=u\eta\;\wedge\;{\bf y}={\bf y}\eta)\theta '\models_{\cal J}\;

2014: (\exists x\; \phi)\theta '$.

2015: Now we can make $\theta '$ more specific by re-instantiating the values

2016: ${\bf y}\eta$ for the variables in ${\bf y}$. 

2017: This suffices (by (1)).

2018: \item In this case there is no fresh $u$ which produces a 

2019:         $\tupel{\csp ';\eta}\in\mycons (

2020:         \tupel{\csp ;\theta}\mysem{\phi\verz{x/u}})$.

2021:         The induction hypothesis then gives

2022:         $\tupel{\csp ;\theta}\models_{\cal J}

2023:         (\neg\phi\verz{x/u})$ (for all fresh $u$), from which

2024:         $\tupel{\csp ;\theta}\models_{\cal J}(\exists x\;\phi)$ (as $u$ is fresh

2025:         w.r.t. $\theta$). \hfill{$\Box$}

2026: \end{enumerate} 

2027: 

2028: \end{document}

2029: