1: \documentclass{tlp}    % Specifies the document style.

2: 

3: \usepackage{times}

4: \usepackage[german,english]{babel}

5: \usepackage{algorithm}

6: \usepackage{algorithmic}

7: \usepackage{epsfig}

8: \usepackage{xspace}

9: \usepackage{url}

10: \usepackage{harvard}

11: 

12: \newcommand{\nop}[1]{}

13: 

14: \renewcommand{\textfraction}{.1}

15: 

16: 

17: \newcommand{\dlv}{{\bf\small{DLV}}\xspace}

18: \newtheorem{example}{Example}

19: 

20: \newtheorem{theorem}{Theorem}

21: \newtheorem{fact}{Fact}

22: \newtheorem{definition}{Definition}

23: \newtheorem{proposition}{Proposition}

24: \newtheorem{corollary}{Corollary}

25: \newtheorem{lemma}{Lemma}

26: 

27: \newenvironment{theorem*}[2]%

28: {\begin{trivlist} \item[] {\bf

29: #1~\protect{\ref{#2}}}\it}{\end{trivlist}}

30: 

31: 

32: \newcommand{\qed}{\hfill$\Box$}

33: \def\h {\hspace{1cm}}

34: \def\Or{\vee}

35: \def\And{\wedge}

36: \def\U{{U_\gp}}

37: \def\OL{{\cal OL}}

38: \def\DOL{{\cal DOL}}

39: \def\dol{{\cal DOL}}

40: \def\PM{{P^M}}

41: \def\R{{\cal R }}

42: \def\SMSD{SMS^{\DOL}}

43: \def\LP{{\cal LP}}

44: \def\O{{\cal O}}

45: \def\gp{{\cal P}}

46: \def\gd{{\cal D}}

47: \def\D{{\cal D}}

48: \def\gk{{\cal K}}

49: \def\Mneg{\neg (\BP-M)}

50: \def\BPA{2^{B_{\gp} }}

51: \def\PDRM{\PD^{\R_M}}

52: \def\PDRI{\PD^{\R_I}}

53: \def\bj{{\bf J}}

54: \def\bi{{\bf I}}

55: \def\TP{{\cal T}_{\gp}}

56: \def\TPS{\overline{{\cal T}_{\gp}}}

57: \def\twoBP{{2}^{\BP}}

58: \def\twoBPBP{{2}^{\BP \cup \neg. \BP}}

59: \def\Nat{\cal N}

60: 

61: \def\+{\hspace*{0.5cm}}

62: \def\-{\+\+}

63: \def\MM{{\rm MM}}

64: \def\MP{{M^+}}

65: \def\MN{{M^-}}

66: \def\DOL{{\cal DOL}}

67: \def\RedPI{P^{I}}

68: \def\RedPM{P^{M}}

69: \def\BP {B_{\gp}}

70: \def\DAT{{\tt Datalog}}

71: \def\datn{\mbox{$\rm Datalog^{\neg}$}}

72: \def\dat{\mbox{$\tt Datalog^{\vee}$}}

73: \def\Min{{\rm MM}}

74: \def\PH{\Pi_{\CP}}

75: 

76: \def\BD{{\cal D\!B}}

77: \def\DD{{\bf D}}

78: \def\DB{D\!B}

79: \def\derives{\leftarrow}

80: \def\Q{{\cal Q}}

81: \def\QQ{{\bf Q}}

82: 

83: \def\PD{\PP\!_{D}}

84: \def\POSS{\exists}

85: \def\CERT{\forall}

86: \def\EPOSS{{\cal E \! X \! P}}

87: \def\ECERT{{\cal E \! X \! P}^\CERT}

88: \def\XS{{\cal X\!S}}

89: \def\RR{{\bf R}}

90: 

91: 

92: \newcommand{\tuple}[1]{\langle#1\rangle}

93: 

94: 

95: \newcommand{\SigmaP}[1]{{\Sigma}_{#1}^{P}}

96: \newcommand{\PiP}[1]{{\Pi}_{#1}^{P}}

97: \newcommand{\DeltaP}[1]{{\Delta}_{#1}^{P}}

98: \newcommand{\ThetaP}[1]{{\Theta}_{#1}^{P}}

99: 

100: \newcommand{\polytrans}{\leq_m^p}

101: \newcommand{\tabstretch}{\raisebox{0ex}[3ex][2ex]{}}

102: 

103: \renewcommand{\P}{\mbox{${\cal P}$}}

104: \newcommand{\base}{\mbox{B$_{\cal P}$}}

105: \newcommand{\universo}{\mbox{U$_{\cal P}$}}

106: \newcommand{\non}{\mbox{$\neg$}}

107: \newcommand{\ap}{\mbox{A$_{\cal P}$}}

108: \newcommand{\apc}{\mbox{$\hat{A}_{{\cal P},C}$}}

109: \newcommand{\pfc}{\mbox{PF$_{C}$}}

110: \newcommand{\set}[1]{\{#1\}}

111: 

112: \newcommand{\Pol}{{\rm P}}

113: \newcommand{\NP}{\mbox{${\rm N\!P}$}}

114: \newcommand{\coNP}{\mbox{${\rm coN\!P}$}}

115: \newcommand{\CONP}{\mbox{${\rm coN\!P}$}}

116: 

117: \newcommand{\irule}[1]{\ensuremath{\mathtt{#1}}}

118: 

119: \newcommand{\tneg}{\ensuremath{\neg}}

120: \newcommand{\dneg}{\ensuremath{\mathtt{not}}}

121: 

122: \def\cNP{\NP \cap \mbox{co}\NP}

123: \def\PP{\gp}

124: \def\GUSP{GUS_{\gp}}

125: \def\GUSPD{GUS_{\PD}}

126: \def\GusP{\GUS_{\PP}}

127: \def\punto{\hspace*{\fill}{\rule[-0.5mm]{1.5mm}{3mm}}}

128: \def\DLPI{{\rm DLP\mbox{$^{<}$}}}

129: \def\DLPII{{\rm DLP\mbox{$^{<,ic}$}}}

130: \def\DOL{{\cal DOL}}

131: \def\PS{{\cal P\!S}}

132: \def\MS{{\cal M\!S}}

133: \def\LS{{\cal L\!S}}

134: \def\TS{{\cal T\!S}}

135: \def\LS{{\cal L\!S}}

136: \def\WS{{\cal W\!S}}

137: \def\bldl{\smallskip\[\bf\begin{array}{ll}}

138: \def\cldl{\vspace{-0.4cm}\[\bf\begin{array}{ll}}

139: \def\eldl{\end{array}\]\rm}

140: \def\prule#1#2{\tt #1 \leftarrow & \tt #2 \\}

141: 

142: \begin{document}

143: \bibliographystyle{dcu}

144: 

145: \title{Disjunctive Logic Programs with Inheritance}

146: \author[F. Buccafurri, W. Faber and N. Leone]

147: {FRANCESCO BUCCAFURRI\\

148: DIMET -- Universit{\`a} di Reggio Calabria

149: 89100, Reggio Calabria, Italia\\

150: \email{bucca@ns.ing.unirc.it}

151: \and

152: WOLFGANG FABER\\

153: Institut f{\"u}r Informationssysteme,

154: Technische Universit{\"a}t Wien,

155: 1040 Vienna, Austria\\

156: \email{faber@kr.tuwien.ac.at}

157: \and

158: NICOLA LEONE\\

159: Dipartimento di Matematica,

160: Universit{\`a} degli Studi della Calabria,

161: 87030 Rende (CS), Italia\\

162: \email{leone@unical.it}}

163: 

164: \maketitle

165: 

166: \begin{abstract}

167: The paper proposes a new knowledge representation language, called $\DLPI$,

168: which extends disjunctive logic programming (with strong negation)

169: by inheritance.

170: The addition of inheritance enhances the knowledge modeling

171: features of the language providing a natural representation

172: of default reasoning with exceptions.\\

173: A declarative model-theoretic semantics of $\DLPI$ is provided,

174: which is shown to generalize the Answer Set Semantics

175: of disjunctive logic programs.\\

176: The knowledge modeling features of the language are illustrated

177: by encoding classical nonmonotonic problems in $\DLPI$.\\

178: The complexity of $\DLPI$ is analyzed, proving that inheritance does

179: not cause any computational overhead, as reasoning in $\DLPI$ has

180: exactly the same complexity as reasoning in disjunctive logic

181: programming.  This is confirmed by the existence of an efficient

182: translation from $\DLPI$ to plain disjunctive logic programming.

183: Using this translation, an advanced KR system supporting the $\DLPI$

184: language has been implemented on top of the \dlv system and has

185: subsequently been integrated into \dlv.

186: \end{abstract}

187: 

188: 

189: 

190: \section{Introduction}

191: Disjunctive logic programs

192: are logic programs where disjunction is allowed in the heads of the rules

193: and negation as failure (NAF) may occur in the bodies of the rules.

194: Such programs are now widely recognized as a valuable tool for

195: knowledge representation and commonsense reasoning

196: \cite{bara-gelf-94,lobo-etal-92,gelf-lifs-91}.

197: One of the attractions of disjunctive logic programming

198: is its ability to naturally model incomplete

199: knowledge \cite{bara-gelf-94,lobo-etal-92}.

200: The need to differentiate between atoms which are false because

201: of the failure to prove them true (NAF, or CWA negation)

202: and atoms the falsity of which is explicitly provable

203: led to extend disjunctive logic programs by strong negation

204: \cite{gelf-lifs-91}.

205: Strong negation, permitted also in the heads of rules,

206: further enhances the knowledge modeling features of the language,

207: and its usefulness is widely acknowledged in the literature

208: \cite{alfe-pere-92,bara-gelf-94,kowa-sadr-90,alfe-etal-96,saka-inou-96,alfe-etal-98a}.

209: However, it does not allow to represent default reasoning with

210: exceptions in a direct and natural way.

211: Indeed, to render  a default rule $r$ {\em defeasible},

212: $r$ must at least be equipped with an extra negative literal,

213: which ``blocks'' inferences from $r$ for abnormal instances \cite{gelf-son-97}.

214: For instance, to encode the famous nonmonotonic reasoning (NMR) example stating

215: that birds {\em normally} fly while penguins do not fly, one should 

216: write%

217: \footnote{\dneg{} and \tneg{} denote the weak negation symbol

218: and the strong negation symbol, respectively.}

219: the rule

220: \[\irule{fly(X) \derives bird(X),\ \dneg{}\ \tneg fly(X).}\]

221: along with the fact

222: \[\irule{\tneg fly(penguin).}\]

223: 

224: 

225: This paper proposes an extension of disjunctive logic programming

226: by inheritance, called $\DLPI$. The addition of inheritance

227: enhances the knowledge modeling features of the language. Possible

228: conflicts are solved in favor of the rules which are ``more

229: specific'' according to the inheritance hierarchy. This way, a

230: direct and natural representation of default reasoning with

231: exceptions is achieved (e.g., defeasible rules do not need to be

232: equipped with extra literals as above -- see section \ref{KR}).

233: 

234: The main contributions of the paper are the following:

235: \begin{itemize}

236: \item

237: We formally define the $\DLPI$ language, providing a declarative

238: model theoretic semantics of $\DLPI$, which

239: is shown to generalize the Answer Set Semantics

240: of \cite{gelf-lifs-91}.

241: \item

242: We illustrate the knowledge modeling features of the language

243: by encoding classical nonmonotonic problems in $\DLPI$.

244: Interestingly, $\DLPI$ also supplies a very natural representation of

245: frame axioms.

246: \item

247: We analyze the computational complexity of reasoning over $\DLPI$

248: programs.

249: Importantly,

250: while inheritance enhances the knowledge modeling ability of disjunctive logic

251: programming, it does not cause any computational overhead,

252: as reasoning in $\DLPI$ has exactly the same complexity

253: as reasoning in disjunctive logic programming.

254: \item

255: We compare $\DLPI$ to related work proposed in the literature. In

256: particular, we stress the differences between $\DLPI$ and

257: Disjunctive Ordered Logic ($\DOL$)

258: \cite{bucc-etal-98a,bucc-etal-99c}; we point out the relation to

259: the Answer Set Semantics of \cite{gelf-lifs-91}; we compare $\DLPI$

260: with prioritized disjunctive logic programs \cite{saka-inou-96};

261: we analyze its relationships to inheritance networks \cite{tour-86}

262: and we discuss the possible application of $\DLPI$

263: to give a formal semantics to updates of logic programs.

264: \cite{alfe-etal-98b,mare-trus-94,leon-etal-95b}.

265: \item

266: We implement a $\DLPI$ system.

267: To this end, we first design an efficient translation

268: from $\DLPI$ to plain disjunctive logic programming.

269: Then, using this translation, we implement a

270: $\DLPI$ evaluator on top of the \dlv system

271: \cite{eite-etal-98a}.

272: It is part of \dlv and can be freely retrieved from \cite{dlvi-web}.

273: \end{itemize}

274: 

275: The sequel of the paper is organized as follows.

276: The next two sections provide a formal definition of $\DLPI$;

277: in particular, its syntax is given in Section

278: \ref{syntax} and its semantics is defined in Section \ref{sec:semantics}.

279: Section \ref{KR} shows the use of $\DLPI$ for knowledge representation

280: and reasoning, providing a number of sample $\DLPI$ encodings.

281: Section \ref{sec:complexity} analyzes the computational complexity

282: of the main reasoning tasks arising in the framework of $\DLPI$.

283: Section \ref{sec:relatedwork} discusses related work.

284: The main issues underlying the implementation

285: of our $\DLPI$ system are tackled in Section \ref{sec:implementation},

286: and our conclusions are drawn in Section \ref{sec:conclusion}.

287: 

288: 

289: \section{Syntax of $\DLPI$}\label{syntax}

290: This section provides a formal description of

291: syntactic constructs of the language.

292: 

293: Let the following disjoint sets be given: a set $\cal V$

294: of {\em variables}, a set

295: $\Pi$ of {\em predicates}, a set

296: $\Lambda$ of {\em constants}, and

297: a finite partially ordered set of symbols

298: $(\cal O, <)$,

299: where $\cal O$ is a set of strings, called {\em object identifiers},

300: and $<$ is a strict partial order

301: (i.e., the relation $<$ is:

302: (1) irreflexive -- $c \not < c\;\; \forall c\in \cal O$, and

303: (2) transitive -- $a<b \wedge b<c \Rightarrow a<c\;\; \forall a,b,c\in \cal O$).

304: 

305: A $term$ is either a constant in $\Lambda$ or a variable

306: in $\cal V$.%

307: \footnote{Note that function symbols

308: are not considered in this paper.}

309: 

310: An $atom$ is a construct of the form

311: $a(t_{1},..., t_{n})$, where $a$ is a $predicate$ of arity $n$

312: in $\Pi$ and $t_{1},..., t_{n}$ are terms.

313: 

314: A $literal$ is either a $positive~literal$ $p$ or a

315: $negative~literal$ $\tneg ~p$, where $p$ is an atom ($\tneg$ is the $strong~negation$ symbol).

316: Two literals are $complementary$ if they are of the form $p$ and $\tneg

317: p$, for some atom $p$.

318: 

319: Given a literal $L$, $\tneg .L$ denotes its complementary literal.

320: Accordingly, given a set $A$ of literals,

321: $\tneg .A$ denotes the set \{$\tneg .L~|~L \in A$\}.

322: 

323: A {\em  rule} $r$ is an expression of the form

324: 

325: $\quad

326: a_1\Or\cdots\Or

327:         a_n \derives b_1,\cdots, b_k, \dneg\;

328:         b_{k+1},\cdots, \dneg\; b_m \ \bigotimes \quad\quad n\geq 1,\ m\geq 0

329: $

330: \\

331: where $a_1,\cdots ,a_n,b_1,\cdots ,b_m$ are literals,

332: $\dneg$ is the {\em negation as failure} symbol

333: and $\bigotimes$ is either (1) the symbol '.' or (2)

334: the symbol '!'.

335: In case (1) $r$ is a {\em defeasible rule},

336: in case (2) it is a {\em strict rule}.

337: 

338: The disjunction $a_1\Or\cdots\Or a_n$ is the {\em head} of $r$, while

339: the conjunction $b_1,$ $\ldots,$ $b_k,$ $\dneg\; b_{k+1},$ $\ldots,$ $\dneg\; b_m$ is the {\em

340: body} of $r$.

341: $b_1, ... , b_k$ is called the

342: {\em positive part} of the body of $r$ and

343: $\dneg\;b_{k+1},... ,\dneg\; b_ m$ is called the

344: {\em NAF (negation as failure) part} of the body of $r$.

345: We often denote the sets of literals appearing in the head, in the

346: positive, and in the NAF part of the body of a rule

347: $r$ by $Head(r)$, $Body^+(r)$, and $Body^-(r)$, respectively.

348: 

349: If the body of a rule $r$ is empty, then $r$ is called {\em fact}. The

350: symbol '$\derives$' is usually omitted from facts.

351: 

352: An {\em object} $o$ is a pair $\tuple{oid(o), \Sigma(o)}$, where $oid(o)$ is an

353: object identifier in $\cal O$ and $\Sigma(o)$ is a (possibly empty) set of

354: rules.

355: 

356: A {\em knowledge base} on $\cal O$ is a set of objects, one for each element

357: of $\cal O$.

358: 

359: Given a knowledge base $\cal K$ and an object identifier $o \in \cal O$, the

360: {\em $\DLPI$ program for} $o$ ({\em on} $\cal K$)

361: is the set of objects

362: $\gp = \{ (o' , \Sigma(o' )) \in {\cal K} \ | \  o=o' \ or \ o <  o'  \}$.

363: 

364: 

365: The relation $<$ induces a partial order on $\gp$ in the obvious way,

366: that is, given $o_i = (oid(o_i),\Sigma(o_i))$ and $o_j= (oid(o_j),

367: \Sigma(o_j))$,

368: $o_i < o_j$ iff $oid(o_i) < oid(o_j)$ (read "$o_i$ is more specific

369: than $o_j$").

370: 

371: A term, an atom, a literal, a rule, 

372: or program is {\em ground} if no variable appears in it.

373: 

374: Informally, a knowledge base can be viewed as a set of

375: {\em objects} embedding the definition of their

376: properties specified through disjunctive logic rules,

377: organized in an IS-A (inheritance) hierarchy

378: (induced by the relation $<$).

379: A program $\gp$ for an object $o$ on a knowledge base $\cal K$

380: consists of the portion of $\cal K$ "seen" from $o$ looking up in

381: the IS-A hierarchy. Thanks to the inheritance mechanism, $\gp$

382: incorporates the knowledge explicitly defined for $o$ plus the

383: knowledge inherited from the higher objects.

384: 

385: If a knowledge base admits a {\em bottom} element (i.e., an object

386: less than all the other objects, by the relation $<$), we usually

387: refer to the knowledge base as ``program'', since it is equal to the

388: program for the bottom element.

389: 

390: Moreover, we represent

391: the {\em transitive reduction} of

392: the relation $<$ on the objects.%

393: \footnote{$(a,b)$ is in the

394: transitive reduction of $<$ iff $a < b$ and

395: there is no $c$ such that $a < c$ and $c < b$.}

396: An object $o$ is denoted as $oid(o) : o_1, \ldots, o_n \; \Sigma(o)$%

397: \footnote{The set $\Sigma(o)$ is denoted without commas as separators.}

398: , where

399: $(oid(o),o_1),$ $\ldots$, $(oid(o),o_n)$ are exactly those pairs of the transitive reduction of $<$,

400: in which the first object identifier is $oid(o)$.  $o$ is referred to as {\em sub-object} of

401: $o_1, \ldots, o_n$.

402: 

403: \begin{example}\label{ex-1}

404: {

405: Consider the following program $\gp$:

406: \begin{tabbing}

407: \quad\quad \irule{o_2:o_1}  \= \{ \= p \kill

408: \quad\quad \irule{o_1}      \> \{ \> \irule{a \Or \tneg b \leftarrow c, \dneg \ d.} \quad \irule{e \derives b!} \ \} \\

409: \quad\quad \irule{o_2:o_1}  \>  \{ \> \irule{b.} \quad \irule{\tneg a \Or c.} \quad \irule{c \leftarrow b.} \}

410: \end{tabbing}

411: $\gp$ consists of two objects \irule{o_1} and \irule{o_2}.

412: \irule{o_2} is a sub-object of \irule{o_1}.

413: According to the convention illustrated above, the knowledge base on which

414: $\gp$ is defined coincides with $\gp$, and the object

415: for which $\gp$ is defined is \irule{o_2} (the bottom object).

416: }

417: $\punto$

418: \end{example}

419: 

420: \section{Semantics of $\DLPI$}\label{sec:semantics}

421: In this section we assume that a knowledge base $\cal K$ is given and

422: an object $o$ has been fixed.

423: Let $\gp$ be the $\DLPI$ program for $o$ on $\cal K$.

424: The {\em Universe} $\U$ of $\gp$ is the set of all constants

425: appearing in the rules. 

426: The {\em Base} $\BP$ of $\gp$ is the set of all

427: possible ground literals constructible from

428: the predicates appearing in the rules of $\gp$ and

429: the constants occurring in $\U$.

430: Note that, unlike in traditional logic programming the Base of

431: a $\DLPI$ program contains both positive and negative literals.

432: Given a rule 

433: $r$  occurring in $\gp$,

434: a {\em ground instance} of $r$ is a rule obtained from $r$

435: by replacing every variable $X$ in $r$ by $\sigma(r)$, where

436: $\sigma$ is a mapping from the variables occurring in $r$ to

437: the constants in $\U$.

438: We denote by $ground( \gp )$ the (finite) multiset of

439: all instances of

440: the rules 

441: occurring in $\gp$.

442: The reason why $ground(\gp)$

443: is a multiset is that a rule may appear in several

444: different objects of $\gp$, and we require the respective ground

445: instances be distinct.

446: Hence, we can define a function $obj\_of$ from

447: ground instances of rules in $ground(\gp)$

448: onto the set $\cal O$ of the object identifiers, associating

449: with a ground instance ${\overline r}$ of $r$

450: the (unique) object of $r$.

451: 

452: A subset of ground literals in $\BP$ is said to be {\em consistent} if

453: it does not contain a pair of complementary literals.

454: An {\em interpretation} $I$ is a consistent subset of $\BP$.

455: Given an interpretation $I \subseteq \BP$,

456: a ground literal (either positive

457: or negative) $L$ is {\em true}

458: w.r.t. $I$ if $L \in I$ holds.

459: $L$ is {\em false} w.r.t. $I$ otherwise.

460: 

461: 

462: Given a rule $r \in ground( \gp )$, the head of

463: $r$ is {\em true} in $I$ if

464: at least one literal of the head is true w.r.t $I$.

465: The body of $r$ is {\em true} in $I$ if:

466: (1) every literal in $Body^+(r)$ is true w.r.t. $I$, and

467: (2) every literal in $Body^-(r)$ is false w.r.t. $I$.

468: A rule $r$ is {\em satisfied} in $I$ if

469: either the head of $r$ is true in $I$ or the

470: body of $r$ is not true in $I$.

471: 

472: 

473: Next we introduce the concept of a {\em model}

474: for a $\DLPI$-program.

475: Different from traditional logic programming, the

476: notion of satisfiability of rules

477: is not sufficient for this goal,

478: as it does not take into account the presence of explicit contradictions.

479: Hence, we first present some preliminary definitions.

480: 

481: Given two ground rules $r_1$ and $r_2$

482: we say that $r_1$ {\em threatens} $r_2$ {\em on}

483: a literal $L$ if (1)

484: $\tneg . L \in Head(r_1)$ and $L \in Head(r_2)$,

485: (2) $obj\_of(r_1) < obj\_of(r_2)$

486: and (3) $r_2$ is defeasible,

487: 

488: \begin{definition}\label{ov}

489: {\em

490: Given an interpretation $I$ and two ground rules

491: $r_1$ and $r_2$ such that $r_1$ threatens $r_2$ on $L$ we say that

492: $r_1$ {\em overrides} $r_2$ {\em on} $L$ {\em in} $I$ if:

493: (1) $\tneg. L \in I$, and

494: (2) the body of $r_2$ is true in $I$.

495: 

496: A (defeasible) rule $r \in ground(\gp)$ is {\em overridden in}

497: $I$ if for each $L \in Head(r)$ there

498: exists $r_1 \in ground(\gp)$ such that

499: $r_1$ overrides $r$ on $L$ in $I$.

500: }

501: $\punto$

502: \end{definition}

503: 

504: Intuitively, the notion of overriding allows us to solve conflicts

505: arising between rules with complementary heads.

506: For instance, suppose that both $a$ and $\tneg a$ are derivable in $I$

507: from rules $r$ and $r'$, respectively.

508: If $r$ is more specific than $r'$ in the inheritance hierarchy

509: and $r'$ is not strict,

510: then $r'$ is overridden, meaning that $a$ should be preferred to $\tneg a$

511: because it is derivable from a more trustable rule.

512: 

513: Observe that, by definition of overriding, strict rules cannot

514: be overridden, since they are never threatened.

515: 

516: \begin{example}\label{ex-2}

517: {

518: Consider the program $\gp$ of Example \ref{ex-1}.

519: Let \irule{I = \{ \tneg a, b, c, e \}} be an interpretation.

520: Rule \irule{\tneg a \Or c \leftarrow. } in the object \irule{o_2} overrides

521: rule \irule{a \Or \tneg b \leftarrow c, \dneg \ d.} in \irule{o_1}

522: on the literal \irule{a} in \irule{I}.

523: Moreover, rule \irule{b  \leftarrow.} in \irule{o_2} overrides

524: rule \irule{a \Or \tneg b \leftarrow c, \dneg \ d.} in \irule{o_1}

525: on the literal \irule{\tneg b} in \irule{I}.

526: Thus, the rule

527: \irule{a \Or \tneg b \leftarrow c, \dneg \ d.} in \irule{o_1}

528: is overridden in \irule{I}.

529: }

530: $\punto$

531: \end{example}

532: 

533: \begin{example}\label{ex-5}

534: {

535: Consider the following program $\gp$:

536: \begin{tabbing}

537: \quad\quad \irule{o_2:o_1} \= \{ \= p \kill

538: \quad\quad \irule{o_1}     \> \{ \> \irule{\tneg a!} \quad \irule{\tneg b.} \ \} \\

539: \quad\quad \irule{o_2:o_1} \> \{ \> \irule{a \derives \dneg \ b.} \quad \irule{b \derives \dneg \ a.}  \}

540: \end{tabbing}

541: Consider now the interpretations \irule{M_1 = \{a, \tneg b \}} and 

542: \irule{M_2 = \{b, \tneg a \}}. While the rule \irule{\tneg b.} is overridden

543: in \irule{M_2}, the rule \irule{\tneg a!} cannot be overridden since

544: it is a strict rule. Due to overriding, strict rules and defeasible

545: rules are quite different from the semantic point of view. In our

546: example, the overriding mechanism allows us to invalidate the

547: defeasible rule \irule{\tneg b.} in favor of the more trustable

548: one \irule{b \derives \dneg \ a.} (w.r.t.\ the interpretation \irule{M_2}). In

549: words, the defeasible rule is invalidated in \irule{M_2} because of a

550: more specific contradictory rule and no inconsistency is

551: generated. In other words, it is possible to find an

552: interpretation containing the literal \irule{b} (i.e., stating an

553: exception for the rule \irule{\tneg b.}) such that all the rules

554: of $\gp$ are either satisfied or overridden (i.e., invalidated) in

555: it. Such an interpretation is just \irule{M_2}. This cannot happen for

556: the strict rule \irule{\tneg a!}. Indeed, no interpretation

557: containing the literal \irule{a} (i.e., stating an exception for the

558: strict rule) can be found which satisfies all non-overridden rules of $\gp$. }

559: $\punto$

560: \end{example}

561: In the example above we have implicitly used the notion of {\em

562: model} for a program $\gp$ that we next formally provide. A model

563: for a program is an interpretation satisfying all its non

564: overridden rules.

565: 

566: \begin{definition}\label{model}

567: {\em

568: Let $I$ be an interpretation for $\gp$.

569: $I$ is a {\em model for} $\gp$ if every rule

570: in $ground(\gp)$ is satisfied or overridden in  $I$.

571: $I$ is a {\em minimal model for} $\gp$ if no (proper)

572: subset of $I$ is a model for $\gp$.

573: }

574: $\punto$

575: \end{definition}

576: 

577: Note that strict rules must be satisfied in every model, since they

578: cannot be overridden.

579: 

580: \begin{example}\label{ex-5bis}

581: {

582: It is easy to see that \irule{M_1=\{ a, \tneg b \}} is not a

583: model for the program $\gp$ of Example \ref{ex-5} since the rule

584: \irule{\tneg a!} is neither overridden nor satisfied. On the contrary,

585: \irule{M_2=\{ b, \tneg a \}} is a model for $\gp$, since

586: \irule{\tneg b.} is overridden by the rule

587: \irule{b \derives \dneg \ a.} The latter rule is satisfied

588: since \irule{b \in M_2}. The rule \irule{\tneg a!}

589: is satisfied as \irule{\tneg a \in M_2} and

590: the rule \irule{a \derives \dneg \ b.} is satisfied since

591: both body and head are false w.r.t. \irule{M_2}.

592: }

593: \end{example}

594: 

595: Next we define the transformation $G_I$ based on which

596: our semantics is defined. This transformation applied to

597: a program $\gp$ w.r.t. an interpretation $I$

598: output a set of rules $G_I(\gp)$ with no

599: negation by failure in the body.

600: Intuitively, such rules are those remaining from $ground(\gp)$

601: by (1) eliminating the rules overridden in the interpretation $I$, (2)

602: deleting rules whose NAF part is not "true" in $I$

603: (i.e., some literal negated by negation as failure occurs in $I$) and

604: (3) deleting the NAF part of all the remainder rules.

605: Since the transformation encodes the overriding mechanism,

606: the distinction between strict rules and defeasible rules in $G_I(\gp)$

607: is meaningless

608: (indeed, there is no difference between strict and defeasible rules

609: except for the overriding mechanism where

610: the upper rule is required to be defeasible).

611: For this reason the syntax of rules in $G_I(\gp)$

612: can be simplified by dropping the symbol $.$ from defeasible rules

613: and the symbol $!$ from strict rules.

614: \begin{definition}\label{reduction}

615: {\em

616: Given an interpretation $I$ for $\gp$,

617: the {\em reduction of} $\gp$

618: {\em w.r.t.} $I$, denoted by

619: $G_I(\gp)$, is the set of rules

620: obtained from $ground(\gp)$ by

621: (1) removing every rule overridden in $I$,

622: (2) removing every rule $r$ such that

623: $Body^-(r) \cap I \neq \emptyset$,

624: (3) removing the NAF part from the bodies of the remaining rules.

625: }

626: $\punto$

627: \end{definition}

628: 

629: \begin{example}\label{ex-3}

630: {

631: Consider the program $\gp$ of Example \ref{ex-1}.

632: Let \irule{I} be the interpretation

633: \irule{\{\tneg a , b, c, e\}}. As

634: shown in Example \ref{ex-2}, rule

635: \irule{a \Or \tneg b \derives c, \dneg \ d.} is overridden in \irule{I}.

636: Thus,

637: $G_I(\gp)$ is the set of rules

638: \{\irule{\tneg a \Or c.} \quad \irule{e \derives b.} \quad \irule{b.} \quad \irule{c \derives b.} \}.

639: Consider now the interpretation

640: \irule{M = \{a,b,c,e \}}.

641: It is easy to see that

642: $G_{M}(\gp) = \{ \irule{a \Or \tneg b \derives c.} \quad \irule{\tneg a \Or c.}

643: \quad \irule{e \derives b.} \quad \irule{b.} \quad \irule{c \derives b.} \}$.

644: }

645: $\punto$

646: \end{example}

647: 

648: We observe that the reduction of a program is simply

649: a set of ground rules. Given a set $S$ of

650: ground rules, we denote

651: by $pos(S)$ the

652: positive disjunctive program

653: (called the {\em positive version of} $S$), obtained

654: from $S$ by considering each negative

655: literal $\tneg p (\bar X)$ as a positive

656: one with predicate symbol $\tneg p$.

657: 

658: \begin{definition}\label{answerset}

659: {\em

660: Let $M$ be a model for $\gp$.

661: We say that $M$ is a

662: {\em ($\DLPI$-)answer set} for $\gp$

663: if $M$ is a minimal model of the positive

664: version $pos(G_M(\gp))$ of $G_M(\gp)$.

665: }

666: $\punto$

667: \end{definition}

668: 

669: Note that interpretations must be consistent by definition, so

670: considering $pos(G_M(\gp))$ instead of $G_M(\gp)$ does not lose

671: information in this respect.

672: 

673: Note that the notion of minimal model of Definition~\ref{model} cannot

674: be used in Definition~\ref{answerset}, as $G_M$ is a set of rules and

675: not a $\DLPI$ program.

676: 

677: \begin{example}\label{ex-4}

678: {

679: Consider the program $\gp$ of Example \ref{ex-1}:

680: 

681: It is easy to see that the interpretation

682: \irule{I} of Example \ref{ex-3} is not an answer set

683: for $\gp$. Indeed, although

684: \irule{I} is a model for $pos(G_I(\gp))$ it is

685: not minimal, since the interpretation

686: \irule{\{b,c,e \}} is a model for $pos(G_I(\gp))$, too.

687: Note that the interpretation \irule{I' = \{ b,c,e\}} is not

688: an answer set for $\gp$. Indeed,

689: $G_{I'}(\gp) = \{$~\irule{a \Or \tneg b \derives c.} \quad

690: \irule{\tneg a \Or c.} \quad \irule{e \derives b.} \quad \irule{b.} \quad \irule{c \derives b.} $\}$

691: and \irule{I'} is not a model for  $pos(G_{I'}(\gp))$, since

692: the rule \irule{a \Or \tneg b \derives c.} is not satisfied in \irule{I'}.

693: 

694: On the other hand, the interpretation \irule{M} of

695: Example \ref{ex-3} is an answer set for $\gp$,

696: since \irule{M} is a minimal model for

697: $pos(G_{M}(\gp))$.

698: Moreover, it can be easily realized that

699: \irule{M} is the only answer set for $\gp$.

700: 

701: Finally, the program $\gp$ of Example \ref{ex-5} admits one

702: consistent answer set \irule{M_2 = \{ b, \tneg a \}}. Note that

703: if we replace the strict rule \irule{\tneg a!} by a defeasible

704: rule \irule{\tneg a.}, $\gp$ admits two answer sets, namely 

705: \irule{M_1 = \{ a, \tneg b \}} and \irule{M_2 = \{ b, \tneg a \}}.

706: Asserting \irule{\tneg a}

707: by a strict rule, prunes the answer set \irule{M_1} stating the

708: exception (truth of the literal \irule{a}) to this rule. } $\punto$

709: \end{example}

710: 

711: 

712: It is worthwhile noting that if a rule \irule{r} is not satisfied in a

713: model \irule{M}, then \emph{all} literals in the head of \irule{r}

714: must be overridden in \irule{M}.

715: 

716: Let $\gp_1$ be the program

717: \begin{tabbing}

718: \quad\quad \irule{o2 : o_3} \= \{ \= dummy \kill

719: \quad\quad \irule{o_3} \> \{ \> \irule{a \Or b.} \quad  \irule{\derives b.} \}\\

720: \quad\quad \irule{o_2 : o_3} \> \{ \> \irule{\tneg a.} \}

721: \end{tabbing}

722: and $\gp_2$

723: \begin{tabbing}

724: \quad\quad \irule{o2 : o_1} \= \{ \= dummy \kill

725: \quad\quad \irule{o_1} \> \{ \> \irule{a.} \quad \irule{\derives b.} \}\\

726: \quad\quad \irule{o_2 : o_1} \> \{ \> \irule{\tneg a.} \}

727: \end{tabbing}

728: 

729: Then, \irule{\{\tneg a\}} is not a model for program $\gp_1$,

730: because the head literal \irule{b} in the head of \irule{a \Or b.} is not overridden

731: in \irule{M}. If we drop \irule{b} from rule \irule{a \Or b.}, then \irule{\{\tneg a\}} is a model of the

732: resulting program $\gp_2$.

733: 

734: Observe also that two programs having the same answer sets, as

735: \irule{o_1} and \irule{o_3} (both have the single answer set

736: \irule{\{\tneg a\}}), may get different answer sets even if we add the

737: same object to both of them. Indeed, program $\gp_1$ has no answer

738: set, while program $\gp_2$ has the answer set \irule{\{\tneg a\}}.

739: 

740: This is not surprising, as a similar phenomenon also arises in normal

741: logic programming where \irule{P_1 = \{a.\}} and 

742: \irule{P_2 = \{a \derives \dneg b.\}} have the same answer set \irule{\{a\}},

743: while \irule{P_1 \cup \{b.\}} and \irule{P_2 \cup \{b.\}} have different

744: answer sets (\irule{\{a,b\}} and \irule{\{b\}}, respectively).

745: 

746: Finally we show that each answer set of a program $\gp$ is also a

747: minimal model of $\gp$:

748: 

749: \begin{proposition}\label{is-minimal}

750: If $M$ is an answer set for $\gp$, then $M$ is

751: a minimal model of $\gp$.

752: \end{proposition}

753: 

754: {\noindent

755: \proof

756: By contradiction suppose $M'$ is a model for $\gp$ such that

757: $M' \subset M$.

758: 

759: First we show that $M'$ is a model for $pos(G_M(\gp))$ too,

760: i.e., every rule in $pos(G_M(\gp))$ is satisfied in $M'$.

761: Recall that $pos(G_M(\gp))$ is the positive version of the program

762: obtained by applying the transformation $G_M$ to the program

763: $ground(\gp)$. Consider a generic rule $r$

764: of $ground(\gp)$. Since $M'$ is a model

765: for $\gp$ either (i) $r$ is overridden in $M'$ or (ii)

766: is satisfied in $M'$.

767: 

768: In case (i), since $M' \subset M$,

769: from Definition \ref{ov} immediately follows that

770: $r$ is overridden in $M$ too.

771: Thus, $r$ does not occur in $G_M(\gp)$

772: since the transformation $G_M$ removes all rules overridden in $M$.

773: 

774: In case (ii) (i.e., $r$ is satisfied in $M'$), if $r$ is such that

775: $B(r) \cap M \neq \emptyset$, then the rule is removed by $G_M$.

776: Otherwise, $r$ is transformed by $G_M$ into a rule $r'$

777: obtained from $r$ by dropping the NAF part from the body.

778: Since $r$ is satisfied in $M'$, also $r'$ is satisfied in $M'$.

779: As a consequence, all the rules of $pos(G_M(\gp))$ are

780: satisfied in $M'$, that is $M' \subset M$ is a model for $pos(G_M(\gp))$.

781: Thus, by Definition \ref{answerset}, $M$ is not an answer set

782: for $\gp$ since it is not a minimal model of $pos(G_M(\gp))$.

783: The proof is hence concluded.

784: }

785: 

786: \section{Knowledge Representation with $\DLPI$}\label{KR}

787: 

788: In this section, we present a number of examples which illustrate

789: how knowledge can be represented using $\DLPI$.

790: To start, we show the $\DLPI$ encoding of a classical example

791: of nonmonotonic reasoning.

792: 

793: \begin{example}\label{ex-penguin}

794: {

795: Consider the following program $\gp$

796: with $\O(\gp)$ consisting of three

797: objects

798: \irule{bird}, \irule{penguin} and \irule{tweety},  such that

799: \irule{penguin} is a sub-object of \irule{bird} and

800: \irule{tweety} is a sub-object of \irule{penguin}:

801: 

802: \begin{tabbing}

803: \irule{tweety:penguin} \= \{ \= p \kill

804: \irule{bird}           \> \{ \> \irule{flies.} \  \}

805: \\

806: \irule{penguin:bird}   \> \{ \> \irule{\tneg flies!} \  \}

807: \\

808: \irule{tweety:penguin} \> \{   \  \}

809: \end{tabbing}

810: Unlike in traditional logic programming, our language supports two

811: types of negation, that is {\em strong negation} and {\em negation

812: as failure}. Strong negation is useful to express negative pieces

813: of information under the complete information assumption. Hence, a

814: negative fact (by strong negation) is true only if it is

815: explicitly derived from the rules of the program. As a

816: consequence, the head of rules may contain also such negative

817: literals and rules can be conflicting on some literals. According

818: to the inheritance principles, the ordering relationship between

819: objects can help us to assign different levels of reliability to

820: the rules, allowing us to solve possible conflicts. For instance,

821: in our example, the contradicting conclusion {\em tweety both

822: flies and does not fly} seems to be entailed from the program (as

823: \irule{tweety} is a \irule{penguin} and \irule{penguin}s are \irule{bird}s, both \irule{flies}

824: and \irule{\tneg flies} can be derived from the rules of the program).

825: However, this is not the case. Indeed, the "lower" rule \irule{\tneg

826: flies.} specified in the object \irule{penguin} is considered

827: as a sort of refinement to the first general rule, and thus the

828: meaning of the program is rather clear: {\em tweety does not fly},

829: as tweety is a penguin. That is, \irule{\tneg flies.} is

830: preferred to the default rule \irule{flies.} as the hierarchy

831: explicitly states the specificity of the former. Intuitively,

832: there is no doubt that \irule{M = \{ \tneg flies \}} is the only

833: reasonable conclusion. }

834: $\punto$

835: \end{example}

836: The next example, from the field of database authorizations,

837: combines the use of both weak and strong negation.

838: \begin{example}\label{ex-security}

839: {

840: Consider the following knowledge base representing a set

841: of security specification about a simple {\em part-of}

842: hierarchy of objects.

843: \begin{eqnarray}

844: \lefteqn{\irule{o_1}} \nonumber\\

845: & \{ \nonumber\\

846: && \irule{authorize(bob) \derives \dneg \ authorize(ann).} \label{rule:auth1}\\

847: && \irule{authorize(ann) \Or authorize(tom) \derives \dneg \ \tneg authorize(alice).} \label{rule:auth2}\\

848: && \irule{authorize(amy)!} \label{rule:auth3}\\

849: & \} \nonumber\\

850: \lefteqn{\irule{o_2:o_1}} \nonumber\\

851: & \{ \nonumber\\

852: && \irule{\tneg authorize(alice)!} \label{rule:auth4}\\

853: & \} \nonumber\\

854: \lefteqn{\irule{o_3:o_1}} \nonumber\\

855: & \{ \nonumber\\

856: && \irule{\tneg authorize(bob)!} \label{rule:auth5}\\

857: & \} \nonumber

858: \end{eqnarray}

859: 

860: Object \irule{o_2} is  part-of the object \irule{o_1} as well as \irule{o_3}

861: is part-of \irule{o_1}.

862: Access authorizations to objects are specified by

863: rules with head predicate \irule{authorize} and subjects to

864: which authorizations are granted appear as arguments.

865: Strong negation is utilized to encode negative authorizations

866: that represent explicit denials. Negation as failure

867: is used to specify the

868: absence of authorization (either positive or negative).

869: Inheritance implements the automatic propagation

870: of authorizations from an object to

871: all its sub-objects.

872: The overriding mechanism allows us to represent

873: exceptions: for instance, if an object $o$ inherits a positive

874: authorization but a denial for the same subject

875: is specified in $o$, then

876: the negative authorization prevails on the positive one.

877: Possible loss of control due to overriding mechanism can be

878: avoided by using strict rules: strict authorizations cannot

879: be overridden.

880: 

881: Consider the program $\gp_{o_2} = \{ ( \irule{o_1}, \{ (\ref{rule:auth1}), (\ref{rule:auth2}), (\ref{rule:auth3}) \} ),

882: ( \irule{o_2}, \{ (\ref{rule:auth4}) \} ) \}$ for the object \irule{o_2} on the above knowledge

883: base. This program defines the access control for the object

884: \irule{o_2}. Thanks to the inheritance mechanism, authorizations

885: specified for the object \irule{o_1}, to which \irule{o_2} belongs, are

886: propagated also to \irule{o_2}. It consists of rules (\ref{rule:auth1}), (\ref{rule:auth2}) and

887: (\ref{rule:auth3}) (inherited from \irule{o_1}) and (\ref{rule:auth4}). Rule (\ref{rule:auth1}) states that

888: \irule{bob} is authorized to access object \irule{o_2} provided that no

889: authorization for \irule{ann} to access \irule{o_2} exists. Rule (\ref{rule:auth2})

890: authorizes either \irule{ann} or \irule{tom} to access \irule{o_2} provided that no

891: denial for \irule{alice} to access \irule{o_2} is derived. The strict rule

892: (\ref{rule:auth3}) grants to \irule{amy} the authorization to access object \irule{o_1}.

893: Such authorization can be considered "strong", since no exceptions

894: can be stated to it without producing inconsistency. As a

895: consequence, all the answer sets of the program contain the

896: authorization for \irule{amy}. Finally, rule (\ref{rule:auth4}) defines a denial

897: for \irule{alice} to access object \irule{o_2}. Due to the absence of the

898: authorization for \irule{ann}, the authorization to \irule{bob} of accessing

899: the object \irule{o_2} is derived (by rule (\ref{rule:auth1})). Further, the explicit

900: denial to access the object \irule{o_2} for \irule{alice} (rule (\ref{rule:auth4})) allows

901: to derive neither authorization for \irule{ann} nor for \irule{tom} (by rule

902: (\ref{rule:auth2})). Hence, the only answer set of this program is \irule{\{

903: authorize(bob), \tneg authorize(alice), authorize(amy) \}}.

904: 

905: Consider now the program

906: $\gp_{o_3} = \{ ( \irule{o_1}, \{ (\ref{rule:auth1}), (\ref{rule:auth2}) \} ), ( \irule{o_3}, \{ (\ref{rule:auth5}) \} ) \}$

907: for the object \irule{o_3}.

908: Rule (\ref{rule:auth5}) defines a denial for \irule{bob} to access

909: object \irule{o_3}.

910: The authorization for \irule{bob} (defined by rule (\ref{rule:auth1})) is no longer derived.

911: Indeed, even if rule (\ref{rule:auth1}) allows to derive

912: such an authorization due to the absence of authorizations for

913: \irule{ann}, it is overridden by the explicit denial (rule (\ref{rule:auth5})) defined

914: in the object \irule{o_3} (i.e., at a more specific level).

915: The body of rule (\ref{rule:auth2}) inherited from \irule{o_1} is true for this program

916: since no denial for alice can be derived, and it entails a mutual exclusive access to object

917: \irule{o_3} for \irule{ann} and \irule{tom} (note that no other head contains

918: \irule{authorize(ann)} or \irule{authorize(bob)}).

919: The program $\gp_{o_3}$ admits two answer sets, namely

920: \{\irule{authorize(ann)}, \irule{\tneg authorize(bob)}, \irule{authorize(amy)}\} and

921: \{\irule{authorize(tom)}, \irule{\tneg authorize(bob)}, \irule{authorize(amy)}\} representing

922: two alternative authorization sets to grant

923: the access to the object \irule{o_3}.

924: }

925: $\punto$

926: \end{example}

927: 

928: \subsection*{Solving the Frame Problem}

929: 

930: The frame problem has first been addressed by McCarthy and Hayes

931: \cite{mcca-haye-69}, and in the meantime a lot of research has been

932: conducted to overcome it (see e.g.\ \cite{shan-97} for a survey).

933: 

934: In short, the frame problem arises in planning, when actions and

935: fluents are specified: An action affects some of the fluents, but all

936: unrelated fluents should remain as they are. In most formulations

937: using classical logic, one must specify for every pair of

938: actions and unrelated fluents that the fluent remains unchanged.

939: Clearly this is an undesirable overhead, since with $n$ actions and

940: $m$ fluents, $n \times m$ clauses would be needed.

941: 

942: Instead, it would be nice to be able to specify for each fluent that it

943: {\em ``normally remains valid''} and that only actions which explicitly

944: entail the contrary can change them.

945: 

946: Indeed, this goal can be achieved in a very elegant way using $\DLPI$:

947: One object contains the rules which specify {\em inertia} (the fact

948: that fluents normally do not change). Another object inherits from it

949: and specifies the actions and the effects of actions --- in this way a

950: very natural, straightforward and effective representation is

951: achieved, which avoids the frame problem.

952: 

953: \begin{example}\label{ex-yaleshooting}

954: As an example we show how the famous Yale Shooting Problem, which is due to

955: Hanks and McDermott \cite{hank-mcde-87}, can be represented and

956: solved with $\DLPI$:

957: 

958: The scenario involves an individual (or in a less violent version a

959: turkey), who can be shot with a gun.  There are two fluents, \irule{alive}

960: and \irule{loaded}, which intuitively mean that the individual is alive and

961: that the gun is loaded, respectively. There are three actions,

962: \irule{load}, \irule{wait} and \irule{shoot}. Loading has the effect that the gun is

963: loaded afterwards, shooting with the loaded gun has the effect that

964: the individual is no longer alive afterwards (and also that the gun is

965: unloaded, but this not really important), and waiting has no

966: effects.

967: 

968: The problem involves {\em temporal projection}: It is known that initially the individual is alive, and

969: that first the gun is loaded, and after waiting, the gun is shot

970: with. The question is: Which fluents hold after these actions and

971: between them?

972: 

973: In our encoding, the \irule{inertia} object contains the defaults for the

974: fluents, the \irule{domain} object additionally specifies the effects of

975: actions, while the \irule{yale} object encodes the problem instance.

976: 

977: For the time framework we use the \dlv bounded integer built-ins: The

978: upper bound \irule{n} of positive integers is specified by either adding the

979: fact \irule{\#maxint = n.} to the program or by passing the option

980: \irule{-N=n} on the commandline (this overrides any \irule{\#maxint =

981: n.} statement). It is then possible to use the built-in constant

982: \irule{\#maxint}, which evaluates to the specified upper bound, and

983: several built-in predicates, of which in this paper we just use

984: \irule{\#succ(N,N1)} , which holds if \irule{N1} is the successor of

985: \irule{N} and \irule{N1 \leq \#maxint}. For additional \dlv built-in

986: predicates, consult the \dlv homepage \cite{dlv-web}.

987: 

988: \begin{eqnarray}

989: \lefteqn{\irule{inertia}} \nonumber\\

990: & \{ \nonumber\\

991: && \irule{alive(T1) \derives alive(T), \#succ(T,T1).}\\

992: && \irule{\tneg alive(T1) \derives \tneg alive(T), \#succ(T,T1).}\\

993: && \irule{loaded(T1) \derives loaded(T), \#succ(T,T1).}\\

994: && \irule{\tneg loaded(T1) \derives \tneg loaded(T), \#succ(T,T1).}\\

995: & \} \nonumber\\

996: \lefteqn{\irule{domain : inertia}} \nonumber\\

997: & \{\\

998: && \irule{loaded(T1) \derives load(T), \#succ(T,T1)!} \\

999: && \irule{\tneg loaded(T1) \derives shoot(T), loaded(T), \#succ(T,T1)!} \\

1000: && \irule{\tneg alive(T1) \derives shoot(T), loaded(T), \#succ(T,T1)!} \\

1001: & \} \nonumber\\

1002: \lefteqn{\irule{yale : domain}} \nonumber\\

1003: & \{\\

1004: && \irule{load(0)! \quad wait(1)! \quad shoot(2)! \quad alive(0)!} \\

1005: & \} \nonumber

1006: \end{eqnarray}

1007: 

1008: The only answer set for this program (and \irule{\#maxint = 3}) contains, besides the facts of the \irule{yale}

1009: object, \irule{loaded(1)}, \irule{loaded(2)},

1010: \irule{alive(0)}, \irule{alive(1)}, \irule{alive(2)} and

1011: \irule{\tneg loaded(3)}, \irule{\tneg alive(3)}.

1012: That is, the individual is alive until the shoot action is

1013: taken, and no longer alive afterwards, and the gun is loaded between

1014: loading and shooting.

1015: $\punto$

1016: \end{example}

1017: 

1018: We want to point out that this formalism is equally suited for solving

1019: problems which involve finding a plan (i.e.\ a sequence of actions)

1020: rather than doing temporal projection (determining the effects of a given plan) as in the Yale

1021: Shooting Problem: You have to add a rule \irule{action(T) \Or \tneg action(T)

1022: \derives \#succ(T,T1).} for every action, and you have to specify the

1023: goal state by a query, e.g. \irule{\tneg alive(3), \tneg

1024: loaded(3)?} A query is a \dlv language feature which (for this example) is equivalent to

1025: the rules \irule{h \derives \tneg alive(3), \tneg loaded(3).} and 

1026: \irule{i \derives \dneg \ h, \dneg \ i.}, meaning that only answer sets containing

1027: \irule{\tneg alive(3)} and \irule{\tneg loaded(3)} should be considered.

1028: 

1029: Below you find a classical plan-finding example: The blocksworld domain and the

1030: Sussman anomaly as a concrete problem.

1031: 

1032: \begin{example}

1033: In \cite{erde-99}, several planning problems, including the

1034: blocksworld problems, are encoded using disjunctive datalog.

1035: 

1036: In general, planning problems can be effectively specified using

1037: action languages (e.g.\

1038: \cite{gelf-lifs-93,dung-93,giun-lifs-98,lifs-99}).  Then, a

1039: translation from these languages to another language (in our case

1040: $\DLPI$) is applied.

1041: 

1042: We omit the step of describing an action

1043: language and the associated translation, and directly show the

1044: encoding of an example planning domain in disjunctive datalog. This

1045: encoding is rather different from the one presented in \cite{erde-99}.

1046: 

1047: The objects in the blocksworld are one \irule{table} and an arbitrary number

1048: of labeled cubic \irule{block}s. Together, they are referred to as

1049: \irule{loc}ations.

1050: 

1051: The state of the blocksworld at a particular time can be fully

1052: specified by the fluent \irule{on(B,L,T)}, which specifies that

1053: block \irule{B} resides on location \irule{L} at time \irule{T}.

1054: 

1055: So, first we state in the object \irule{bw\_inertia} that the fluent

1056: \irule{on} is inertial.

1057: \begin{eqnarray}

1058: \lefteqn{\irule{bw\_inertia}} \nonumber\\

1059: & \{ \nonumber\\

1060: && \irule{on(B,L,T1) \derives on(B,L,T), \#succ(T,T1).}\\

1061: & \} \nonumber

1062: \end{eqnarray}

1063: 

1064: We continue to define the blocksworld domain in the object \irule{bw\_domain}, which inherits from the inertia object:

1065: \begin{eqnarray}{}

1066: \lefteqn{\irule{bw\_domain : bw\_inertia}} \nonumber\\

1067: & \{ \nonumber\\

1068: && \irule{move(B,L,T) \Or \tneg move(B,L,T) \derives block(B), loc(L), \#succ(T,T1)!} \label{rule:bw:guess}\\

1069: &&                               \irule{on(B,L,T1) \derives move(B,L,T), \#succ(T,T1)!} \label{rule:bw:on_effect}\\

1070: &&                               \irule{\tneg on(B,L,T1) \derives move(B,L1,T), on(B,L,T), \#succ(T,T1)!} \label{rule:bw:not_on_effect}\\

1071: &&                               \irule{\derives move(B,L,T), on(B1,B,T).} \label{rule:bw:constraint_clear}\\

1072: &&                               \irule{\derives move(B,B1,T), on(B2,B1,T), block(B1).} \label{rule:bw:constraint_clear2}\\

1073: &&                               \irule{\derives move(B,B,T).} \label{rule:bw:constraint_notonitself}\\

1074: &&                               \irule{\derives move(B,L,T), move(B1,L1,T), B<>B1.} \label{rule:bw:constraint_uniquesource}\\

1075: &&                               \irule{\derives move(B,L,T), move(B1,L1,T), L<>L1.} \label{rule:bw:constraint_uniquedestination}\\

1076: &&                               \irule{loc(table)!} \\

1077: &&                               \irule{loc(B) \derives block(B)!}\\

1078: & \} \nonumber

1079: \end{eqnarray}

1080: 

1081: There is one action, which is moving a block from one location to

1082: another location. A move is started at one point in time, and it is

1083: completed before the next time. Rule (\ref{rule:bw:guess}) expresses that at any time \irule{T}, the action of

1084: moving a block \irule{B} to location \irule{L} may be initiated

1085: (\irule{move(B,L,T)}) or not (\irule{\tneg move(B,L,T)}).

1086: 

1087: Rules (\ref{rule:bw:on_effect}) and (\ref{rule:bw:not_on_effect}) specify the

1088: effects of the move action: The

1089: moved block is at the target location at the next time, and no longer

1090: on the source location.

1091: 

1092: (\ref{rule:bw:constraint_clear}) -- (\ref{rule:bw:constraint_uniquedestination})

1093: are constraints, and their semantics is that in any

1094: answer set the conjunction of their literals must not be true.%

1095: \footnote{\label{foot:constraints}We use constraints for clarity, but they can be eliminated

1096: by rewriting \irule{\derives B.} to \irule{p \derives B, \dneg \ p.},

1097: where \irule{p} is a new symbol which does not appear anywhere else

1098: in the program.}

1099: Their respective meanings are:

1100: (\ref{rule:bw:constraint_clear}): A moved block must be clear.

1101: (\ref{rule:bw:constraint_clear2}): The target of a move must be clear if it is a block (the table may hold an arbitrary number of blocks).

1102: (\ref{rule:bw:constraint_notonitself}) A block may not be on itself.

1103: (\ref{rule:bw:constraint_uniquesource}) and (\ref{rule:bw:constraint_uniquedestination}): No two move actions may be performed at the same time.

1104: 

1105: The timesteps are again represented by \dlv's integer built-in

1106: predicates and constants.

1107: 

1108: \begin{figure}

1109: \begin{center}

1110: \epsfig{file=sussman.eps}

1111: \end{center}

1112: \caption{The Sussman Anomaly}

1113: \label{sussman}

1114: \end{figure}

1115: 

1116: What is left is the concrete problem instance, in our case the

1117: so-called Sussman Anomaly (see Figure \ref{sussman}):

1118: \begin{eqnarray}

1119: \lefteqn{\irule{sussman : bw\_domain}} \nonumber\\

1120: & \{ \nonumber\\

1121: && \irule{block(a)!} \  \quad \irule{block(b)!} \  \quad \irule{block(c)!} \label{rule:bwi:blocks}\\

1122: && \irule{on(b, table, 0)!} \  \quad \irule{on(c, a, 0)!} \  \quad \irule{on(a, table, 0)!} \label{rule:bwi:initial_situation}\\

1123: & \} \nonumber\\

1124: \lefteqn{\irule{on(c, b, \#maxint),on(b, a, \#maxint), on(a, table, \#maxint) ?}} \label{rule:bwi:query}

1125: \end{eqnarray}

1126: 

1127: Since different problem

1128: instances may involve different numbers of blocks, the blocks are

1129: defined as facts (\ref{rule:bwi:blocks}) together with the problem instance.%

1130: \footnote{Note that usually the instance will be separated from

1131: the domain definition.}

1132: 

1133: We give the initial situation by facts (\ref{rule:bwi:initial_situation}), while the goal situation is

1134: specified by query (\ref{rule:bwi:query}). This query enforces that only those answer sets

1135: are computed, in which the conjunction of the query literals is true.

1136: 

1137: \end{example}

1138: 

1139: \section{Computational Complexity}

1140: \label{sec:complexity}

1141: \def\parag{{\vspace{0.15in} \noindent}}

1142: 

1143: As for the classical nonmonotonic formalisms

1144: \cite{mare-trus-91,mare-trus-90,reit-80},

1145: two important decision problems, corresponding to two different

1146: reasoning tasks, arise in $\DLPI$:

1147: \\

1148: {\em (Brave Reasoning)}

1149: Given a $\DLPI$ program $\gp$ and a ground literal $L$,

1150: decide whether there exists an answer set $M$ for $\gp$

1151: such that $L$ is true w.r.t. $M$.

1152: \\

1153: {\em (Cautious Reasoning)}

1154: Given a $\DLPI$ program $\gp$ and a ground literal $L$,

1155: decide whether $L$ is true in all answer sets for $\gp$.

1156: 

1157: We next prove that the complexity of reasoning

1158: in $\DLPI$ is exactly

1159: the same as in traditional disjunctive logic programming.

1160: That is, inheritance comes for free, as the addition of inheritance

1161: does not cause any computational overhead.

1162: We consider the propositional case, i.e., we consider ground

1163: $\DLPI$ programs.

1164: 

1165: \begin{lemma}\label{recognition}

1166: Given a ground $\DLPI$ program $\gp$ and an interpretation

1167: $M$ for $\gp$,

1168: deciding whether $M$ is an answer set

1169: for $\gp$ is in $\CONP$.

1170: \end{lemma}

1171: 

1172: \begin{proof}

1173: We check in $\NP$ that $M$ \textbf{is not} an answer set of $\gp$

1174: as follows.

1175: Guess a subset $I$ of $M$, and verify that:

1176: (1) $M$ is not a model for $pos(G_M(\gp))$, or

1177: (2) $I$ is a model for $pos(G_M(\gp))$ and $I\subset M$.

1178: The construction of $pos(G_M(\gp))$ (see Definition \ref{reduction})

1179: is feasible in polynomial time, and the tasks (1) and (2) are

1180: clearly tractable.

1181: Thus, deciding whether $M$ is not an answer set for $\gp$ is in $\NP$,

1182: and, consequently, deciding whether $M$ is an answer set

1183: for $\gp$ is in $\CONP$.

1184: \end{proof}

1185: 

1186: \begin{theorem}\label{brave}

1187: Brave Reasoning on $\DLPI$ programs is $\SigmaP{2}$-complete.

1188: \end{theorem}

1189: 

1190: \begin{proof}

1191: Given a ground $\DLPI$ program $\gp$ and a ground literal

1192: $L$, we verify that $L$ is a brave consequence of $\gp$ as follows.

1193: Guess a set $M \subseteq \BP$ of ground literals, check that

1194: (1) $M$ is an answer set for $\gp$, and (2) $L$ is true w.r.t. $M$.

1195: Task (2) is clearly polynomial; while (1) is in $\CONP$,

1196: by virtue of Lemma \ref{recognition}.

1197: The problem therefore lies in $\SigmaP{2}$.

1198: 

1199: $\SigmaP{2}$-hardness follows from Theorem

1200: \ref{the:answerset} and the results in \cite{eite-gott-95,eite-etal-97f}.

1201: \end{proof}

1202: 

1203: \begin{theorem}\label{cautious}

1204: Cautious Reasoning on $\DLPI$ programs is $\PiP{2}$-complete.

1205: \end{theorem}

1206: 

1207: \begin{proof}

1208: Given a ground $\DLPI$ program $\gp$ and a ground literal

1209: $L$, we verify that $L$ is not a cautious consequence of $\gp$ as follows.

1210: Guess a set $M \subseteq \BP$ of ground literals, check that

1211: (1) $M$ is an answer set for $\gp$, and (2) $L$ is not true w.r.t. $M$.

1212: Task (2) is clearly polynomial; while (1) is in $\CONP$,

1213: by virtue of Lemma \ref{recognition}.

1214: Therefore, the complement of cautious reasoning is in $\SigmaP{2}$,

1215: and cautious reasoning is in $\PiP{2}$.

1216: 

1217: $\PiP{2}$-hardness follows from Theorem

1218: \ref{the:answerset} and the results in \cite{eite-gott-95,eite-etal-97f}.

1219: \end{proof}

1220: 

1221: \section{Related Work}\label{sec:relatedwork}

1222: 

1223: \subsection{Answer Set Semantics}

1224: 

1225: Answer Set Semantics, proposed by Gelfond and Lifschitz

1226: in \cite{gelf-lifs-91}, is the most widely acknowledged semantics

1227: for disjunctive logic programs with strong negation.

1228: For this reason, while defining the semantics of our language,

1229: we took care of ensuring full agreement with Answer Set Semantics

1230: (on inheritance-free programs).

1231: 

1232: \begin{theorem}\label{the:answerset}

1233: Let $\gp$ be a $\DLPI$ program consisting of a single object

1234: $o=\tuple{oid(o),\Sigma(o)}$.%

1235: \footnote{

1236: On inheritance-free programs, there is no difference

1237: between strict and defeasible rules.

1238: Therefore, without loss of generality

1239: we assume that rules are of only one type here.

1240: This allows us to drop the symbol ('.' or '!') at the end of the rules

1241: of single object programs.}

1242: Then, $M$ is an answer set of $\gp$ if and only if it is a consistent

1243: answer set of $\Sigma(o)$ (as defined in \cite{gelf-lifs-91}).

1244: \end{theorem}

1245: 

1246: \begin{proof}

1247: First we show that $G_M(\gp)$ is equal to $\Sigma(o)^M$ (as defined in

1248: \cite{gelf-lifs-91}):

1249: 

1250: Deletion rule (1) of Definition \ref{reduction} never applies,

1251: since for every literal L and any two rules $r_1$, $r_2$ $\in

1252: ground(\gp)$, $obj\_of(r_1) \not < obj\_of(r_2)$ holds, thus

1253: violating condition (1) in Definition \ref{ov} and therefore no

1254: rule can be overridden. It is evident that the deletion rules (2)

1255: and (3) of Definition \ref{reduction} are equal to deletion rules

1256: (i) and (ii) of the definition of $\Pi^S$ in \S 7 in

1257: \cite{gelf-lifs-91}, respectively. The first ones delete rules, where

1258: some NAF literal is contained in $M$, while the second ones delete

1259: all NAF literals of the remaining rules.

1260: 

1261: Next, we show that the criteria for a consistent set $M$ of

1262: literals being an answer set of a positive (i.e. NAF free)

1263: program (as in \cite{gelf-lifs-91}) is equal to the notion of

1264: satisfaction:

1265: 

1266: Since the set is consistent, condition (ii) in \S 7 of \cite{gelf-lifs-91}

1267: does not apply. Condition (i) says: $L_{k+1}, \dots, L_{m} \in M$ (the

1268: body is true) implies that the head is true. This is logically equivalent to ``The body is not true or the head is true'', which is the definition of rule satisfaction.

1269: 

1270: In total we have that the minimal models of $pos(G_M(\gp))$ are equal

1271: to the consistent answer sets of $\Sigma(o)^M$, since answer sets are

1272: minimal by definition.

1273: 

1274: Additionally, we require in Definition \ref{answerset} that $M$ is

1275: also a model of $\gp$, while in \cite{gelf-lifs-91} there is no such

1276: requirement. However, all minimal models of $pos(G_M(\gp))$ are also

1277: models of $\gp$: All rules in $G_M(\gp)$ are satisfied, and only the

1278: deletion rules (2) and (3) of Definition \ref{reduction} have been

1279: applied (as shown above). So, for any rule $r$, which has been deleted

1280: by (2), some literal in $Body^-(r)$ is in $M$, so $r$'s body is not

1281: true, and thus $r$ is satisfied in $M$. If a rule $r$, which has been

1282: transformed by (3), is satisfied without $Body^-(r)$, then either

1283: $Head(r)$ is true or $Body^+(r)$ is not true, so adding any NAF part

1284: to it does not change its satisfaction status.

1285: \end{proof}

1286: 

1287: Theorem \ref{the:answerset} shows that the set of rules contained in a

1288: single object of a $\DLPI$ program has precisely the same answer sets

1289: (according to the definition in \cite{gelf-lifs-91}) as the single object

1290: program (according to Definition~\ref{answerset}).

1291: 

1292: For a $\DLPI$ program

1293: $\gp$ consisting of more than one object, the answer sets (as defined in

1294: \cite{gelf-lifs-91}) of the collection of all rules in $\gp$ in general do not coincide with the answer sets of $\gp$.

1295: 

1296: For instance the program

1297: \begin{tabbing}

1298: \irule{o1:o} \= \{ \= p \kill

1299: \irule{o}           \> \{ \> \irule{p.} \  \}

1300: \\

1301: \irule{o1:o}   \> \{ \> \irule{\tneg p.} \  \}

1302: \end{tabbing}

1303: has the answer set \irule{\{\tneg p \}}, while the disjunctive logic program

1304: \irule{\{p.\ \tneg p.\}} does not have a consistent answer set.

1305: 

1306: Nevertheless, in Section~\ref{sec:implementation_I} we will show that

1307: each $\DLPI$ program $\gp$ can be translated into a disjunctive logic

1308: program $\gp'$, the semantics of which is equivalent to the semantics

1309: of $\gp$. However, this translation requires the addition of a number

1310: of extra predicates.

1311: 

1312: \subsection{Disjunctive Ordered Logic}\label{DOL}

1313: 

1314: Disjunctive Ordered Logic ($\DOL$) is an extension of

1315: Disjunctive Logic Programming with strong negation and inheritance

1316: (without default negation)

1317: proposed in \cite{bucc-etal-98a,bucc-etal-99c}.

1318: The $\DLPI$ language incorporates some ideas taken from $\DOL$.

1319: However, the two languages are very different in several respects.

1320: Most importantly, unlike with $\DLPI$,

1321: even if a program belongs to the common fragment of $\DOL$

1322: and of the language of \cite{gelf-lifs-91}

1323: (i.e., it contains neither inheritance nor default negation),

1324: $\DOL$ semantics is completely different from Answer Set Semantics,

1325: because of a different way of handling contradictions.%

1326: \footnote{Actually, this was a main motivation for the authors

1327: to look for a different language.}

1328: In short, we observe the following differences between $\DOL$ and

1329: $\DLPI$:

1330: \begin{itemize}

1331: \item

1332: $\DOL$ does not include default negation $\dneg$,

1333: while $\DLPI$ does.

1334: \item

1335: $\DOL$ and $\DLPI$ have different semantics

1336: on the common fragment.

1337: Consider a program $\gp$ consisting of a single object

1338: $o=\tuple{oid(o),\Sigma(o)}$, where

1339: $\Sigma(o)=\{\irule{p.}\quad\irule{\tneg p.} \}$.

1340: Then, according to $\DOL$, the semantics of $\gp$

1341: is given by two models, namely, \irule{\{p\}} and \irule{\{\tneg p\}}.

1342: On the contrary, $\gp$ has no answer set according to

1343: $\DLPI$ semantics.

1344: \item

1345: $\DLPI$ generalizes (consistent) Answer Set Semantics to

1346: disjunctive logic programs with inheritance, while $\DOL$ does not.

1347: \end{itemize}

1348: 

1349: \subsection{Prioritized Logic Programs}

1350: 

1351: $\DLPI$ can be also seen as an attempt to handle priorities in

1352: disjunctive logic programs

1353: (the lower the object in the inheritance hierarchy,

1354: the higher the priority of its rules).

1355: 

1356: There are several works on preference handling in logic programming

1357: \cite{delg-etal-00a,brew-eite-98,gelf-son-97,nute-94,kowa-sadr-90,prad-mink-96,saka-inou-96}.

1358: However, we are aware of only one previous work on priorities

1359: in \textbf{disjunctive} programs, namely, the

1360: paper by Sakama and Inoue \cite{saka-inou-96}.

1361: This interesting work can be seen as an extension of

1362: Answer Set Semantics to deal with priorities.

1363: Comparing the two approaches under the perspective of priority handling,

1364: we observe the following:

1365: \begin{itemize}

1366: \item

1367: On priority-free programs, the two languages yield essentially

1368: the same semantics, as they generalize Answer Set Semantics and

1369: Consistent Answer Set Semantics, respectively.

1370: \item

1371: In \cite{saka-inou-96}, priorities are defined among %(ground)

1372: \textbf{literals}, while priorities concern program

1373: \textbf{rules} in $\DLPI$.

1374: \item

1375: The different kind of priorities (on rules vs.\ literals)

1376: and the way how they are dealt with in the two approaches

1377: imply different complexity in the respective reasoning tasks.

1378: Indeed, from the simulation of abductive reasoning

1379: in the language of \cite{saka-inou-96}, and the complexity

1380: results on abduction reported in \cite{eite-etal-97k},

1381: it follows that brave reasoning is $\SigmaP{3}$-complete

1382: for the language of \cite{saka-inou-96}.

1383: On the contrary, brave reasoning is ``only''

1384: $\SigmaP{2}$-complete in $\DLPI$%

1385: \footnote{We refer to the complexity in the propositional case here.}.

1386: \end{itemize}

1387: 

1388: \cite{delg-etal-00a} deals with nondisjunctive programs, but the

1389: authors note that their semantics-defining transformation ``is also

1390: applicable to disjunctive logic programs''. In this formalism, the

1391: preference relation is defined by regular atoms (with a set of

1392: constants representing the rules), allowing the definition of

1393: dynamic preferences. However, the semantics of the preferences is

1394: based on the order of rule application (or defeating) and thus seems to be

1395: quite different from our approach.

1396: 

1397: A comparative analysis of the various approaches to the treatment

1398: of preferences in ($\vee$-free)

1399: logic programming has been carried out

1400: in \cite{brew-eite-98}.

1401: 

1402: \subsection{Inheritance Networks}

1403: 

1404: From a different perspective, the objects of a

1405: $\DLPI$ program can also be seen as the nodes of an inheritance network.

1406: 

1407: We next show that $\DLPI$ satisfies the basic semantic principles

1408: which are required for inheritance networks in \cite{tour-86}.

1409: 

1410: \cite{tour-86} constitutes a fundamental attempt to present a formal

1411: mathematical theory of multiple inheritance with exceptions.

1412: The starting point of this work is the consideration

1413: that an intuitively acceptable semantics for inheritance

1414: must satisfy two basic requirements:

1415: \begin{enumerate}

1416: \item

1417: Being able to reason with redundant statements, and

1418: \item

1419: not making unjustified choices in ambiguous situations.

1420: \end{enumerate}

1421: 

1422: Touretzky illustrates this intuition by means of two basic examples.

1423: 

1424: The former requirement is presented by means of the {\em Royal

1425: Elephant} example, in which we have the following knowledge:

1426: ``Elephants are gray.'', ``Royal elephants are elephants.'', ``Royal

1427: elephants are not gray.'', ``Clyde is a royal elephant.'', ``Clyde is

1428: an elephant.''

1429: 

1430: 

1431: The last statement is clearly redundant; however, since it is

1432: consistent with the others there is no reason

1433: to rule it out.

1434: Touretzky shows that an intuitive semantics should be able

1435: to recognize that Clyde is not gray, while many systems fail in

1436: this task.

1437: 

1438: Touretzky's second principle is shown by the {\em Nixon diamond} example, in which the following is known:

1439: ``Republicans are not pacifists.'',

1440: ``Quakers are pacifists.'',

1441: ``Nixon is both a Republican and a quaker.''

1442: 

1443: 

1444: According to our approach, he claims that a good semantics should draw

1445: no conclusion about the question whether Nixon is a $pacifist$.

1446: 

1447: The proposed solution for the problems above

1448: is based on a topological relation,

1449: called {\em inferential distance ordering}, stating that an individual

1450: $A$ is "nearer" to $B$ than to $C$ iff $A$ has an inference

1451: path {\em through} $B$ to $C$.

1452: If $A$ is "nearer" to $B$ than to $C$, then as far as $A$ is concerned,

1453: information coming from $B$ must be preferred w.r.t. information

1454: coming from $C$.

1455: Therefore, since Clyde is "nearer" to being a royal elephant than to

1456: being an elephant, he states that Clyde is not gray.

1457: On the contrary no conclusion is taken on Nixon, as there is not

1458: any relationship between quaker and republican.

1459: 

1460: The semantics of $\DLPI$ fully agrees with the intuition underlying the

1461: {\em inferential distance ordering}.

1462: 

1463: \begin{example}

1464: Let us represent the Royal Elephant example in our

1465: framework:

1466: \vspace{-0.2cm}

1467: \[

1468: \begin{array}{ll}

1469: \irule{elephant} & \{ \irule{gray.} \}\\

1470: \irule{royal\_elephant: elephant} & \{ \irule{\tneg gray.} \}\\

1471: \irule{clyde:elephant,\ royal\_elephant} & \{\ \}

1472: \end{array}

1473: \vspace{-0.1cm}

1474: \]

1475: %It is easy to see that

1476: The only answer set of the above

1477: $\DLPI$ program is \irule{\{\tneg gray\}}.

1478: 

1479: The Nixon Diamond example can be expressed in our language as follows:

1480: \vspace{-0.2cm}

1481: \[

1482: \begin{array}{ll}

1483: \irule{republican} & \{ \irule{\tneg pacifist.} \}\\

1484: \irule{quaker} & \{ \irule{pacifist.} \}\\

1485: \irule{nixon : republican, quaker} & \{\ \}

1486: \end{array}

1487: \vspace{-0.1cm}

1488: \]

1489: This $\DLPI$ program has no

1490: answer set, and therefore no conclusion is drawn.

1491: %$\punto$

1492: \end{example}

1493: 

1494: \subsection{Updates in Logic Programs}

1495: 

1496: The definition of the semantics of updates in logic programs is

1497: another topic where $\DLPI$ could potentially be applied.

1498: Roughly, a simple formulation of the problem is the following:

1499: Given a ($\vee$-free) logic program $P$ and

1500: a sequence $U_1,\cdots,U_n$ of successive updates

1501: (insertion/deletion of ground atoms),

1502: determine what is or is not true in the end.

1503: Expressing the insertion (deletion) of an atom $A$ by the rule

1504: $A\derives$ ($\tneg A\derives$),

1505: we can represent this problem by a $\DLPI$ knowledge base

1506: $\{\tuple{t_0,P},\tuple{t_1,\{U_1\}},\cdots,$ $\tuple{t_n,\{U_n\}}\}$

1507: ($t_i$ intuitively represents the instant of time when the update

1508: $U_i$ has been executed), where $t_n<\cdots <t_0$.%

1509: \footnote{In this context, $<$ should be interpreted as ``more recent''.}

1510: The answer sets of the program for $t_k$ can be taken as the

1511: semantics of the execution of $U_1,\cdots,U_k$ on $P$.

1512: For instance, given the logic program \irule{P=\{a\derives b, \dneg\; c\}} and the updates

1513: \irule{U_1=\{b.\}}, \irule{U_2=\{c.\}},

1514: \irule{U_3=\{\tneg b. \}}, we build the $\DLPI$ program

1515: \vspace{-0.2cm}

1516: \begin{tabbing}

1517: $\quad \irule{t_0} \quad\quad\quad$ \= $ \{\;\irule{a\derives b, c, \dneg\; d.}\;\}$

1518: \\

1519: $\quad \irule{t_1:t_0}$ \> $\{\; \irule{b.} \;\}$

1520: \\

1521: $\quad \irule{t_2:t_1}$ \> $\{\; \irule{c.} \;\}$

1522: \\

1523: $\quad \irule{t_3:t_2}$ \> $\{\; \irule{\tneg b.} \;\}$.

1524: \vspace{-0.1cm}

1525: \end{tabbing}

1526: 

1527: The answer set \irule{\{a,b,c \}} of the program for \irule{t_2} gives the semantics of the

1528: execution of \irule{U_1} and \irule{U_2} on \irule{P}; while the answer set \irule{\{c\}}

1529: of the program for \irule{t_3} expresses the semantics of the execution

1530: of \irule{U_1}, \irule{U_2} and \irule{U_3} on \irule{P} in the given order.

1531: 

1532: The semantics of updates obtained in this way is very similar

1533: to the approach adopted for the ULL language in \cite{leon-etal-95b}.

1534: Further investigations are needed on this topic to see whether

1535: $\DLPI$ can represent update problems in more general settings

1536: like those treated in \cite{mare-trus-94} and in \cite{alfe-etal-98b}.

1537: A comparative analysis of various approaches to updating logic programs

1538: is being carried out in \cite{eite-etal-2000-jelia}.

1539: Preliminaries results of this work show that,

1540: under suitable syntactic conditions,

1541: $\DLPI$ supports a nice ``iterative'' property

1542: for updates, which is missed in other formalisms.

1543: 

1544: 

1545: \section{Implementation Issues}\label{sec:implementation}

1546: \subsection{From $\DLPI$ to Plain DLP}\label{sec:implementation_I}

1547: 

1548: 

1549: In this section we show how a $\DLPI$ program can be translated into

1550: an equivalent plain disjunctive logic program (with strong negation,

1551: but without inheritance).  The translation allows us to exploit

1552: existing disjunctive logic programming (DLP) systems for the implementation

1553: of $\DLPI$.

1554: 

1555: \noindent

1556: {\bf Notation.}

1557: \begin{enumerate}

1558: \item

1559: Let $\gp$ be the input $\DLPI$ program.

1560: \item

1561: We denote  a literal by $\phi (\bar X)$,

1562: where $\bar X$ is the tuple of the literal's arguments, and

1563: $\phi$ represents an {\em adorned predicate}, that is either

1564: a predicate symbol $p$

1565: or a strongly negated predicated symbol $\tneg p$.

1566: Two adorned predicates are {\em complementary} if one is the negation

1567: of the other (e.g., $q$ and $\tneg q$ are complementary).

1568: $\tneg.\phi$ denotes the complementary adorned predicate of the adorned

1569: predicate $\phi$.

1570: \item

1571: An adorned predicate $\phi$ is

1572: {\em conflicting} if both $\phi(\bar{X})$ and $\tneg.\phi(\bar Y)$ occur in the heads of rules in $\gp$.

1573: \item

1574: Given an object $o$ in $\gp$,

1575: and a head literal $\phi(\bar X)$ of a defeasible rule in $\Sigma(o)$,

1576: we say that $\phi$ is {\em threatened in o} if a literal $\tneg.\phi(\bar Y)$

1577: occurs in the head of a rule in $\Sigma(o')$

1578: where $o' < o$.

1579: A defeasible rule $r$ in $\Sigma(o)$ is {\em threatened in o} if

1580: all its head literals are threatened in $o$.

1581: \end{enumerate}

1582: The rewriting algorithm translating $\DLPI$ programs

1583: in plain disjunctive logic programs with constraints\footnote{Again we use constraints for clarity, see footnote \ref{foot:constraints} on page \pageref{foot:constraints}}

1584: is shown in Figure \ref{alg1}.

1585: 

1586: \begin{figure}%[ht]

1587: \begin{algorithmic}

1588: \STATE \hspace{-0.3 cm} {\bf ALGORITHM}

1589: \STATE \hspace{-0.3 cm} {\bf INPUT}: a $\DLPI$-program $\gp$

1590: \STATE \hspace{-0.3 cm}

1591: {\bf OUTPUT}: a plain disjunctive logic program with constraints $DLP(\gp)$

1592: \end{algorithmic}

1593: \begin{algorithmic}[1]

1594: \STATE $DLP(\gp) \Leftarrow \{ prec'(o,o_1) \derives \ | \ o < o_1 \}$

1595: \FOR{each object $o \in \O(\gp)$}

1596: \FOR{each threatened adorned predicate $\phi$ in $o$}

1597: \STATE Add the following rule to $DLP(\gp)$:

1598: \STATE \quad $ovr'(\phi,o,X_1,\cdots,X_n) \derives \tneg . \phi'(X,X_1,\cdots,X_n), prec'(X,o)$

1599: \STATE where $n$ is the arity of $\phi$ and $X,X_1,\cdots,X_n$ are distinct variables.

1600: \ENDFOR

1601: \FOR{each rule $r$ in $\Sigma(o)$, say

1602: $\phi_1(\bar X_1) \Or  \cdots \Or \phi_n(\bar X_n) \derives BODY$,}

1603: \IF{$r$ is threatened}

1604: \STATE Add the following two rules to $DLP(\gp)$:

1605: \STATE \quad $\phi'_1( o,\bar X_1) \Or \cdots \Or \phi'_n(o,\bar X_n) \derives BODY, \ \dneg \ ovr'(r,o,\bar X_1, ... , \bar X_n)$

1606: \STATE \quad $ovr'(r,o,\bar X_1, ... , \bar X_n) \derives ovr'({\phi_1},o,\bar X_1), ... , ovr'({\phi_n},o, \bar X_n)$

1607: \ELSE

1608: \STATE Add the following rule to $DLP(\gp)$:

1609: \STATE \quad $\phi'_1( o,\bar X_1) \Or \cdots \Or \phi'_n(o,\bar X_n) \derives BODY$

1610: \ENDIF

1611: \ENDFOR

1612: \ENDFOR

1613: \FOR{each adorned predicate $\phi$ appearing in $\gp$}

1614: \STATE Add the following rule to $DLP(\gp)$:

1615: \STATE \quad $\phi(X_1,\cdots,X_n) \derives \phi'(X_0,X_1,\cdots,X_n)$

1616: \STATE where $n$ is the arity of $\phi$ and $X_0,\cdots,X_n$ are distinct variables.

1617: \ENDFOR

1618: \FOR{each conflicting adorned predicate $\phi$ appearing in $\gp$}

1619: \STATE Add the following constraint to $DLP(\gp)$:

1620: \STATE \quad $\derives \phi(X_1,\cdots,X_n), \tneg . \phi(X_1,\cdots,X_n)$

1621: \STATE where $n$ is the arity of $\phi$ and $X_1,\cdots,X_n$ are distinct variables.

1622: \ENDFOR

1623: \end{algorithmic}

1624: \caption{A Rewriting Algorithm}

1625: \label{alg1}

1626: \end{figure}

1627: 

1628: An informal description of how the algorithm proceeds is

1629: the following:

1630: \begin{itemize}

1631: \item

1632: $DLP(\gp)$ is initialized to a set of facts with head

1633: predicate $prec'$ representing the partial ordering among objects

1634: (statement 1).

1635: 

1636: \item

1637: Then, for each object $o$ in $\O(\gp)$:

1638: \begin{itemize}

1639: \item

1640: For each threatened literal $\phi(\bar X)$ appearing in $o$,

1641: rules defining when the literal is overridden are added

1642: (statements 3--7).

1643: \item

1644: For each rule $r$ belonging to $o$:

1645: \begin{enumerate}

1646: \item

1647: If $r$ is threatened, then the rule is rewritten, such that the head

1648: literals include information about the object in which they have been

1649: derived, and the body includes a literal which satisfies the rule

1650: if it is overridden.

1651: In addition, a rule is added which encodes when the rule is overridden (statements 9--12).

1652: 

1653: \item

1654: Otherwise (i.e., if $r$ is not threatened) just the rule head is rewritten as described above,

1655: since these rules cannot be overridden (statements 13--15).

1656: \end{enumerate}

1657: \end{itemize}

1658: \item

1659: For all adorned predicates in the program, we add a rule which states

1660: that an atom with this predicate holds, no matter in which object it

1661: has been derived (statements 19--23). The information in which object

1662: an atom has been derived is only needed for determination of

1663: overriding.

1664: 

1665: \item

1666: Finally, statements 24--28 add a constraint for each adorned predicate, which prevents the generation of inconsistent sets of literals.

1667: \end{itemize}

1668: 

1669: $DLP(\gp)$ is referred to as the {\em DLP version} of the program $\gp$.%

1670: \footnote{$DLP(\gp)$ is a function-free disjunctive logic program.

1671:   Allowing functions could make the algorithm notation more compact,

1672:   but would not give any computational benefit.}

1673: 

1674: We now give an example to show how the translation works:

1675: 

1676: \begin{example}\label{ex-translation}

1677: {

1678: The datalog version $DLP(\gp)$ of the program

1679: $\gp$ of Example \ref{ex-1} is:

1680: 

1681: \noindent

1682: $\begin{array}{ll}

1683: \bf (1) & \bf rules \ expliciting \ partial \ order \ among \ objects:\\

1684: & \irule{prec'(o_2,o_1).}\\

1685: \end{array}$\\

1686: $\begin{array}{ll}

1687: {\bf (2)} & {\bf rules \ for \ threatened \ adorned \ predicates \ in} \ o_1:\\

1688: & \irule{ovr'(a,o_1) \derives \tneg a'(X), prec'(X,o_1).}\\

1689: & \irule{ovr'(\tneg b, o_1)  \derives b'(X), prec'(X,o_1).}\\

1690: \end{array}$\\

1691: $\begin{array}{ll}

1692: {\bf (3)} & {\bf rewriting \ of \ rules \ in} \ o_1:\\

1693: & \irule{a'(o_1) \Or \tneg b'(o_1) \derives  c, \dneg \ d, \dneg \ ovr'(r_1,o_1).} \\

1694: & \irule{ovr'(r_1,o_1)  \derives ovr'(a,o_1), ovr'(\tneg b,o_1).}\\

1695: & \irule{e'(o_1) \derives b.}\\

1696: \end{array}$\\

1697: $\begin{array}{ll}

1698: {\bf (4)} & {\bf rewriting \ of \ rules \ in} \ o_2:\\

1699: & \irule{\tneg a'(o_2) \Or  c'(o_2).}\\

1700: & \irule{b'(o_2).}\\

1701: & \irule{c'(o_2) \derives b.}\\

1702: \end{array}$\\

1703: $\begin{array}{ll}

1704: \bf (5) & \bf projection \ rules :\\

1705: &\begin{array}{l@{\qquad}l}

1706: \irule{a \derives a'(X).} & \irule{\tneg a \derives \tneg a'(X).}\\

1707: \irule{b \derives b'(X).} & \irule{\tneg b \derives \tneg b'(X).}\\

1708: \irule{c \derives c'(X).} & \irule{d \derives d'(X).}\\

1709: \irule{e \derives e'(X).} & \\

1710:  \end{array}

1711: \end{array}$\\

1712: $\begin{array}{ll}

1713: \bf (6) & \bf constraints:\\

1714: &\irule{\derives  a, \tneg a.}\\

1715: &\irule{\derives  b, \tneg b.}

1716: \end{array}$\\

1717: }

1718: $\punto$

1719: \end{example}

1720: 

1721: Given a model $M$ for $DLP(\gp)$, $\pi(M)$ is the set of literals

1722: obtained from $M$ by eliminating all the literals with a ``primed''

1723: predicate symbol, i.e. a predicate symbol in the set $\{ prec', ovr'

1724: \} \cup \{ \phi'  \ |  \ \exists \ an \ adorned \ literal$

1725: $\phi(\bar X) \ appearing \ in \ \gp \}$. $\pi(M)$ is the set of literals

1726: without all atoms which were introduced by the translation algorithm.

1727: 

1728: The DLP version of a $\DLPI$-program $\gp$ can be used in place of

1729: $\gp$ in order to evaluate answer sets of $\gp$.  The result

1730: supporting the above statement is the following:

1731: \begin{theorem}\label{equivalence}

1732: Let $\gp$ be a $\DLPI$-program. Then,

1733: for each answer set $M$ for $\gp$ there exists a consistent answer set

1734: $M'$ for $DLP(\gp)$ such that $\pi(M') = M$.

1735: Moreover, for each consistent answer set $M'$ for $DLP(\gp)$ there exists

1736: an answer set $M$ for $\gp$ such that $\pi(M') = M$.

1737: \end{theorem}

1738: 

1739: \begin{proof}

1740: First we show that given an answer set $M$ for $\gp$ there exists

1741: a consistent answer set $M'$ for $DLP(\gp)$ such that $\pi(M') = M$.

1742: We proceed by constructing the model $M'$.

1743: Let $K_1 = \{ prec'(o,o_1) \mid o < o_1 \}$.

1744: Let $K_2$

1745: be the set of ground literals

1746: $ovr'(r,o, \bar X)$

1747: such that there exists a (defeasible) rule $r \in ground(\gp)$

1748: with $obj\_of(r) = o$ such that $r$ is overridden in $M$

1749: and $\bar X$ is the tuple of arguments appearing in

1750: the head of $r$.

1751: Let $K_3$ be the set of ground literals

1752: $ovr'(L,o)$ such that there exist two rules

1753: $r,r' \in ground(\gp)$ such that

1754: $L \in Head(r)$, $r$ is defeasible and $r'$ overrides

1755: $r$ in $L$.

1756: Let denote by $\cal K$ the collection of sets

1757: of ground literals such that each element

1758: $K \in \cal K$ satisfies the following properties:

1759: \begin{enumerate}

1760: \item

1761: for each literal $\phi(\bar X) \in M$ there is a

1762: literal $\phi'(o,\bar X)$ in $K$, for some object identifier $o$,

1763: \item

1764: for each $r \in G_M(\gp)$ such that the body of $r$ is true in

1765: $M$, for at least one literal $\phi(\bar X)$ of the head of $r$ a

1766: corresponding literal $\phi'(obj\_of(r),\bar X)$ occurs in $K$,

1767: \item

1768: $K \subseteq \{ \phi'(o,\bar X) \ | \ \phi(\bar X) \

1769: \mbox{is an adorned predicate appearing in}\  \gp \wedge o \in {\cal O} \}$,

1770: \item

1771: $K$ is a consistent set of literals.

1772: \end{enumerate}

1773: First observe that

1774: the family $\cal K$ is not empty

1775: (i.e., there is at least a set of consistent sets of literals

1776: satisfying items (1), (2) and (3) above).

1777: This immediately follows from the fact

1778: that $M$ is an answer set of the program $\gp$.

1779: 

1780: Let $M_{K} = K_1 \cup K_2 \cup K_3 \cup K \cup M$,

1781: for a generic $K \in \cal K$. It is easy to

1782: show that $G_{M_{K}}(DLP(\gp))$ is independent on which $K \in

1783: \cal K$ is chosen. Indeed, no literals from $K$ appear in the NAF

1784: part of the rules in $ground(DLP(\gp))$.

1785: 

1786: Now we examine which rules the program

1787: $pos(G_{M_{K}}(DLP(\gp)))$ contains

1788: (for any set $K \in \cal K$).

1789: 

1790: Both the rules with head predicate $prec'$ and $ovr'$ and the rules of

1791: the form $\phi(\bar X) \derives \phi'(X, \bar X)$ (added by

1792: statement 21 of Figure \ref{alg1}) appear unchanged in

1793: $pos(G_{M_K}(DLP(\gp)))$. Indeed, these rules do not contain a NAF

1794: part (recall that the GL transformation can modify only rules in which a

1795: NAF part occurs). Each constraint of $DLP(\gp)$ (added by statement 26

1796: of the algorithm), that is a rule of the form $b \derives \phi(\bar

1797: X), \tneg . \phi(\bar X), \dneg \ b$ (where $b$ is a literal not

1798: occurring in $M_K$) is translated into the rule $b \derives \phi(\bar

1799: X), \tneg . \phi(\bar X)$.

1800: 

1801: The other rules in $pos(G_{M_K}(DLP(\gp)))$ originate from

1802: rules of $ground(DLP(\gp))$ obtained by rewriting rules of

1803: $ground(\gp)$ (see statements 11 and 15 of the algorithm).

1804: 

1805: Thus, consider a rule $r$ of $ground(\gp)$.

1806: 

1807: If $r$ is defeasible and overridden in $M$ then the

1808: corresponding rule in $ground(DLP(\gp))$

1809: (generated by statement 11 of the algorithm) contains a NAF part not

1810: satisfied in $M_K$, by construction of $K_2$ and $K_3$. Hence, such

1811: a rule appears neither in $pos(G_M(\gp))$ nor in $pos(G_{M_K}(DLP(\gp)))$.

1812: 

1813: The other case we have to consider

1814: is that the rule $r$ is either a strict rule

1815: or a defeasible rule not overridden in $M$.

1816: 

1817: First suppose that $r$ is a strict rule or is a defeasible rule

1818: not threatened in $M$ (recall that a rule not threatened in $M$ is

1819: certainly not overridden in $M$).

1820: In this case, the corresponding rule, say $r'$

1821: in $ground(DLP(\gp))$ (generated by

1822: statement 15 of the algorithm)

1823: has the same body of $r$

1824: and the head modified by renaming predicates

1825: (from $\phi$ to $\phi'$) and by adding the object $o$

1826: (from which the rule $r$ comes) as first

1827: argument in each head literal.

1828: Since the body of $r'$ does not contain literals

1829: from $K_1, K_2, K_3$ and $K$,

1830: and further $M \subseteq M_K$ (for each $K \in \cal K$),

1831: $r'$ is eliminated by the GL transformation w.r.t. $M_K$ if and only

1832: if $r$ is eliminated by the GL transformation w.r.t. $M$.

1833: Moreover, in case $r'$ is not eliminated by the GL transformation

1834: w.r.t $M_K$,

1835: since the body of $r'$ does not contain literals

1836: from $K_1, K_2, K_3$ and $K$,

1837: the GL transformation w.r.t. $M_K$ modifies

1838: the body of $r'$ in the same way

1839: the GL transformation w.r.t. $M$ modifies the body

1840: of $r$.

1841: Thus, each rule $r$ in

1842: $pos(G_M(\gp))$ has a corresponding rule in $pos(G_{M_K}(DLP(\gp)))$ with

1843: the same body and a rewritten head.

1844: 

1845: Now suppose that $r$ is a threatened defeasible rule

1846: that is not overridden in $M$.

1847: In this case, the corresponding rule, say $r'$

1848: in $ground(DLP(\gp))$ (generated by

1849: statement 11 of the algorithm)

1850: has the head modified by renaming predicates

1851: (from $\phi$ to $\phi'$) and by adding the object $o$ as first

1852: argument in each head literal

1853: and a body obtained by adding

1854: to the body of $r$ a literal of

1855: the form $\dneg  \ ovr'(r,o, \bar X)$, where

1856: $o$ is the object from which $r$ comes, and $\bar X$

1857: represents the tuple of terms appearing in the

1858: head literals of $r$.

1859: Since the rule $r$ is

1860: not overridden in $M$, the literal $ovr'(r,o, \bar X)$

1861: cannot belong to $K_2$ and hence cannot

1862: belong to $M_K$.

1863: Thus, the GL transformation w.r.t $M_K$ eliminates

1864: the NAF part of the rule $r'$.

1865: As a consequence, also in this case, each rule in

1866: $pos(G_M(\gp))$ has a corresponding rule in $pos(G_{M_K}(DLP(\gp)))$ with

1867: 

1868: Now we prove that, for any $K \in \cal K$,

1869: $M_K$ is a model for

1870: $pos(G_{M_K}(DLP(\gp)))$.

1871: Indeed, rules with head predicate $prec'$

1872: are clearly satisfied.

1873: Further, rules with head predicate $ovr'$

1874: are satisfied by construction of set $K_2$,

1875: $K_3$ and $K$.

1876: Moreover, rules of the form

1877: $\phi(\bar X) \derives \phi'(X, \bar X)$ are

1878: satisfied since $M \subseteq M_K$ and

1879: by construction of $K$.

1880: Rules of $pos(G_{M_K}(DLP(\gp)))$

1881: of the form $b \derives \phi(\bar X), \dneg \ \phi(\bar X)$,

1882: originated by the translation of the constraints,

1883: are satisfied since $M_K$ is a consistent set of literals.

1884: 

1885: Consider now the remaining rules

1886: (those corresponding to rules of $pos(G_M(\gp))$).

1887: Let $r$ be a rule of $pos(G_{M_K}(DLP(\gp)))$

1888: and $r'$ the rule of

1889: $pos(G_M(\gp))$ corresponding to $r$.

1890: As shown earlier, the two rules have

1891: the same body.

1892: Thus, if the body of $r$ is true

1893: w.r.t. $M_K$, the body of $r'$ is

1894: true w.r.t. $M$, since no literal

1895: of $M_K \setminus M$ can appear in the body

1896: of the rule $r'$ (and hence of the rule $r$).

1897: As a consequence, by property (2) of

1898: the collection $\cal K$ to which the

1899: set $K$ belongs, the head of the rule $r$

1900: is true in $M_K$.

1901: 

1902: Thus, $M_K$ is a model

1903: for $pos(G_{M_K}(DLP(\gp)))$.

1904: 

1905: Now we prove the following claim:

1906: 

1907: {\bf Claim 1.} Let $\bar M$ be a model for $pos(G_{M_K}(DLP(\gp)))$.

1908: Then, $\pi(\bar M)$ is a model for

1909: $pos(G_{M}(\gp))$.

1910: 

1911: \begin{proof}

1912: By contradiction suppose that $\pi(\bar M)$ is not a model

1913: for  $pos(G_{M}(\gp))$. Thus, there exists a rule $r \in  pos(G_{M}(\gp))$

1914: with body true in $\pi(\bar M)$ and head false in $\pi(\bar M)$.

1915: Since, as shown earlier, the rule $r$ has a corresponding

1916: rule $r'$ in  $pos(G_{M_K}(DLP(\gp)))$ with the same body

1917: of $r$ and the head obtained by replacing each literal

1918: $\phi(\bar X)$ of the head of $r$ by the corresponding literal

1919: $\phi'(o,\bar X)$, where $o$ is the object from which $r$ comes.

1920: Since  $\pi(\bar M)$ is a model for $pos(G_{M_K}(DLP(\gp)))$,

1921: at least one of the "$\phi'$ literal"  of the head of $r'$ must be

1922: true in $\pi(\bar M)$. Then, due to the presence

1923: of the rules of the form $\phi(\bar X) \derives \phi'(X, \bar X)$ in

1924: $pos(G_{M_K}(DLP(\gp)))$,  $\pi(\bar M)$ must contain also the "$\phi$

1925: corresponding literal" belonging to the head of $r$ (contradiction)

1926: \end{proof}

1927: 

1928: Moreover we  prove that each model

1929: for $pos(G_{M_K}(DLP(\gp)))$

1930: \begin{description}

1931: \item(1)

1932: contains $M$, and

1933: \item(2)

1934: belongs to $\cal K$.

1935: \end{description}

1936: To prove item (1), suppose by contradiction $\bar M$ is

1937: a model for $pos(G_{M_K}(DLP(\gp)))$ such that

1938: $M \cap \bar M \neq M$.

1939: Thus, $\pi(\bar M) \subset M$.

1940: On the other hand, by Claim 1, $\pi(\bar M)$

1941: is a model for $pos(G_M(\gp))$.

1942: But since $M$ is an answer set for $\gp$

1943: and then a minimal model for

1944: $pos(G_M(\gp))$, a contradiction arises.

1945: 

1946: Now we have to prove the item (2) above. 

1947: First observe that

1948: the properties 3. and 4. of the family $\cal K$ are trivially verified

1949: by the models of $pos(G_{M_K}(DLP(\gp)))$.

1950: Thus, by contradiction suppose there exists a model

1951: $\bar M$ of $pos(G_{M_K}(DLP(\gp)))$

1952: such that it does not satisfy

1953: one of the properties 1. or 2. characterizing the family $\cal K$. 

1954: 

1955: First suppose that property 1. is not satisfied by $\bar M$, that is,

1956: there is a literal $\phi (\bar X)$ in $M$ such that no

1957: corresponding literal $\phi'(o, \bar X)$ occurs in $\bar M$, for

1958: some object identifier $o$. Let $\bar M'$ be the set obtained by

1959: $\bar M$ by eliminating all such literals $\phi(\bar X)$. It is

1960: easy to see that $\bar M'$ is still a model for

1961: $pos(G_{M_K}(DLP(\gp)))$. Indeed, rules of the form $\phi(\bar X)

1962: \derives \phi'(X, \bar X)$ are satisfied since literals $\phi(\bar

1963: X)$ dropped from $\bar M$ do not have corresponding "$\phi'$

1964: literals" by hypothesis. Further, no other rule in

1965: $pos(G_{M_K}(DLP(\gp)))$ contains a literal from $M$ in the head.

1966: On the other hand, by Claim 1, $\pi(M')$ is a model

1967: for $pos(G_M(\gp))$. But this is a contradiction,

1968: since $\pi(M') \subset M$ and $M$ is an answer set for $\gp$.

1969: 

1970: 

1971: Suppose now that property 2. is not satisfied by $\bar M$,

1972: that is, there is a rule $r \in pos(G_M(\gp))$ such

1973: that the body of $r$ is true in $M$ and

1974: no "$\phi'$ literals"  corresponding

1975: to literals of the head occur in $\bar M$.

1976: Since, $M \subseteq \bar M$ (see item (1) above), the corresponding

1977: rule of $pos(G_{M_K}(DLP(\gp)))$ is not satisfied.

1978: But this implies that $\bar M$ can not be a model

1979: for $pos(G_{M_K}(DLP(\gp)))$ (contradiction).

1980: 

1981: A consequence of the fact that every model of

1982: $pos(G_{M_K}(DLP(\gp)))$ contains $M$ is that

1983: every model of $pos(G_{M_K}(DLP(\gp)))$ must

1984: contain the sets $K_1$, $K_2$ and $K_3$.

1985: because of the rules added by statements

1986: 1,5 and 12 of the algorithm.

1987: 

1988: Thus, the model

1989: $M'=M_{K'}$ for $K' \in \cal K$ such

1990: that no set

1991: $\bar K \in \cal K$ exists

1992: such that $\bar K \subset K'$

1993: is a minimal model for

1994: $pos(G_{M_K}(DLP(\gp))$, that is,

1995: a consistent answer set for $DLP(\gp)$.

1996: Hence,

1997: the first part of the proof is concluded, since

1998: $\pi(M') = M$.

1999: 

2000: 

2001: 

2002: 

2003: Now, we prove that

2004: given a consistent answer set $M'$ for $DLP(\gp)$,

2005: $M = \pi(M')$ is an answer set for $\gp$.

2006: 

2007: First we prove that a literal $\phi(\bar X)$ belongs

2008: to $M$ if and only if

2009: there exits a literal $\phi'(o, \bar X)$ in

2010: $M'$, for some object identifier $o$.

2011: 

2012: Indeed, $\phi(\bar X) \in M$ implies that

2013: $\phi(\bar X) \in M'$. But since $M'$ is a minimal model

2014: for $pos(G_{M'}(DLP(\gp))$, there must exits a rule in

2015: $pos(G_{M'}(DLP(\gp))$ with head

2016: containing the literal $\phi(\bar X)$ and body

2017: true w.r.t. $M'$ (otherwise the literal

2018: $\phi(\bar X)$ could be dropped from

2019: $M'$ without invalidate any rule of

2020: $pos(G_{M'}(DLP(\gp))$ and thus $M'$ would not

2021: be minimal).

2022: Conversely, if $\phi'(o, \bar X) \in M'$, 

2023: for some object identifier $o$, the literal

2024: $\phi(\bar X)$ belongs to $M'$, since $M'$

2025: is a model for $pos(G_{M'}(DLP(\gp))$

2026: and the rule $\phi(\bar X) \derives \phi'(o, \bar X)$ belongs

2027: to $pos(G_{M'}(DLP(\gp))$.

2028: Thus,  $\phi(\bar X) \in M$.

2029: 

2030: Moreover, we prove that every rule of

2031: $pos(G_{M'}(DLP(\gp))$ has a corresponding

2032: rule in $pos(G_M(\gp))$ with same body

2033: and a head obtained by replacing the $\phi'$

2034: literals with the $\phi$ corresponding ones

2035: and by eliminating the object argument

2036: from these literals.

2037: Indeed, from the above result, the GL transformation

2038: deletes a rule $r$ from $ground(DLP(\gp))$ if either

2039: the corresponding rule belonging to $ground(\gp)$

2040: is overridden in $M$ (due the the literal

2041: $\dneg  \ ovr'(r,o,\bar X)$ occurring in the body of $r$)

2042: or some negated (by negation $\dneg$) literal is

2043: false in $M'$. But this literal is false in

2044: $M'$ if and only if it is false in $M$.

2045: On the other hand, in case the rule is not

2046: deleted by the GL transformation, its body

2047: is rewritten in the same way of the corresponding

2048: rule appearing in $pos(G_M(\gp))$.

2049: 

2050: As a consequence, $M$ is a model for $pos(G_{M}(\gp))$.

2051: Indeed, if the body of a rule $r$ of

2052: $pos(G_{M}(\gp))$ is true w.r.t. $M$, the corresponding

2053: rule $r'$ of  $pos(G_{M'}(DLP(\gp))$ has the body true

2054: w.r.t. $M'$. Hence, at least one of the head literals

2055: of $r'$ must be true in $M'$.

2056: Let $\phi'(o, \bar X)$ such a literal.

2057: As shown earlier, this implies that $\phi(\bar X)$

2058: belongs to $M$.

2059: But $\phi(\bar X)$ appears in the head of $r$

2060: and hence $r$ is satisfied in $M$.

2061: 

2062: Now we prove that $M$ is minimal.

2063: By contradiction, suppose that $\bar M \subset M$ is

2064: a model for $pos(G_{M}(\gp))$.

2065: Consider the literals belonging to the set

2066: $M  \setminus \bar M$. Because

2067: of the correspondence between the rules

2068: of $pos(G_{M}(\gp))$ and the rules

2069: of $pos(G_{M'}(DLP(\gp))$, the set of literals

2070: obtained from $M'$ by eliminating

2071: all the literals $\phi(\bar X)$ belonging

2072: to the set $M \setminus \bar M$ as well as

2073: the corresponding $\phi'$ literals

2074: is still a model for $pos(G_{M'}(DLP(\gp))$.

2075: But this is a contradiction,

2076: since $M'$ is a consistent answer set for

2077: $DLP(\gp)$.

2078: 

2079: Since $M$ is a model for  $pos(G_{M}(\gp))$

2080: and is minimal, $M = \pi(M')$ is an answer set

2081: for the program $\gp$. Hence the proof is concluded.

2082: \end{proof}

2083: 

2084: \begin{example}\label{ex-equivalence}

2085: {

2086: Consider the program $\gp$ of Example \ref{ex-1}.

2087: It is easy to see that

2088: $DLP(\gp)$ (see Example \ref{ex-translation}) admits

2089: one consistent answer set

2090: $M = \{prec'(o_2,o_1), a'(o_1), e'(o_1),$

2091: $b'(o_2),$ $c'(o_2),$ $ovr'(\tneg b,o_1),$ $a,$ $e,$ $b,$ $c \}$.

2092: Thus, $\pi(M) = \{a,b,c,e\}$.

2093: On the other hand,

2094: $\pi(M)$ is the only answer

2095: set for $\gp$,

2096: as shown in Example \ref{ex-4}.

2097: }

2098: $\punto$

2099: \end{example}

2100: 

2101: \subsection{System Architecture}

2102: 

2103: We have used the \dlv system \cite{eite-etal-98a} to implement a system

2104: for $\DLPI$. The concept is that of a front-end to plain DLP, which

2105: has been used before for implementing various ways of reasoning modes

2106: and languages on top of the \dlv system. The front-end implements the

2107: translation described in Section~\ref{sec:implementation}. A schematic

2108: visualization of its architecture is shown in Figure

2109: \ref{architecture}.

2110: 

2111: \begin{figure}%[th]

2112: \epsfig{file=arch.eps,width=\textwidth}

2113: \caption{Flow diagram of the system.}

2114: \label{architecture}

2115: \end{figure}

2116: 

2117: First of all, we have extended the \dlv parser to incorporate the

2118: $\DLPI$ syntax. In this way, all the advanced features of \dlv

2119: (e.g.\ bounded integer arithmetics, comparison built-ins, etc.) are also

2120: available with $\DLPI$.

2121: The {\em Rewriter} module implements the translation depicted

2122: in Figure \ref{alg1}.

2123: Once the rewritten version $\pi(\gp )$ of $\gp$ is generated,

2124: its answer sets

2125: are then computed using the \dlv core. Before the output is

2126: shown to the user, $\pi$ is applied to each answer set in order to strip the

2127: internal predicates from the output.

2128: 

2129: On the webpage \cite{dlvi-web} the system is described in detail. It

2130: has been fully incorporated into the \dlv system. To use it, just

2131: supply an input file using the syntax described in

2132: Section~\ref{syntax} --- \dlv automatically invokes the $\DLPI$

2133: frontend in this case.

2134: 

2135: Note that it is currently required to specify the objects in the order

2136: of the inheritance hierarchy: Specifying that some object inherits

2137: from another object which has not been defined before will result in

2138: an error. Since cyclic dependencies are not allowed in our language,

2139: this requirement is not a restriction.

2140: 

2141: \section{Conclusion}\label{sec:conclusion}

2142: 

2143: We have presented a new language, named $\DLPI$,

2144: resulting from the extension of (function-free)

2145: disjunctive logic programming with inheritance.

2146: $\DLPI$ comes with a declarative model-theoretic semantics,

2147: where possible conflicts are solved in favor of more specific

2148: rules (according to the inheritance hierarchy).

2149: $\DLPI$ is a consistent generalization of the Answer Set Semantics

2150: of disjunctive logic programs, it respects some fundamental

2151: inheritance principles, and it seems to be suitable

2152: also to give a semantics to updates in logic programs. 

2153: 

2154: While inheritance enhances the knowledge representation

2155: modeling features of disjunctive logic programming,

2156: the addition of inheritance does not increase

2157: its computational complexity.

2158: Thus, inheritance ``comes for free'': the user can

2159: take profit of its knowledge modeling ability,

2160: without paying any extra cost in terms of computational load.

2161: It was therefore possible to implement a $\DLPI$ system

2162: on top of the disjunctive logic programming system \dlv.

2163: The system is freely available on the web \cite{dlvi-web} and ready-to-use

2164: for experimenting with the use of inheritance in KR applications.

2165: 

2166: 

2167: \section*{Acknowledgements}

2168: 

2169: The idea of representing inertia in planning problems in a higher

2170: object is due to Axel Polleres. The introduction of the notion of

2171: strict rules was suggested by Michael Gelfond. This work was

2172: partially supported by FWF (Austrian Science Funds) under the

2173: projects \mbox{P11580-MAT} and \mbox{Z29-INF}.

2174: 

2175: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

2176: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

2177: 

2178: 

2179: \bibliography{bibtex}

2180: \end{document}

2181: