1: %% Searched string: {}

2: \typeout{}

3: \typeout{The complexity of redundancy}

4: \typeout{}

5: 

6: \def\style{0}	% 

7: 

8: \documentclass[12pt]{article}

9: 

10: \usepackage{latexsym}

11: % usepackage{proof}

12: 

13: %%%%%%%%%%%%% macros %%%%%%%%%%%%%%

14: %%%%%%%%%%%%%%%%%%%%%%%%%% Miscellaneous

15: 

16: \long\def\nop#1{}

17: \long\def\nota#1{\marginpar{\tiny #1}}

18: 

19: \def\separator{\vskip 0.5cm \hrule \vskip 0.5cm}

20: 

21: \hyphenation{Ca-do-li Do-ni-ni Li-be-ra-to-re}

22: 

23: 

24: % se \shortcite non e' definito, lo definisce come \cite

25: 

26: \expandafter\ifx\csname shortcite\endcsname\relax

27: \let\shortcite=\cite

28: \fi

29: 

30: 

31: % framebox

32: 

33: \newbox\current

34: 

35: \long\def\plframebox#1{

36: \setbox\current\vbox{#1}		% set box

37: 

38: \vbox to \ht\current {\hrule\vss

39: \hbox to \wd\current {%

40: \vrule \hss\box\current\hss \vrule}

41: \vss\hrule }

42: }

43: 

44: % \hrule width\wd\current

45: % \vrule height\ht\current

46: 

47: 

48: % mangia i par

49: 

50: \long\def\eatpar#1{%

51: \ifx#1\par                      % se il token e' \par

52: \let\nextmove=\eatpar           % rimetti \eatpar in coda

53: \else

54: \let\nextmove=#1%               altrimenti, rimetti il token in coda

55: \fi

56: \noexpand\nextmove%             il token o \eatpar viene rimesso in coda

57: }

58: 

59: 

60: % modifica i margini

61: 

62: \def\modifymargins#1#2{

63: \newdimen\addtoh

64: \newdimen\addtow

65: \addtoh=#1

66: \addtow=#2

67: 

68: \advance\topmargin by -\addtoh

69: \multiply\addtoh by 2

70: \advance\textheight by \addtoh

71: 

72: \advance\oddsidemargin by -\addtow

73: \advance\evensidemargin by -\addtow

74: \multiply\addtow by 2

75: \advance\textwidth by \addtow

76: }

77: 

78: 

79: % tilde per gli indirizzi www

80: 

81: \begingroup

82: \catcode`\~=11

83: \gdef\centertilde#1{\lower #1pt\hbox{~}}

84: \endgroup

85: 

86: 

87: % ora corrente

88: 

89: \newcount\currenttime

90: \newcount\hour

91: \newcount\minute

92: 

93: \def\printtime{%

94: \currenttime=\time

95: \hour=\currenttime

96: \divide\hour by 60

97: \minute=-\hour

98: \multiply\minute by 60

99: \advance\minute by \currenttime

100: \the\hour:\ifnum\minute<10 0\fi\the\minute

101: }

102: 

103: 

104: % mette l'ora nella data che appare sotto il titolo

105: 

106: \begingroup

107: \makeatletter

108: \global\let\@@date=\@date

109: \gdef\@date{\@@date\ --- \printtime}

110: \endgroup

111: 

112: 

113: % oggi

114: 

115: \def\oggi{\number\day\space 

116: \ifcase\month\or

117: Gennaio\or Febbraio\or Marzo\or Aprile\or Maggio\or Giugno\or

118: Luglio\or Agosto\or Settembre\or Ottobre\or Novembre\or Dicembre\fi

119: \space \number\year}

120: 

121: 

122: % riga vuota

123: 

124: \def\riga{\vskip 1\baselineskip \noindent}

125: 

126: \newcounter{rmexample}

127: 

128: \newenvironment{rmexample}

129: {\addtocounter{rmexample}{1}

130: \medskip

131: \noindent{\bf Example~\thermexample}:}{\ifhmode\nobreak{\raisebox{-.2ex}{$\Diamond$}}\par\fi\smallskip}

132: 

133: \def\proof{\noindent {\sl Proof.\ \ }}

134: \def\proofsketch{{\sl Proof (sketch).\ \ }}

135: \def\proofof#1{{\sl Proof of #1.}}

136: 

137: \def\qed{\hfill{\boxit{}}

138:   \ifdim\lastskip<\medskipamount \removelastskip\penalty55\medskip\fi}

139: \def\qedn#1{\hfill{\boxit{}$_#1$}

140:   \ifdim\lastskip<\medskipamount \removelastskip\penalty55\medskip\fi}

141: \long\def\boxit#1{\vbox{\hrule\hbox{\vrule\kern3pt

142:                   \vbox{\kern3pt#1\kern3pt}\kern3pt\vrule}\hrule}}

143: 

144: \def\ovl#1{\overline{#1}}

145: 

146: 

147: %%%%%%%%%%%%%%%%%%%%%%%%%% General Math

148: 

149: \def\calA{{\cal A}} \def\B{{\cal B}} \def\D{{\cal D}}

150: \def\E{{\cal E}} \def\F{{\cal F}} \def\G{{\cal G}} \def\H{{\cal H}}

151: \def\I{{\cal I}} \def\J{{\cal J}} \def\K{{\cal K}} \def\L{{\cal L}}

152: \def\M{{\cal M}} \def\N{{\cal N}} \def\O{{\cal O}} \def\calP{{\cal P}}

153: \def\Q{{\cal Q}} \def\R{{\cal R}} \def\calS{{\cal S}} \def\T{{\cal T}}

154: \def\U{{\cal U}} \def\V{{\cal V}} \def\W{{\cal W}} \def\X{{\cal X}}

155: \def\Y{{\cal Y}} \def\Z{{\cal Z}}

156: 

157: %%%%%%%%%%%%%%%%%%%%%%%%%% Abbreviations

158: 

159: \def\eset{\emptyset}

160: \def\col{\colon}

161: \def\ol#1{\overline{#1}}                % overline

162: \def\ul#1{\underline{#1}}               % underline

163: \def\uls#1{\underline{\raisebox{0pt}[0pt][0.45ex]{}#1}} % underline with space

164: \def\iff{if and only if}

165: \def\kb{k.b.}

166: \def\ie{i.e.}

167: \def\eg{e.g.}

168: \def\wrt{w.r.t.}

169: \def\aka{a.k.a.}

170: %\def\wlog{w.l.o.g.}

171: 

172: %%%%%%%%%%%%%%%%%%%%%%%%%% Relations

173: 

174: \def\incl{\subseteq}

175: \def\imp{\Rightarrow}

176: \def\imply{\rightarrow}

177: \def\deq{\doteq}

178: \def\defas{\doteq}                      % defined as

179: \def\dleq{\dot{\leq}}                   % dotted less equal

180: \def\finimpl{\models_{fin}}             % finitely implies

181: \def\subsumed{\sqsubseteq}              % subsumed by

182: 

183: %%%%%%%%%%%%%%%%%%%%%%%%%% Minimal Sets

184: 

185: \def\setdiff{\Delta}

186: \def\mindiff{\delta}    %  proposta; si accettano simboli migliori

187: \def\minTdiff{\mu}      %  idem

188: \def\minset{min_\subseteq}  %% come Eiter, Gottlob 92

189: \def\M{{\cal M}}

190: \def\F{{\cal F}}

191: \def\form{form}

192: \def\card#1{card(#1) }

193: 

194: %%%%%%%%%%%%%%%%%%%%%%%%%% Spaces

195: 

196: \def\asp{\makebox[3pt]{}}       % arrow space, put before and after arrows

197: \def\osp{\hskip1pt}             % operator space, put before and after ops

198: \def\asps#1{{\asp#1\asp}}

199: \def\osps#1{{\osp{#1}\osp}}

200: \def\qland{\;\;\land\;\;}

201: 

202: \def\con{\asp\asp\&\asp}

203: % Incompatibile con LaTex2e

204: % \def\sbox{\vbox{\hrule

205: %                \hbox{\vrule\hskip4pt\vbox{\vskip4pt}\vrule}

206: %                \hrule}}

207: 

208: \def\per{\mbox{\bf .}}                  % period

209: 

210: \def\cld{,\ldots,}                      % ,...,

211: \def\ld#1{#1 \ldots #1}                 % #1 ... #1

212: \def\cd#1{#1 \cdots #1}                 % #1 ... #1

213: \def\lds#1{\, #1 \; \ldots \; #1 \,}    % _#1_..._#1_

214: \def\cds#1{\, #1 \; \cdots \; #1 \,}    % _#1_..._#1_

215: \def\dd#1#2{#1_1,\ldots,#1_{#2}}        % da da, makes x1,...,xn

216: 

217: %%%%%%%%%%%%%%%%%%%%%%%%%% Delimiters

218: 

219: \def\quotes#1{{\lq\lq#1\rq\rq}}         % quote

220: \def\braces#1{$\{$ #1 $\}}              % braces

221: \def\set#1{\{#1\}}                      % set

222: \def\Set#1{\left\{ #1 \right\}}

223: \def\bigset#1{ \Bigl\{ #1 \Bigr\} }

224: \def\bigmid{\ \Big|\ }                  % mid

225: \def\card#1{|{#1}|}                     % cardinality of a set

226: \def\Card#1{\left| #1 \right|}

227: \def\cards#1{\sharp #1}

228: \def\sub#1{[#1]}                        % [ #1 ]

229: \def\tup#1{\langle #1 \rangle}          % tuple < #1 >

230: \def\Tup#1{\left\langle #1 \right\rangle}

231: \def\l{\langle}

232: \def\r{\rangle}

233: \newcommand{\pair}[2]{\langle #1, #2 \rangle}

234: 

235: \def\If{\lq\lq$\Leftarrow$\rq\rq\ \ }           % 1st direction of iff-proof

236: \def\OnlyIf{\lq\lq$\Rightarrow$\rq\rq\ \ }      % 2nd direction of iff-proof

237: 

238: %%%%%%%%%%%%%%%%%%%%%%%%%% Constraints

239: 

240: \def\relc#1#2#3{#1#2#3}

241: %\def\inc#1#2{#1 \!:#2}

242: \def\inc#1#2{#1\col#2}

243: 

244: %%%%%%%%%%%%%%%%%%%%%%%%%% General Commands

245: 

246: 

247: 

248: %%%%%%%%%%%%%%%%%%%%%%%%%% Programs

249: 

250: \def\pwhile{{\tt while ~}}

251: \def\pfor{{\tt for ~}}

252: \def\pforeach{{\tt foreach ~}}

253: \def\pto{{\tt ~ to ~}}

254: \def\pdo{{\tt ~ do ~ }}

255: 

256: \def\pif{{\tt if ~ }}

257: \def\pthen{{\tt ~ then ~ }}

258: \def\pelse{{\tt ~ else ~ }}

259: \def\por{{\tt ~ or ~ }}

260: \def\pand{{\tt ~ and ~ }}

261: 

262: \def\pbegin{{\tt begin}}

263: \def\pend{{\tt end}}

264: 

265: \def\pret{{\tt return ~}}

266: \def\ptrue{{\tt true}}

267: \def\pfalse{{\tt false}}

268: 

269: \def\pind{~~~}

270: 

271: %%%%%%%%%%%%%%%%%%%%%%%%%% Interpretation

272: 

273: \def\mod{M\!od}

274: \def\form{F\!orm}

275: \def\var{V\!ar}

276: \def\diff{Di\!f\!f}

277: \def\dist{\mbox{{\sc dist}}}

278: 

279: %%%%%%%%%%%%%%%%%%%%%%%%%% Concept forming operators

280: 

281: \def\OR{\sqcup}

282: \def\NOT{\neg}

283: \def\ALL#1#2{\forall #1 \per #2}

284: \def\SOME#1#2{\exists #1 \per #2}

285: \def\SOMET#1{\exists #1}

286: \def\ALLRC{\ALL R C}

287: \def\SOMERC{\SOME R C}

288: \def\SOMERT{\SOMET R}

289: \def\ATLEAST#1#2{(\geq #1 \, #2)}

290: \def\ATMOST#1#2{(\leq #1 \, #2)}

291: \def\EXACTLY#1#2{(= #1 \, #2)}

292: \def\INV#1{#1^{-1}}

293: 

294: \def\Atmost#1#2{A_{(\leq #1 \, #2)}}

295: \def\Atleast#1#2{A_{(\geq #1 \, #2)}}

296: 

297: %%%%%%%%%%%%%%%%%%%%%%%%%% PDL forming operators

298: 

299: \def\true{{\sf true}}

300: \def\false{{\sf false}}

301: \def\Not{\neg}

302: \def\Or{\vee}

303: \def\Implies{\rightarrow}

304: \def\Diam#1#2{\langle #1 \rangle #2}

305: \def\DiamT#1{\langle #1 \rangle \true}

306: \def\Boxx#1#2{[#1]#2}

307: \def\Inv#1{#1^{-}}

308: \def\Star#1{#1^{\ast}}

309: \def\Comp{;}

310: \def\Choice{\cup}

311: 

312: \def\AllR{\Star{(\cup_i R_i)}}

313: 

314: %%%%%%%%%%%%%%%%%%%%%%%%%% Complexity Classes

315: 

316: \def\C{{\rm C}}

317: \def\nc{{\rm NC}}

318: \def\p{{\rm P}}

319: \def\np{{\rm NP}}

320: \def\conp{{\rm coNP}}

321: \def\Dp{${\rm D}^p$}

322: \def\S#1{\mbox{$\Sigma^p_{#1}$}}

323: \def\P#1{$\Pi^p_{#1}$}

324: \def\D#1{\mbox{$\Delta^p_{#1}$}}

325: \def\Dlog#1{\mbox{$\Delta^p_{#1}[\log n]$}}

326: \def\PH{{\rm PH}}

327: \def\poly{{\rm poly}}

328: \def\pp{{\rm PP}}

329: \def\copp{{\rm co\pp}}

330: \def\nppp{$\np^\pp$}

331: 

332: \def\FC{\mbox{\rm FC}}

333: \def\leqFC{\leq^{\rm FC}}

334: 

335: \def\pspace{{\rm PSPACE}}

336: \def\logspace{{\rm LOGSPACE}}

337: \def\exptime{\mbox{\rm EXPTIME}}

338: 

339: %%%%%%%%%%%%%%%%%%%%%%%%%% Compilability Classes

340: 

341: \def\c{$\leadsto$}

342: 

343: \def\cC{\c{\rm C}}

344: \def\cp{\c{\rm P}}

345: \def\cnp{{\rm compNP}}

346: \def\cconp{{\rm compcoNP}}

347: \def\cDp{${\rm compD}^p$}

348: \def\cS#1{comp$\Sigma^p_#1$}

349: \def\cP#1{comp$\Pi^p_#1$}

350: \def\cD#1{comp$\Delta^p_#1$}

351: \def\cDlog#1{comp$\Delta^p_#1[\log n]$}

352: 

353: \def\cpspace{{\rm compPSPACE}}

354: \def\clogspace{{\rm compLOGSPACE}}

355: 

356: \def\nuc#1{\mbox{$\parallel\!\leadsto$#1}}

357: 

358: \def\nucC{\nuc{\rm C}}

359: \def\nucp{\nuc{\rm P}}

360: \def\nucnp{\nuc{\rm NP}}

361: \def\nucconp{\nuc{\rm coNP}}

362: \def\nucS#1{\nuc{$\Sigma^p_{#1}$}}

363: \def\nucP#1{\nuc{$\Pi^p_{#1}$}}

364: \def\nucD#1{\nuc{\D{#1}}}

365: \def\nucDp{{\rm nucomp}\Dp}

366: \def\nucDlog#1{{\rm nucomp}\Dlog{#1}}

367: 

368: \def\comp{\leq_{comp}}

369: \def\nucomp{\leq_{nucomp}}

370: 

371: \def\ep#1{*#1}

372: 

373: %%%%%%%%%%%%%%%%%%%%%%%%%% FPT Classes

374: 

375: \def\fpt{\mbox{\rm FPT}}

376: \def\ufpt{\mbox{\rm uFPT}}

377: \def\sufpt{\mbox{\rm suFPT}}

378: \def\nufpt{\mbox{\rm nuFPT}}

379: 

380: %%%%%%%%%%%%%%%%%%%%%%%%%% Succinctness Classes	

381: 

382: \def\mC{{\rm model-C}}

383: \def\tC{{\rm thm-C}}

384: 

385: \def\mC{{\rm model-C}}                 % Model checking e' C

386: \def\mP{{\rm model-P}}                 % Model checking e' P

387: \def\mNP{{\rm model-NP}}               % Model checking e' NP

388: \def\mcoNP{{\rm model-coNP}}           % Model checking e' coNP

389: \def\mS#1{{\rm model-}$\Sigma^p_{#1}$}

390: \def\mPi#1{{\rm model-}$\Pi^p_{#1}$}

391: 

392: \def\tC{{\rm thm-C}}                 % Inference e' C

393: \def\tP{{\rm thm-P}}                 % Inference e' P

394: \def\tNP{{\rm thm-NP}}               % Inference e' NP

395: \def\tcoNP{{\rm thm-coNP}}           % Inference e' coNP

396: \def\tS#1{{\rm thm-}$\Sigma^p_{#1}$}

397: \def\tPi#1{{\rm thm-}$\Pi^p_{#1}$}

398: 

399: 

400: \def\diventa{\mapsto} 

401: 

402: 

403: %%%%%%%%%%%%%%%%%%%%%%%%%% Problems

404: 

405: \def\profont{\sf}

406: 

407: \def\sat{{\profont sat}}

408: \def\unsat{{\profont unsat}}

409: \def\qbf{{\rm QBF}}

410: \def\maxlexmod{{\profont maxlexmod}}

411: \def\minlexmod{{\profont minlexmod}}

412: \def\infncirc{{\profont infncirc}}

413: \def\critsat{{\profont critsat}}

414: \def\threesat{{\profont 3sat}}

415: \def\threeunsat{{\profont 3unsat}}

416: \def\threecolor{{\profont 3colorability}}

417: \def\clique{{\profont clique}}

418: \def\vc{{\profont vc}}

419: \def\gi{{\profont gi}}

420: \def\sgi{{\profont sgi}}

421: \def\hc{{\profont hc}}

422: \def\shc{{\profont shc}}

423: \def\md{{\profont md}}

424: \def\cq{{\profont cq}}

425: \def\rp{{\profont rp}}

426: \def\nf{{\profont nf}}

427: \def\st{{\profont st}}

428: \def\ec{{\profont ec}}

429: \def\x3c{{\profont x3c}}

430: \def\threecnf{{\profont 3cnf}}

431: \def\ci{{\profont ci}}

432: \def\mmc{{\profont mmc}}

433: \def\finf{{\profont fi}}

434: \def\epssat{$\epsilon$\threesat}

435: \def\diagn{{\profont diagn}}

436: \def\strips{{\profont STRIPS}}

437: \def\ibr{{\profont ibr}}

438: \def\mbt{{\profont mbt}}

439: \def\irr{{\profont irr}}

440: 

441: 

442: %%%%%%%%%%%%%%%%%%%%%%%%%% Theorems

443: 

444: \def\possnewtheorem#1#2{

445: \expandafter\ifx\csname #1\endcsname\relax

446: \newtheorem{#1}{#2}

447: \fi

448: }

449: 

450: \def\possnewtheoremthree#1[#2]#3{

451: \expandafter\ifx\csname #1\endcsname\relax

452: \newtheorem{#1}[#2]{#3}

453: \fi

454: }

455: 

456: \possnewtheorem{theorem}{Theorem}

457: \possnewtheorem{corollary}{Corollary}

458: \possnewtheorem{lemma}{Lemma}

459: \possnewtheoremthree{proposition}[theorem]{Proposition}

460: \possnewtheorem{definition}{Definition}

461: \possnewtheorem{question}{Question}

462: \possnewtheorem{example}{Example}

463: \possnewtheorem{property}{Property}

464: \possnewtheorem{assumption}{Assumption}

465: \possnewtheorem{conjecture}{Conjecture}

466: \newenvironment{theorem*}[1]{{\noindent \bf Theorem~#1}\begin{it}}{\end{it}\

467: 

468: }

469: 

470: %%%%%%%%%%%%%%%%%%%%%%%%%% Revision & Update

471: 

472: \def\agm#1{{\sc agm#1}}

473: \def\km#1{{\sc km#1}}

474: \def\leh#1{{\sc leh#1}}

475: 

476: \def\ginsberg{*_G}

477: \def\fuv{*_{FUV}}

478: \def\satoh{*_S}

479: \def\dalal{*_D}

480: \def\winslett{*_W}

481: \def\borgida{*_B}

482: \def\forbus{*_F}

483: \def\ssu{*_{SSU}}

484: \def\weber{*_{W\!eb}}

485: \def\hegner{*_{H}}

486: \def\widtio{*_{Wit}}

487: \def\revesz{*_{R}}

488: \def\up{*_{UP}}

489: \def\fm{*_{FM}}

490: 

491: \let\texcirc=\circ

492: \def\circ{C\!I\!RC}

493: \def\ncirc{\mbox{{\sc ncirc}}}

494: \newcommand{\deftheory}[2]{\langle #1, #2 \rangle}

495: % Comando per un default PF normale

496: \def\defaultone#1{\frac{~:#1}{#1}}

497: % Comando per un default normale

498: \def\defaulttwo#1#2{\frac{#1:#2}{#2}}

499: % Comando per un default qualsiasi

500: \def\defaultthree#1#2#3{\frac{#1:#2}{#3}}

501: \def\anr{*_{ANR}}

502: \def\nat{*_{NR}}

503: \def\ocf{{\sc ocf}}

504: \def\cond{*_{CT}}

505: \def\adj{*_{AT}}

506: \def\rr#1{*_{RR(#1)}}

507: \def\pr#1{*_{PR(#1)}}

508: 

509: \def\ranking#1{\kappa_{[T;P_1,\ldots,P_{#1}]}}

510: 

511: %%%%%%%%%%%%%%%%%%%%%%%%%% RAA

512: 

513: \def\A{$\cal{A}$}

514: 

515: \def\init#1{~{\sf initially}~#1}

516: \def\after#1#2{#1~{\sf after}~#2}

517: \def\causes#1#2{#1~{\sf causes}~#2}

518: \def\causesif#1#2#3{#1~{\sf causes}~#2~{\sf if}~#3}

519: 

520: %%%%%%%%%%%%%%%%%%%%%%%%%%

521: 

522: %\def\SetFigFont#1#2#3{}

523: 

524: 

525: 

526: \def\qequiv#1{\stackrel{#1}{\equiv}}

527: 

528: \long\def\ies#1{I.E.S.%

529: \if.#1%

530: \else

531: #1%

532: \fi}

533: % \def\iess{\stackrel{ies}{\subseteq}}

534: 

535: \long\def\comment#1\endcomment{\vskip\baselineskip

536: {\tt

537: 

538: #1

539: }\vskip\baselineskip}

540: 

541: \long\def\comment#1\endcomment{}

542: 

543: \title{Redundancy in Logic I:\\

544: CNF Propositional Formulae}

545: \author{Paolo Liberatore%

546: \thanks{

547: Dipartimento di Informatica e Sistemistica,

548: Universit\`a di Roma ``La Sapienza'',

549: via Salaria 113, 00198, Rome, Italy.}

550: }

551: 

552: \begin{document}

553: 

554: \maketitle

555: 

556: %%%%%%%%%%%%% abstract %%%%%%%%%%%%%%

557: \begin{abstract}

558: 

559: A knowledge base is redundant if it contains parts that

560: can be inferred from the rest of it. We study the problem

561: of checking whether a CNF formula (a set of clauses) is

562: redundant, that is, it contains clauses that can be derived

563: from the other ones. Any CNF formula can be made irredundant

564: by deleting some of its clauses: what

565: results is an  irredundant equivalent subset (I.E.S.) We

566: study the complexity of some related problems: verification,

567: checking existence of a I.E.S.\  with a given size, checking

568: necessary and possible presence of clauses in I.E.S.'s, and

569: uniqueness. We also consider the problem of redundancy

570: with different definitions of equivalence.

571: 

572: \end{abstract}

573: 

574: 

575: \

576: 

577: \noindent {\bf Keywords:} propositional logic,

578: redundancy, formula minimization, computational complexity.

579: 

580: \

581: 

582: \noindent {\bf Note:} this paper is an extended and

583: revised version of the paper ``The Complexity of

584: Checking Redundancy of CNF Propositional Formulae'',

585: presented at the conference ECAI 2002.

586: 

587: \begin{verbatim}

588: \end{verbatim}

589: 

590: \tableofcontents

591: 

592: %%%%%%%%%%%%% intr %%%%%%%%%%%%%%

593: \section{Introduction}

594: 

595: A knowledge base is redundant if it contains parts that

596: can be removed without reducing the information it carries.

597: In this paper, we study the redundancy of a propositional

598: formula in Conjunctive Normal Form (CNF), that is, sets

599: of clauses. A CNF formula is redundant if and only if one

600: or more clauses can be removed from it without changing

601: its set of models.

602: 

603: The problem of redundancy, and the related problem of

604: minimization, are important for a number of reasons.

605: First, removing redundant clauses leads to a simplification

606: of the knowledge base. This may have some computational

607: advantage in some cases (\eg, it leads to an

608: exponential reduction of size.) Moreover, simplifying

609: a formula leads to a representation of the same knowledge

610: that is easier to understand, as a large amount of

611: redundancy may obscure the meaning of the represented

612: knowledge. The irredundant part of a knowledge base can

613: instead be considered the core of the knowledge it

614: represents.

615: 

616: Redundancy can be a negative characteristic or

617: not, depending on how the knowledge base is obtained.

618: Intuitively, a concept that is repeated many times (for

619: example, in a book) is likely to be a very important

620: one. If a formula results from the translation of

621: something expressed by human beings, the fact that a

622: clause is redundant is noteworthy, as it may

623: indicate that this clause carries a piece of knowledge

624: that is considered important.

625: 

626: On the other hand, redundancy may be a negative feature

627: of a knowledge base, as it may result from an incorrect

628: encoding or merging of several sources. In such cases,

629: indeed, it is possible that the intended meaning of a

630: clause is different from what the clause formally means

631: (for example, the clause has been expressed using the wrong

632: variable names.) Whatever the reason a clause is redundant,

633: the fact that it is redundant is an hint of something,

634: which may be either an high importance of the knowledge

635: it express, or an hint of a mistake that has been made

636: while building the knowledge base.

637: 

638: The problem of redundancy of knowledge bases may also be

639: relevant to applications in which efficiency of entailment is

640: important. Indeed, the size of a knowledge base is one

641: of the factors that determine the speed of the inference

642: process. While some theorem provers introduce a limited

643: number of redundant formulae for speeding up solving,

644: excessive redundancy can cause problems of storage,

645: which in turns slows down reasoning. In particular, updates

646: can increase the size of knowledge bases exponentially

647: \cite{cado-etal-99,libe-00}, and redundancy makes the problem of

648: storing the knowledge base worst.

649: 

650: Algorithms for checking

651: redundancy of knowledge bases have been developed for the

652: case of production rules \cite{gins-88-a,schm-snyd-97}.

653: In this paper, we instead study redundancy of propositional

654: knowledge base in CNF form, that is, checking whether a

655: clause in a set is implied by the others.

656: 

657: A related question that has been already investigated

658: in the propositional case is whether a knowledge base is

659: equivalent to a shorter one. This problem is called

660: {\em minimization of propositional formulae}, and it has been

661: one of the first to be analyzed from the point of view

662: of computational complexity: its study begun in the paper that

663: introduced the polynomial hierarchy \cite{meye-stoc-72}.

664: A complexity characterization of this problem has been first

665: given for Horn knowledge bases

666: \cite{maie-80,ausi-etal-86,hamm-koga-93}; afterwards, the

667: problem has been tackled again in the general case

668: \cite{hema-wech-97,uman-97}. While the Horn case is

669: now quite understood (the problem is \np-complete,

670: using several different notions of minimality,) some

671: problems regarding non-Horn formulae are still open.

672: For example, the problem of deciding whether a formula

673: is minimal (no other formula with less literals is

674: equivalent to it) is trivially in \S{2}, but

675: has only be proved \conp-hard quite recently

676: \cite{hema-wech-97}, and no other strict bound is

677: known. What makes this problem difficult to handle

678: is the fact that the considered formulae are not

679: constrained to any particular form, such as CNF or

680: DNF, or even NNF.

681: 

682: Redundancy elimination can be considered as a weak form

683: of formula minimization: if a set of clauses is redundant,

684: it is not minimal, as some clauses can be removed from

685: it while preserving equivalence. On the other hand,

686: redundancy elimination only allows for removal of clauses,

687: so it is not guaranteed to produce a minimal knowledge base.

688: For example, $\{ x \vee y, x \vee \neg y\}$ is irredundant,

689: but is equivalent to a shorter set: $\{x\}$. A related

690: problem, not analyzed in this paper, is that of removing redundancy

691: from a single clause, that is, removing literals from clauses

692: rather than removing clauses from sets. The computational

693: analysis of this problem, and of related ones, has been

694: done by Gottlob and Ferm\"uller \shortcite{gott-ferm-93}.

695: 

696: The problem of redundancy elimination is relevant for at

697: least two reasons. First, it seems somehow easier to remove

698: redundant clauses, rather than reshaping the whole knowledge

699: base. Indeed, removing redundant clauses can be done by

700: checking whether each clause can be inferred by the other

701: ones, while finding a minimal equivalent formula

702: involves a process of {\em guessing and checking} a whole

703: knowledge base for equivalence. Even for short knowledge bases,

704: the number of candidate equivalent knowledge bases is very high.

705: 

706: A second reason for preferring redundancy elimination to

707: minimization is that the syntactic form in which

708: a knowledge base is expressed can be important. For example,

709: some semantics for knowledge base revision depend on the

710: syntax of knowledge bases. If a knowledge base is replaced with

711: an equivalent one, even a single update can lead to a completely

712: different result \cite{gins-86,nebe-91}.

713: 

714: \iffalse

715: 

716: The problem of redundancy has been already analyzed as

717: a form of minimization in the case of Horn knowledge bases,

718: in which it is quadratic \cite{ausi-etal-86}. The complexity

719: of general and 2CNF cases are studied in this paper. Namely,

720: we prove that checking a knowledge base for redundancy is

721: \conp-hard in the general case, and improve over the trivial

722: algorithm for 2CNF by providing an algorithm that runs

723: in time $O(n \cdot m)$, where $n$ is the number of variables

724: and $m$ is the number of clauses.

725: 

726: \fi

727: 

728: \begin{table}

729: \begin{center}

730: \begin{tabular}{ll}

731: \hfil Problem &			\hfil Complexity \\

732: \hline

733: Checking irredundancy &		\np\  complete \\

734: A set is an \ies &		\Dp\  complete \\

735: Existence of an \ies\  of size $\leq k$ &		\S{2}\  complete \\

736: A clause is in all \ies's &	\np\  complete \\

737: A clause is in an \ies &	\S{2}\  complete \\

738: Uniqueness of \ies's &			\Dlog{2}\  complete \\

739: \hline

740: \end{tabular}

741: \caption{Complexity results about redundancy}

742: \label{complexity-table}

743: \end{center}

744: \end{table}

745: 

746: Several problems are related to that of redundancy. The

747: aim of checking redundancy is to end up with a subset of

748: clauses that is both equivalent to the original one

749: and irredundant. We call it an {\em irredundant equivalent

750: subset} of the original set, or \ies\  Note that

751: an \ies\  is a subset of the original set, and can therefore

752: only contain clauses of the original set.

753: This makes it different to a minimal equivalent {\em set},

754: which can instead be composed of arbitrary clauses.

755: 

756: The problems that are analyzed in this paper are: checking

757: whether a set is an \ies; checking the existence of an \ies\

758: of size bounded by an integer $k$; deciding whether a clause

759: is in some, or all, the \ies's; and checking uniqueness.

760: Table~\ref{complexity-table} contains the complexity of

761: these problems.

762: 

763: Since redundancy is defined in terms of equivalence (a

764: formula is redundant if it is equivalent to a proper

765: subset of its,) alternative definitions of equivalence

766: lead to different definitions of redundancy. We have

767: considered two definitions of equivalence, both based

768: on the sets of entailed formulae. Namely, var-equivalence

769: \cite{cado-etal-97-c,lang-etal-03} leads to an increase

770: of complexity, while conditional equivalence

771: \cite{libe-zhao-03} does not.

772: 

773: 

774: 

775: %%%%%%%%%%%%% prel %%%%%%%%%%%%%%

776: \section{Redundancy and \ies's}

777: 

778: In this paper, we study the redundancy

779: of sets of propositional clauses. A knowledge base

780: is redundant if it contains some redundant parts, that

781: is, it is equivalent to one of its proper subsets.

782: The definition therefore is affected by three factors:

783: 

784: \begin{enumerate}

785: 

786: \item the logic we consider;

787: 

788: \item what is ``a part'' of a knowledge base;

789: 

790: \item the definition of equivalence.

791: 

792: \end{enumerate}

793: 

794: In this paper, we use propositional logic. Nevertheless,

795: even in this simple case, we still have the problem of

796: defining what is a part of a knowledge base. For example,

797: we can consider a knowledge base a set of formulae, and

798: a part is simply one formula. A restricted case is that

799: of CNF: a knowledge base is a set of clauses, and a part

800: is simply a clause. We could also consider generic Boolean

801: formulae, and a part of them is any subformula.

802: 

803: We however only consider CNF formulae in this paper.

804: We initially consider the usual definition

805: of equivalence: other definitions are

806: considered in a later section. We sometimes use formulae

807: like

808: $a_1 \wedge \cdots \wedge a_m \rightarrow b_1 \vee \cdots \vee b_k$,

809: which can be easily translated into the equivalent clauses

810: $\neg a_1 \vee \cdots \vee \neg a_m \vee b_1 \vee \cdots \vee b_k$.

811: We also assume that clauses are not tautological.

812: 

813: \begin{definition}

814: 

815: A CNF formula is a set of non-tautological clauses.

816: 

817: \end{definition}

818: 

819: Clearly, tautologies can be easily checked and removed,

820: and do not change the complexity of the problems considered

821: here. The redundancy of a single clause is defined as follows.

822: 

823: \begin{definition}

824: 

825: A clause $\gamma \in \Pi$ is redundant in $\Pi$ if

826: and only if $\Pi \backslash \{\gamma\} \models \gamma$.

827: 

828: \end{definition}

829: 

830: The redundancy of a clause implies that the clause

831: can be removed from the set without changing its meaning.

832: In turns, the redundancy of a set of clauses can be

833: defined as its equivalence to one of its proper

834: subsets.

835: 

836: \begin{definition}

837: 

838: A set of clauses $\Pi$ is redundant if and only if

839: there exists $\Pi' \subset \Pi$ such that

840: $\Pi' \equiv \Pi$.

841: 

842: \end{definition}

843: 

844: In propositional logic, this definition is equivalent

845: to the following ones (proofs are omitted due to 

846: their triviality):

847: 

848: \begin{enumerate}

849: 

850: \item there exists $\Pi' \subset \Pi$ such that

851: $\Pi' \models \Pi$;

852: 

853: \item $\Pi$ contains a redundant clause.

854: 

855: \end{enumerate}

856: 

857: These definitions are equivalent in classical

858: logic, but they are not in other logics: for

859: example, in non-monotonic logic $\Pi' \models \Pi$

860: may hold, but still $\Pi' \not\equiv \Pi$ even

861: if $\Pi' \subset \Pi$. In the same way, it can

862: be that no part of the knowledge base is implied

863: by the other ones, but still there exists a

864: proper equivalent subset of it

865: \cite{libe-redu-3}.

866: 

867: A related definition is that of irredundant equivalent

868: subset. Such sets result from removing some redundant

869: clauses while preserving equivalence.

870: 

871: \begin{definition}

872: 

873: A set of clauses $\Pi'$ is said to be an

874: {\em irredundant equivalent subset} (\ies)

875: of another set of clauses $\Pi$ if and only

876: if:

877: 

878: \begin{enumerate}

879: 

880: \item $\Pi' \subseteq \Pi$

881: 

882: \item $\Pi' \equiv \Pi$

883: 

884: \item $\Pi'$ is irredundant

885: 

886: \end{enumerate}

887: 

888: \end{definition}

889: 

890: The second point can be replaced by $\Pi' \models \Pi$

891: for all monotonic logics.

892: An alternative definition is that an \ies\  is

893: an equivalent subset of the original set such

894: that none of its subsets has the same properties.

895: Any set of clauses has at least one \ies, but it

896: may also have more than one of them, as shown by

897: the following example.

898: 

899: \begin{example}

900: 

901: Let 

902: $

903: \Pi = \{ a \vee \neg b, \neg a \vee b ,

904: 	 a \vee c, b \vee c \}

905: $. This set has two \ies's:\eatpar

906: 

907: \begin{eqnarray*}

908: \Pi_1 &=& \Pi \backslash \{ a \vee c \} \\

909: \Pi_2 &=& \Pi \backslash \{ b \vee c \}

910: \end{eqnarray*}

911: 

912: It is indeed easy to see that the first two clauses

913: of $\Pi$ are equivalent to $a \equiv b$, which

914: implies that $a \vee c$ and $b \vee c$ are equivalent.

915: It is also easy to see that neither $a \vee \neg b$

916: nor $\neg a \vee b$ can be removed from $\Pi$ while

917: preserving equivalence with it.

918: 

919: \end{example}

920: 

921: The set of clauses of this example can be used

922: to show that a set of clauses may have exponentially

923: many \ies's. Consider the set:

924: 

925: \[

926: \Pi_n = \bigcup_{i=1,\ldots,n} \Pi[\{a/a_i,b/b_i,c/c_i\}]

927: \]

928: 

929: In words, $\Pi_n$ is made of $n$ copies of $\Pi$,

930: each built on its own set of three variables.

931: While removing clauses from $\Pi_n$, we have $n$

932: independent choices, one for each copy:

933: for each $i$ we can remove either $a_i \vee c_i$ or

934: $b_i \vee c_i$. This proves that $2^n$ outcomes are

935: possible, each leading to a different \ies

936: 

937: Since a formula may have more than one \ies, its

938: clauses can be partitioned into three sets: the ones

939: that are in all \ies's, the ones that are in some

940: \ies's, and the ones that are in no \ies\  The

941: idea is that the first clauses are necessary

942: (they cannot be removed from the set without

943: changing its semantics), the last ones are

944: useless (their removal is harmless), while the

945: other ones are ``useful but not necessary''. We

946: therefore give the following definitions.

947: 

948: \begin{definition}

949: 

950: A clause $\gamma$ in $\Pi$ is:

951: 

952: \begin{description}

953: 

954: \item[necessary:] it is in all \ies's;

955: 

956: \item[useful:] it is in some \ies's;

957: 

958: \item[useless:] it is not in any \ies.

959: 

960: \end{description}

961: 

962: \end{definition}

963: 

964: Note that useful clauses include all necessary ones,

965: and that useless and useful are opposite concepts.

966: In terms of knowledge, necessary clauses express knowledge

967: in a succinct form, as they are not redundant at all.

968: Useless clauses can instead be

969: considered ``strongly redundant'': not only they

970: can be removed; they can always be removed. In a sense,

971: they are not saying anything useful from the point of

972: view of the knowledge they express. On the other hand,

973: their presence may be important at a meta-level.

974: For example, the strong redundancy of a clause $\gamma$

975: may indicate that the information it carries is

976: very important. It may also indicate

977: that the piece of knowledge it represents has been

978: outdated by successive addition, but

979: further additions to the knowledge base may

980: require backing up to the part of knowledge we currently

981: regard as useless. Either way, useless parts may in

982: some cases be useful at a meta-level. Finally, useful

983: but not necessary clauses express knowledge that

984: the knowledge base contains in some other form,

985: that is, these clauses represent ``one possible way''

986: of telling this information. As for all redundant

987: clauses, they may tell that the knowledge they carry

988: is regarded as important, but they may even indicate

989: that mistakes has been made in the construction of

990: the knowledge base, so that two clauses that are believed

991: to say something different in fact do not.

992: 

993: Technically, checking whether a clause is necessary

994: is easy, as it does not require cycling over all

995: possible \ies

996: 

997: \begin{lemma}

998: \label{necessary-lemma}

999: 

1000: A clause $\gamma$ is necessary in $\Pi$ if and only

1001: if $\Pi \backslash \{\gamma\} \not\models \gamma$.

1002: 

1003: \end{lemma}

1004: 

1005: \proof If $\Pi \backslash \{\gamma\} \not\models \gamma$,

1006: then $\gamma$ belongs to all \ies's: this is an easy

1007: consequence of the fact that no subset of

1008: $\Pi \backslash \{\gamma\}$ can imply $\gamma$. What

1009: remains to prove is that

1010: $\Pi \backslash \{\gamma\} \models \gamma$ implies that

1011: there is an \ies\ of $\Pi$ that does not contain $\gamma$.

1012: We can build this \ies\   as follows: we start from

1013: $\Pi \backslash \{\gamma\}$ and iteratively remove

1014: clauses that can be derived from it, until we obtain

1015: a set from which no clause can be removed. This is clearly

1016: an \ies, and it does not contain $\gamma$.~\qed

1017: 

1018: Checking inutility of a clause cannot be expressed

1019: with a simple condition like this one. This is shown

1020: by Theorem~\ref{complexity-useful}, which proves that

1021: the opposite problem of telling whether a clause is

1022: useful is \P{2}-complete. As a result, the definition

1023: of uselessness cannot be expressed as a single entailment

1024: check (like the one for necessity) unless exponentially

1025: large formulae are used.

1026: 

1027: Any set of clauses has at least one \ies. Checking the

1028: existence of an \ies\  is thus trivial. On the other hand,

1029: a set may have more than one \ies. Deciding uniqueness of

1030: \ies's for a specific set of clauses is important, as it

1031: tells whether there is a choice among the possible minimal

1032: representations of the same piece of information. For

1033: example, a trivial algorithm for producing an \ies\  is

1034: that of iteratively removing the first clause

1035: that is implied by the other ones. This algorithm clearly

1036: outputs an \ies. However, other ones may exist, and

1037: be better either because are shorter (have

1038: less clauses), or because their structure make them more

1039: effective to use (for example, they are Horn or in a similar

1040: special form that makes reasoning with them easier.)

1041: 

1042: This problem is also of interest because uniqueness

1043: implies that all clauses are either necessary or useless.

1044: As a result, checking usefulness and inutility becomes

1045: the same and opposite problem of necessity, respectively.

1046: Therefore, they become much simpler than in the general

1047: case.

1048: 

1049: Clearly, if a set is irredundant, it has a single \ies\

1050: On the other hand, some sets may be redundant but have

1051: a single \ies\  anyway. The following example shows such

1052: a set.

1053: 

1054: \[

1055: \Pi = \{a \vee b, a \vee \neg b, a \vee c\}

1056: \]

1057: 

1058: The first two clauses are in fact equivalent to $a$,

1059: which makes $a \vee c$ redundant. On the other hand,

1060: $a \vee c$ cannot be used to infer $a$. As a result,

1061: the only \ies\  of this set is composed of its first

1062: two clauses.

1063: 

1064: The condition of uniqueness is formally defined as:

1065: there exists exactly one $\Pi'$ that is a subset of

1066: $\Pi$ and is irredundant. However, the following lemma

1067: shows an easier why to determine whether a set of

1068: clauses has a single \ies

1069: 

1070: \begin{lemma}

1071: \label{unique-lemma}

1072: 

1073: A set of clauses $\Pi$ has a unique \ies\  if

1074: and only if $\Pi_N \equiv \Pi$, where $\Pi_N$ is

1075: the set of necessary clauses:

1076: 

1077: \[

1078: \Pi_N = \{ \gamma \in \Pi ~|~

1079: \Pi \backslash \{\gamma\} \not\models \gamma \}

1080: \]

1081: 

1082: \end{lemma}

1083: 

1084: \proof If $\Pi$ has a unique \ies, then

1085: its clauses are exactly the clauses that

1086: are in all \ies's of $\Pi$. Lemma~\ref{necessary-lemma}

1087: tells that the clauses that are contained in all

1088: \ies's can be expressed as $\Pi_N$.

1089: 

1090: Let us now assume that $\Pi_N \models \Pi$,

1091: and prove that $\Pi_N$ is the unique \ies\  of $\Pi$.

1092: Since no clause of $\Pi_N$ is implied by the rest

1093: of $\Pi$, it is not implied by the rest of $\Pi_N$

1094: either, which proves that $\Pi_N$ is an \ies\  We

1095: only have to prove that $\Pi$ does not have any other

1096: \ies. Assume, by contradiction, that $\Pi' \not= \Pi_N$

1097: is an \ies: if $\Pi_N \subset \Pi'$, then $\Pi'$

1098: is not irredundant; otherwise, there exists

1099: $\gamma \in \Pi_N \backslash \Pi'$. This condition

1100: can be decomposed into $\gamma \in \Pi_N$ and

1101: $\gamma \not\in \Pi'$. The first formula implies

1102: $\Pi \backslash \{\gamma\} \not\models \gamma$ since

1103: $\Pi_N$ is the set of necessary clauses. The second

1104: formula, together with $\Pi' \models \Pi$, implies

1105: that $\Pi' \backslash \{\gamma\} \models \gamma$.

1106: This is a contradiction, as $\Pi' \subseteq \Pi$.~\qed

1107: 

1108: The following condition is sufficient

1109: for proving that a set of clauses has more than one

1110: \ies\  Intuitively, while removing redundant clauses

1111: from a set, we may arrive to a point in which we have

1112: a choice to make between removing one clause in a

1113: pair. If this is the case, this choice produces two

1114: different \ies's.

1115: 

1116: \begin{lemma}

1117: \label{more-lemma}

1118: 

1119: If $\Pi \backslash \{\gamma_1\} \equiv \Pi$

1120: and $\Pi \backslash \{\gamma_2\} \equiv \Pi$

1121: but $\Pi \backslash \{\gamma_1, \gamma_2\} \not\equiv \Pi$,

1122: then $\Pi$ has at least two \ies's

1123: 

1124: \end{lemma}

1125: 

1126: \proof Since any set of clauses has at least

1127: an \ies, the same happens for $\Pi \backslash \{\gamma_1\}$.

1128: Let therefore $\Pi'$ be an \ies\  of

1129: $\Pi \backslash \{\gamma_1\}$. Since

1130: $\Pi \backslash \{\gamma_1\}$ is equivalent

1131: to $\Pi$, this is also an \ies\  of $\Pi$.

1132: It does not contain $\gamma_1$ because it

1133: is a subset of $\Pi \backslash \{\gamma_1\}$.

1134: We show that it necessarily contains $\gamma_2$.

1135: Suppose it does not: then

1136: $\Pi' \subset \Pi \backslash \{\gamma_1, \gamma_2\}$

1137: which, by assumption, is not equivalent to $\Pi$,

1138: contrarily to the claim that it is.

1139: 

1140: We have therefore proved that any \ies\

1141: of $\Pi \backslash \{\gamma_1\}$ is an \ies\

1142: of $\Pi$ that contains $\gamma_2$ but not

1143: $\gamma_1$. For the same reasons, any

1144: \ies\  of $\Pi \backslash \{\gamma_2\}$

1145: is an \ies of $\Pi$ that contains $\gamma_1$

1146: but not $\gamma_2$. As a result, the \ies's

1147: of $\Pi \backslash \{\gamma_1\}$ and

1148: $\Pi \backslash \{\gamma_2\}$ are all different.

1149: Since each set has at least an \ies, we have

1150: proved that $\Pi$ has at least two \ies's.~\qed

1151: 

1152: This condition is however not necessary.

1153: Indeed, the choice between {\em two} clauses

1154: may show up only when some redundant clauses

1155: have already been removed. This happens for

1156: example when two clauses out of three have

1157: to be removed, like in the following set:

1158: 

1159: \[

1160: \Pi = \{ a \equiv b ,~ a \equiv c ,~

1161: a \vee d ,~ b \vee d, ~ c \vee d \}

1162: \]

1163: 

1164: The clauses composing the first two formulae

1165: are necessary. Since $a$, $b$, and $c$

1166: are equivalent, and the last three

1167: clauses are equivalent as well. As a result,

1168: we can always remove two of them. This proves

1169: that the condition of the theorem (which

1170: requires two non-necessary clauses not to

1171: be removable at the same time) is false,

1172: while the set has more than one \ies.

1173: 

1174: \iffalse

1175: 

1176: The condition of this lemma can be made necessary

1177: by considering subsets of $\Pi$.

1178: 

1179: \begin{lemma}

1180: 

1181: A set of clauses $\Pi$ has more than one \ies\

1182: if and only if there exists $\Pi' \subseteq \Pi$

1183: such that $\Pi' \backslash \{\gamma_1\} \equiv \Pi$

1184: and $\Pi' \backslash \{\gamma_2\} \equiv \Pi$

1185: but $\Pi' \backslash \{\gamma_1, \gamma_2\} \not\equiv \Pi$.

1186: 

1187: \end{lemma}

1188: 

1189: \fi

1190: 

1191: 

1192: \

1193: 

1194: Let us now show some properties that will be useful for

1195: the complexity analysis of problems related to redundancy

1196: and \ies's. Checking whether a specific clause is redundant

1197: is easy to characterize from a computational point of view,

1198: as it amounts to exactly one entailment test:

1199: $\Pi \backslash \{\gamma\} \models \gamma$. On the

1200: other hand, results about the redundancy of a whole

1201: set are harder to obtain, as we have to make sure

1202: that the clauses we define do not interact to form

1203: redundancy when they should not. In other words,

1204: we can still use the fact that proving that

1205: $\Pi \backslash \{\gamma\} \models \gamma$ is

1206: \conp-complete, but this is a real reduction only

1207: if $\Pi$ does not contain any other redundant clauses.

1208: The hardness proofs in this paper are indeed based

1209: on the following method:

1210: 

1211: \begin{quote}

1212: 

1213: the formula resulting from a reduction contains parts

1214: that are known to be irredundant.

1215: 

1216: \end{quote}

1217: 

1218: These parts will be then useful, because they express

1219: some constraints on the model, while they do not

1220: affect redundancy. Since the only parts that are

1221: ``known to be irredundant'' are the necessary clauses,

1222: this method can be used for problems about \ies's

1223: as well. The following definition shows how

1224: clauses can be made irredundant.

1225: 

1226: \begin{definition}

1227: 

1228: The irredundant version of a set of clauses

1229: $\Gamma = \{ \gamma_1, \ldots, \gamma_m \}$

1230: is defined as:

1231: 

1232: \[

1233: \Gamma[C] = \{ c_i \rightarrow \gamma_i ~|~ \gamma_i \in \Gamma \}

1234: \]

1235: 

1236: \noindent where $C=\{c_1,\ldots,c_m\}$ are variables

1237: of the same number of the clauses of $\Gamma$

1238: ($c_i \rightarrow \gamma_i$ denotes the clause

1239: $\neg c_i \vee \gamma_i$.)

1240: 

1241: \end{definition}

1242: 

1243: The point of this definition is that $\Gamma[C]$ is

1244: composed of necessary clauses only. The following

1245: lemma shows exactly how this can be proved.

1246: 

1247: \begin{lemma}

1248: \label{irredundant-lemma}

1249: 

1250: For any set of clauses $\Gamma$ containing no

1251: tautologies, the model $\omega_i$ below satisfies

1252: all clauses of $\Gamma[C]$ but

1253: $c_i \rightarrow \gamma_i$:

1254: 

1255: \[

1256: \omega_i(\Gamma, C) = \{ c_i \} \cup

1257: \{ \neg l_j ~|~ l_j \in \gamma_i \}

1258: \]

1259: 

1260: \end{lemma}

1261: 

1262: \proof $\omega_i(\Gamma, C)$ is not a model of $c_i \rightarrow \gamma_i$,

1263: as we assumed that no clause is tautological. On the converse,

1264: it is a model of $\Gamma[C] \backslash \{ c_i \rightarrow \gamma_i \}$

1265: simply because it falsifies all $c_j$'s with $j \not=i$.~\qed

1266: 

1267: This lemma actually proves that all clauses of

1268: $\Gamma[C]$ are irredundant. We do not state the

1269: lemma this way because the reductions use $\Gamma[C]$

1270: in conjuction with other clauses: in order to prove

1271: that the clauses of $\Gamma[C]$ are irredundant, we

1272: extend the models $\omega_i(\Gamma, C)$ in such a way they

1273: satisfy all other clauses.

1274: 

1275: While it is simple to prove that $\Gamma$ is unsatisfiable

1276: if and only if

1277: $\Gamma[C] \models \neg c_1 \vee \cdots \vee \neg c_m$, we

1278: cannot simply add this clause to $\Gamma[C]$ to show

1279: the hardness of the irredundancy problem, as this

1280: clause may make some clauses of $\Gamma[C]$ redundant. The

1281: complete proof requires adding a new variable to that

1282: clause to avoid this problem.

1283: 

1284: \begin{lemma}

1285: \label{sat-lemma}

1286: 

1287: For any set of clauses $\Gamma$, none of the clauses

1288: of $\Gamma[C]$ is redundant in $\Gamma[C,a]$ below:

1289: 

1290: \[

1291: \Gamma[C,a] = \Gamma[C] \cup

1292: \{\neg c_1 \vee \cdots \vee \neg c_m \vee \neg a\}

1293: \]

1294: 

1295: \noindent where $a$ is a new variable, while the clause

1296: $\neg c_1 \vee \cdots \vee \neg c_m \vee \neg a$ is

1297: redundant (\ie,

1298: $\Gamma[C] \models \neg c_1 \vee \cdots \vee \neg c_m \vee \neg a$)

1299: if and only if $\Gamma$ is unsatisfiable.

1300: 

1301: \end{lemma}

1302: 

1303: \proof Lemma~\ref{irredundant-lemma} proves that

1304: $\omega_i[C]$ is a model of all clauses of $\Gamma[C]$ but

1305: $c_i \rightarrow \gamma_i$. Since it is also a model

1306: of the last clause ($a$ is implicitly assumed to be

1307: false in $\omega_i[C]$), no clause of $\Gamma[C]$ is implied

1308: by the other ones. Let us now prove that the redundancy of

1309: the last clause is related to the satisfiability

1310: of $\Gamma$.

1311: 

1312: \begin{description}

1313: 

1314: \item[$\Gamma$ is unsatisfiable.] Since $\Gamma$ has

1315: no models, no model of $\Gamma[C]$ contains all $c_i$'s.

1316: As a result, $\Gamma[C] \models \neg c_1 \vee \cdots \vee \neg c_m$,

1317: which implies that

1318: $\Gamma[C] \models \neg c_1 \vee \cdots \vee \neg c_m \vee \neg a$,

1319: which in turns implies that $\Gamma[C,a]$ is redundant.

1320: 

1321: \item[$\Gamma$ is satisfiable.] We prove that the

1322: last clause of $\Gamma[C,a]$ is irredundant (the other

1323: ones have already proved to be so.) Since $\Gamma$ is

1324: satisfiable, it has a model $\omega$. By setting all $c_i$'s

1325: and $a$ to be true, we obtain the model

1326: $\omega \cup \{c_1,\ldots,c_m,a\}$, which satisfy $\Gamma[C]$.

1327: This is not a model of $\neg c_1 \vee \cdots \vee \neg

1328: c_m \vee \neg a$: as a result, the last clause is

1329: irredundant.

1330: 

1331: \end{description}~\qed

1332: 

1333: This lemma is used not only in the proof of hardness

1334: of the problem of checking redundancy, but also for

1335: the proof of hardness of other problems (such as

1336: checking necessity of a clause.)

1337: 

1338: 

1339: 

1340: %%%%%%%%%%%%% comp %%%%%%%%%%%%%%

1341: \section{Complexity Results}

1342: 

1343: In this section, we show the complexity results

1344: that are summarized in Table~\ref{complexity-table}.

1345: The first result is about the complexity of checking

1346: whether a set of clauses is redundant.

1347: 

1348: \begin{theorem}

1349: \label{th-irre}

1350: 

1351: Checking irredundancy of a set of clauses is \np-complete.

1352: 

1353: \end{theorem}

1354: 

1355: \proof Membership: we have to check whether,

1356: for any $\gamma \in \Pi$, it holds

1357: $\Pi \backslash \{ \gamma \} \not\models \gamma$.

1358: This can be done by guessing a model for each set

1359: $\Pi \backslash \{ \gamma \} \cup \{\neg \gamma\}$,

1360: which shows the problem to be in \np.

1361: 

1362: Hardness is an easy consequence of

1363: Lemma~\ref{sat-lemma}: a non-tautological

1364: set of clauses $\Gamma$ is satisfiable if and only

1365: if $\Gamma[C,a]$ is irredundant.~\qed

1366: 

1367: What this theorem proves is that checking irredundancy

1368: of a set of clauses is not harder, theoretically, than

1369: checking whether a single clause is irredundant. 

1370: Although the problem looks harder than entailment,

1371: it is indeed the hardness

1372: proof the more complex part of the completeness proof

1373: (it requires using Lemma~\ref{sat-lemma}, which in

1374: turns requires Lemma~\ref{irredundant-lemma}.)

1375: This is because redundancy does not immediately allow

1376: expressing entailment (the irredundant version of a set

1377: of clauses has been introduced exactly for solving this

1378: problem.)

1379: 

1380: Let us now turn to the problems related to \ies's.

1381: The first problem is that of checking whether a set

1382: of clauses is an \ies\  of another one. This problem

1383: clearly requires checking equivalence and irredundancy.

1384: The following theorem actually proves that the

1385: problem is hard for the class \Dp, which contains

1386: all problems that can be decomposed into a problem

1387: in \np\  and a problem in \conp.

1388: 

1389: \begin{theorem}

1390: 

1391: Given two sets of clauses $\Pi$ and $\Pi'$, checking

1392: whether $\Pi'$ is an \ies\  of $\Pi$ is \Dp-complete.

1393: 

1394: \end{theorem}

1395: 

1396: \proof Membership amounts to showing that $\Pi' \subseteq \Pi$

1397: (a polynomial task), that $\Pi' \models \Pi$ (which is

1398: in \conp) and that $\Pi'$ is irredundant (which we proved

1399: to be in \np). Therefore, the problem is in \Dp.

1400: 

1401: Hardness is proved by reduction from the \sat-\unsat\

1402: problem: given a pair of sets of clauses

1403: $\l \Gamma, \Sigma \r$, check whether the first one is

1404: satisfiable while the second one is not. This problem is

1405: \Dp-complete even if $\Gamma$ and $\Sigma$ do not share

1406: variables \cite{blas-gure-82}, which we assume. Let $C$

1407: and $D$ be new sets of variables in one-to-one correspondence

1408: with the clauses of $\Gamma$ and $\Sigma$, respectively.

1409: Let $a$ and $e$ be two other new variables.

1410: Reduction is as follows:\eatpar

1411: 

1412: \begin{eqnarray*}

1413: \Pi &=& \Gamma[C,a] \cup \Sigma[D,e] \\

1414: \Pi' &=& \Gamma[C,a] \cup \Sigma[D]

1415: \end{eqnarray*}

1416: 

1417: First, we show that $\Pi'$ is irredundant if and only

1418: if $\Gamma$ is satisfiable. By Lemma~\ref{irredundant-lemma},

1419: $\Sigma[D]$ is irredundant. Lemma~\ref{sat-lemma} proves

1420: that $\Gamma[C,a]$ 

1421: is irredundant if and only if $\Gamma$ is satisfiable.

1422: Since these two subsets of $\Pi'$ do not share variables,

1423: $\Pi'$ is irredundant if and only if both parts are,

1424: that is, $\Pi'$ is irredundant if and only if $\Gamma$

1425: is satisfiable.

1426: 

1427: What remains to prove is only that $\Pi' \models \Pi$ if and

1428: only if $\Sigma$ is unsatisfiable. By Lemma~\ref{sat-lemma},

1429: $\Sigma[D] \models \neg d_1 \vee \cdots \vee \neg d_r \vee \neg e$

1430: holds if and only if $\Sigma$ is unsatisfiable.~\qed

1431: 

1432: Given that a set of clauses can have more than

1433: one \ies, it is of interest to check the size

1434: of minimal \ies's, as it tells the amount of

1435: redundant information the theory contains, and

1436: also how much the size of the knowledge base

1437: can be reduced by deleting redundant clauses.

1438: The decision problem we consider is that of

1439: checking the existence of \ies's of size bounded

1440: by a constant integer. This problem can be solved

1441: by iterating over all possible \ies's. Such

1442: a procedure amounts to checking whether there

1443: exists a subset that is a \ies\  and has the

1444: given size. The following theorem tells that this

1445: iteration cannot be avoided in general.

1446: 

1447: \begin{theorem}

1448: \label{exists-size}

1449: 

1450: Given a set of clauses $\Pi$ and an integer

1451: $k$, deciding whether $\Pi$ has an \ies\

1452: of size at most $k$ is \S{2}-complete.

1453: 

1454: \end{theorem}

1455: 

1456: \proof Membership: the problem amounts to deciding

1457: whether there exists a subset of $\Pi$ that is

1458: equivalent to it and of size at most $k$. Since

1459: the problem can be expressed as a $\exists\forall$QBF,

1460: it is in \S{2}.

1461: 

1462: Hardness is proved via a quite complicated reduction

1463: from $\exists\forall$QBF. Let $\exists X \forall Y. \neg \Gamma$

1464: be a formula, where

1465: $\Gamma = \{ \gamma_1, \ldots, \gamma_m \}$ is a set of

1466: clauses. This problem is \S{2}-hard, as it

1467: is the complement of the problem of deciding whether

1468: a $\forall\exists$QBF, in which the matrix is a CNF

1469: formula, is valid \cite{stoc-meye-73}.

1470: We build a set $\Pi$ as the union of the following

1471: sets of clauses:

1472: 

1473: \begin{eqnarray*}

1474: \Pi_1 &=& \bigcup^{j=1,\ldots,r}_{i=1,\ldots,n}

1475:           \{ x^j_i, z^j_i \}

1476: \\

1477: \Pi_2 &=& \bigcup_{i=1,\ldots,n}

1478:           \{ x^1_i \wedge \cdots \wedge x^r_i \rightarrow x_i,

1479:              z^1_i \wedge \cdots \wedge z^r_i \rightarrow z_i \}

1480: \\

1481: \Pi_3 &=& \bigcup_{i=1,\ldots,n}

1482:           \{ x_i \rightarrow w_i,

1483:              z_i \rightarrow w_i \}

1484: \\

1485: \Pi_4 &=& \bigcup_{j=1,\ldots,m}

1486:           \{ w_1 \wedge \cdots \wedge w_n \rightarrow \gamma_j^N \}

1487: \\

1488: \Pi_5 &=& \{ v_1, \ldots, v_t, \neg v_1 \vee \cdots \vee \neg v_t \}

1489: \end{eqnarray*}

1490: 

1491: Here, $\gamma^N_j$ is obtained from $\gamma_j$ by replacing

1492: every positive occurrence of $x_i$ with $\neg z_i$. The values

1493: of the constant $k$, $r$, and $t$ are chosen as follows:

1494: if $n$ is the number of variables and $m$ the number of

1495: clauses of $\Gamma$, we set $r=m+1$, $k=(r+2) \cdot n +m$,

1496: and $t=k+1$.

1497: 

1498: We prove that $\exists X \forall Y. \neg \Gamma$ is valid

1499: if and only if 

1500: $\Pi = \Pi_1 \cup \Pi_2 \cup \Pi_3 \cup \Pi_4 \cup \Pi_5$

1501: has an equivalent subset of size at most $k$.

1502: 

1503: The set $\Pi$ is unsatisfiable because $\Pi_5$

1504: is unsatisfiable. Therefore, we are looking for a

1505: subset of $\Pi$ of size at most $k$ that is unsatisfiable.

1506: Note that, removing even a single clause from $\Pi_5$, it

1507: becomes satisfiable. Since $\Pi_5$ does not share any variable

1508: with the other subsets, it follows that no proper subset

1509: of $\Pi_5$ can contribute to the generation of unsatisfiability.

1510: Since $t>k$, if an unsatisfiable subset of size less than

1511: $k$ contains clauses from $\Pi_5$, they can be removed

1512: while maintaining unsatisfiability. As a result,

1513: while looking for an unsatisfiable subset of $\Pi$,

1514: clauses of $\Pi_5$ can be disregarded: these clauses

1515: are only used to guarantee that $\Pi$ is unsatisfiable.

1516: 

1517: We have therefore proved that $\Pi$ has an \ies\  of size

1518: bounded by $k$ if and only if 

1519: $\Pi_1 \cup \Pi_2 \cup \Pi_3 \cup \Pi_4$ has an inconsistent

1520: subset of size bounded by $k$. Let us therefore consider

1521: $\Pi' \subseteq \Pi_1 \cup \Pi_2 \cup \Pi_3$ and

1522: $\Pi'' \subseteq \Pi_4$, and see what happens when

1523: $\Pi' \cup \Pi''$ is an unsatisfiable set of at most

1524: $k$ clauses.

1525: 

1526: First, neither $\Pi'$ nor $\Pi''$ is unsatisfiable alone,

1527: as both $\Pi_1 \cup \Pi_2 \cup \Pi_3$ and $\Pi_4$ are

1528: satisfiable (the first is satisfied by the model that

1529: evaluates to true all variables, the second by the model

1530: that evaluates to false all variables.)

1531: Second, if $\Pi'$ does not imply all $w_i$'s, then

1532: $\Pi' \cup \Pi_4$ is satisfiable, and therefore

1533: $\Pi' \cup \Pi''$ is satisfiable as well. There exists

1534: exactly two minimal subsets of $\Pi_1 \cup \Pi_2 \cup \Pi_3$

1535: that imply $w_i$:

1536: 

1537: \begin{eqnarray*}

1538: \Sigma_i

1539: &=&

1540: \bigcup_{j=1,\ldots,r} \{ x^j_i \} \cup

1541: \{ x^1_1 \wedge \cdots \wedge x^r_i \rightarrow x_i, x_i \rightarrow w_i \}

1542: \\

1543: \Sigma'_i

1544: &=&

1545: \bigcup_{j=1,\ldots,r} \{ z^j_i \} \cup

1546: \{ z^1_1 \wedge \cdots \wedge z^r_i \rightarrow z_i, z_i \rightarrow w_i \}

1547: \end{eqnarray*}

1548: 

1549: These two sets have the same size. The number $k$

1550: has been chosen so that $k=n \cdot (r+2) +m = n \cdot |\Sigma_i| + m$.

1551: Since all $w_i$'s have to be implied, $\Sigma_i \subset \Pi'$

1552: or $\Sigma_i' \subset \Pi'$ for each $i$. Since $m<|\Sigma_i|$, we have

1553: that $k< n \cdot (|\Sigma_i|+1)$, that is, $\Pi'$ cannot contain

1554: more than $n$ sets $\Sigma_i$ or $\Sigma_i'$. More precisely,

1555: $r+1=m+2$ other clauses are necessary to imply another $x_i$

1556: or $z_i$, which are shared with $\Pi''$. Therefore, $\Pi'$

1557: must contain exactly one group among $\Sigma_i$ and $\Sigma'_i$

1558: for any $i$, which amounts to $n \cdot (r+2)$ clauses. The

1559: remaining $m$ clauses can be taken from $\Pi''$. Since

1560: $\Pi_4$ has size $m$, we can simply take $\Pi''=\Pi_4$.

1561: 

1562: We have proved that $\Pi'$ implies either

1563: $x_i$ or $z_i$, for any $i$, but not both. Candidate

1564: unsatisfiable subsets are therefore in correspondence with

1565: truth assignments on the variables $x_i$. Moreover, all

1566: variables $w_i$ are true, which makes $\Pi_4$ equivalent

1567: to $\bigcup_{j=1,\ldots,m} \{ \gamma^N_j \}$. If $\Pi'$

1568: contains $x_i$, then $\neg x_i$ can be removed from any

1569: clause $\gamma^N_j$ containing it, while $\neg z_i$ remains.

1570: The opposite happens if $z_i$ is in $\Pi'$.

1571: 

1572: Either way, if a variable of $\{x_i,z_i\}$ is in $\Pi'$,

1573: the other one is not mentioned in $\Pi'$, so we can assign

1574: it to false in order to satisfy as many clauses as possible

1575: (we are trying to prove unsatisfiability, so we have to test

1576: the most unfavorable possibility). What remains of $\Pi_4$

1577: is the set $\Gamma$ in which all variables $x_i$ has been

1578: removed, by assigning them either to true (if

1579: $\Sigma_i \subset \Pi'$) or to false

1580: (if $\Sigma'_i \subset \Pi'$). Therefore, the choice of

1581: including $\Sigma_i$ or $\Sigma_i'$ makes $\Pi_4$ equivalent

1582: to $\Gamma$ after setting $x_i$ to some truth value.

1583: Therefore, $\Pi$ has an unsatisfiable subset of size $k$

1584: if and only if $\exists X \forall Y . \neg \Gamma$ is true.

1585: 

1586: Note that the choice of

1587: an unsatisfiable set $\Pi$ is not necessary. Indeed,

1588: by adding a new variable $u$ to all clauses, $\Pi$ and

1589: all its subsets are made satisfiable. Since $\Pi$ is

1590: now equivalent to $u$, one of its subsets can be

1591: equivalent to it only if, assigning false to $u$, leads

1592: to unsatisfiability, which has been proved to be

1593: equivalent to the QBF problem.~\qed

1594: 

1595: This theorem implies that, unless the polynomial

1596: hierarchy collapses, the problem of checking

1597: the existence of \ies's of size bounded by $k$

1598: is not in any class below \S{2}. As a result,

1599: the definition of the problem is not equivalent

1600: to a condition that contains ``less quantifiers'',

1601: unless an exponential blow-up is introduced.

1602: In other words, any condition that do not require

1603: checking exponentially sized formulae will contain

1604: an initial part ``there exists something...''

1605: similar to the part ``there exists $\Pi'$...'' of

1606: the original definition. Such a simpler equivalent

1607: condition would indeed imply that the problem is

1608: in \np\  or \conp.

1609: 

1610: This is not the case for the problem of checking

1611: the membership of a clause to all \ies's, on the

1612: other hand: while the initial definition is

1613: ``for all $\Pi' \subseteq \Pi$,...'', we proved

1614: it equivalent to

1615: $\Pi \backslash \{\gamma\} \not\models \gamma$.

1616: This simplification is however only possible because

1617: the problem is easier than what appears from the definition:

1618: while the definition of the problem can be expressed

1619: as a $\forall\exists$QBF (implying that the problem

1620: is in \P{2},) Lemma~\ref{necessary-lemma} proved that

1621: the problem is actually in \conp. The next theorem

1622: also shows that the problem is hard for that class

1623: (and cannot therefore be simplified to a condition

1624: that do not require a satisfiability/entailment

1625: test at all.)

1626: 

1627: \begin{theorem}

1628: 

1629: Deciding whether a clause is necessary in a set

1630: (it is contained in all its \ies's) is \np-complete.

1631: 

1632: \end{theorem}

1633: 

1634: \proof By Lemma~\ref{necessary-lemma}, a clause

1635: is necessary if and only if

1636: $\Pi \backslash \{\gamma\} \not\models \gamma$,

1637: and this problem is in \np. Hardness easily

1638: follows from Lemma~\ref{sat-lemma}: since all

1639: clauses of $\Gamma[C,a]$ are irredundant but

1640: (possibly) the last one, $\Gamma[C,a]$ has exactly

1641: one \ies, which is either $\Gamma[C]$ or $\Gamma[C,a]$,

1642: depending on the satisfiability of $\Gamma$.

1643: As a result, the only clause of

1644: $\Gamma[C,a] \backslash \Gamma[C]$ is in all

1645: \ies's if and only if $\Gamma$ is satisfiable.~\qed

1646: 

1647: While deciding whether a clause is in all \ies's is

1648: in \np, the similar problem of deciding whether a

1649: clause is in {\em at least one} \ies\  is complete

1650: for the class \S{2}, and is therefore harder. This result

1651: is somehow surprising, as these two problems have

1652: very similar definitions, and checking the existence

1653: of an \ies\  containing a clause may look even

1654: simpler than checking all of them.

1655: 

1656: \begin{theorem}

1657: \label{complexity-useful}

1658: 

1659: Deciding whether a clause $\gamma$ is in at least one \ies\

1660: of a set of clauses $\Pi$ is \S{2}-complete.

1661: 

1662: \end{theorem}

1663: 

1664: \proof Membership is trivial: the problem can be expressed

1665: as the existence of a set $\Pi' \subseteq \Pi$ containing

1666: $\gamma$ that is equivalent to $\Pi$ and irredundant.

1667: 

1668: Hardness is proved by reduction from $\exists\forall$QBF.

1669: We assume that the matrix of the QBF formula is the negation

1670: of a CNF: this problem is \S{2}-hard, as it is the complement

1671: of deciding whether a $\forall\exists$QBF formula, in which

1672: the matrix is in CNF, is valid \cite{stoc-meye-73}.

1673: We prove that $\exists X \forall Y . \neg \Gamma$ is valid

1674: (where $\Gamma=\{\gamma_1,\ldots,\gamma_m\}$)

1675: if and only if $w$ is in at least one \ies\  of the

1676: following set $\Pi$:

1677: 

1678: \[

1679: \Pi =

1680: \bigcup_{i=1,\ldots,n} \{ x_i, \neg x_i \} \cup

1681: \{ w \} \cup

1682: \bigcup_{i=1,\ldots,m} \{ w \rightarrow \gamma_i \}

1683: \]

1684: 

1685: This set is clearly unsatisfiable. Its \ies's are its

1686: unsatisfiable minimal subsets. Let us now show how a

1687: subset $\Pi'$ of this kind is composed. If both $x_i$ and

1688: $\neg x_i$ are in $\Pi'$, they are enough to generate

1689: contradiction, so no other clause can be in $\Pi'$,

1690: otherwise the other clauses would be redundant. We have

1691: therefore found a first group of minimal unsatisfiable

1692: subsets of $\Pi$: those composed exactly of a pair

1693: $\{x_i, \neg x_i\}$.

1694: 

1695: Let us now try to build an unsatisfiable $\Pi' \subseteq \Pi$

1696: that contains $w$. Besides $w$, such set $\Pi'$ can include

1697: $\bigcup_{i=1,\ldots,m} \{ w \rightarrow \gamma_i \}$,

1698: as well as a literal between $x_i$ and $\neg x_i$ for

1699: any $i$ (but not both, otherwise the other clauses

1700: would be redundant). It is now evident that such set can

1701: be unsatisfiable only if, for the given choice of the

1702: $x_i$'s, the set $\Gamma$ is unsatisfiable. Thus,

1703: there exists an unsatisfiable subset of $\Pi$ containing

1704: $w$ if and only if $\Gamma$ is unsatisfiable. What remains

1705: to prove is that any \ies\  obtained by removing redundant

1706: clauses from $\Pi'$ contains $w$, but this is an easy

1707: consequence of the fact that $\Pi' \backslash \{w\}$ is

1708: satisfiable.~\qed

1709: 

1710: The hardness result proves that, unlike the necessary

1711: condition, the definition of usefulness cannot be reduced

1712: to a simple entailment/satisfiability check, unless the

1713: polynomial hierarchy collapses or some exponentially

1714: large formulae are used.

1715: 

1716: The problem of uniqueness amounts to checking whether a

1717: set of clauses has a single \ies\  This problem can be

1718: solved without cycling over all possible subsets of

1719: clauses, as Lemma~\ref{unique-lemma} proves that finding

1720: the set of necessary clauses suffices.

1721: 

1722: \begin{theorem}

1723: 

1724: Deciding whether a set of clauses $\Pi$ has a single

1725: \ies\  is \Dlog{2}\  complete.

1726: 

1727: \end{theorem}

1728: 

1729: \proof By Lemma~\ref{unique-lemma}, all we have to

1730: do is to check whether the set of necessary clauses

1731: $\Pi_N$ is equivalent to $\Pi$. In turns, the set

1732: of necessary clauses can be found by checking

1733: $\Pi \backslash \{\gamma\} \not\models \gamma$ for

1734: each clause $\gamma \in \Pi$. As a result, we perform

1735: a polynomial number of parallel calls to an oracle in

1736: \np\  (each one to check whether a clause is necessary)

1737: followed by a single other call (to check equivalence

1738: between $\Pi_N$ and $\Pi$.) By a well-known result by

1739: Gottlob \cite{gott-95-jacm}, the problem is in \Dlog{2}.

1740: 

1741: We prove that the problem of uniqueness is

1742: \Dlog{2}-hard by reduction from the problem

1743: of odd satisfiability: given a sequence of

1744: sets of clauses $(\Pi^1, \ldots, \Pi^r)$,

1745: each built on its own alphabet,

1746: such that the unsatisfiability of $\Pi^j$

1747: implies that of $\Pi^{j+1}$, decide

1748: whether the first $\Pi^k$ that is unsatisfiable

1749: is of odd index, that is, $k$ is odd.

1750: 

1751: For each set of clauses $\Pi^j$, we need an additional

1752: set of variables $C^j=\{c^j_1,\ldots,c^j_m\}$ and three

1753: other variables $a^j$, $b^j$, and $c^j$. We define

1754: $\gamma^j_g =\neg c^j_1 \vee \cdots \vee \neg c^j_m$.

1755: As proved by Lemma~\ref{sat-lemma}, $\Pi^j[C^j]$ implies

1756: $\gamma^j_g \vee d$, where $d$ is a variable not occurring

1757: in $\Pi^j[C^j]$ (\eg, $a^j$), if and only if $\Pi^j$ is

1758: unsatisfiable.

1759: 

1760: Let $j$ be an odd index between $1$ and $r$. Define:\eatpar

1761: 

1762: \begin{eqnarray*}

1763: \Pi^j_D

1764: &=&

1765: \Pi^j[C^j] \cup

1766: \{ \gamma^j_g \vee a^j \vee c^j,~

1767:    \gamma^j_g \vee b^j \vee c^j \}

1768: \\

1769: \Pi^{j+1}_D

1770: &=&

1771: \Pi^{j+1}[C^{j+1}] \cup

1772: \{ \gamma^j_g \vee c^{j+1}_i \vee a^j \vee \neg b^j ~|~

1773: \gamma^{j+1}_i \in \Pi^{j+1} \} \cup

1774: \\

1775: &&

1776: \{ \gamma^j_g \vee c^{j+1}_i \vee \neg a^j \vee b^j ~|~

1777: \gamma^{j+1}_i \in \Pi^{j+1} \}

1778: \end{eqnarray*}

1779: 

1780: Variables are only shared between $\Pi^j_D$

1781: and $\Pi^{j+1}_D$, and only if $j$ is odd.

1782: We therefore only have to check whether

1783: $\Pi^j_D \cup \Pi^{j+1}_D$ has a unique \ies,

1784: where $j$ is odd.

1785: 

1786: Let us consider the easiest cases first.

1787: By Lemma~\ref{sat-lemma}, if $\Pi^j$ is unsatisfiable,

1788: then the clauses $\gamma^j_g \vee c^j$ and

1789: $\gamma^j_g \vee c^{j+1}$ are entailed by

1790: $\Pi^j[C^j]$. As a result, all clauses but

1791: those in $\Pi^j_D \cup \Pi^{j+1}_D$ are redundant.

1792: Since the clauses in $\Pi^j_D \cup \Pi^{j+1}_D$ are

1793: irredundant, we have a single \ies\  $\Pi^j_D \cup \Pi^{j+1}_D$.

1794: 

1795: The second easy case is when $\Pi^{j+1}_D$ unsatisfiable.

1796: By Lemma~\ref{sat-lemma}, $\Pi^{j+1}[C^{j+1}]$ implies

1797: $\neg c^{j+1}_1 \vee \cdots \neg c^{j+1}_m$, that is,

1798: at least a variable $c^{j+1}_i$ is false. As a result,

1799: $(a^j \equiv b^j) \vee \gamma^j_g$ is entailed.

1800: Therefore, the two last clauses of $\Pi^j_D$

1801: are made equivalent; therefore, one of them

1802: can be removed, but not both. By Lemma~\ref{more-lemma},

1803: $\Pi$ has have more than one \ies\

1804: 

1805: The longest part of the proof is to prove that,

1806: if both $\Pi^j$ and $\Pi^{j+1}$ are satisfiable,

1807: then all clauses are irredundant. This is proved

1808: by showing, for each clause, a model of the other

1809: clauses that is not a model of it. For the clauses

1810: in $\Pi^j[C^j]$ this is the model

1811: $\omega_i(C^j)$ of Lemma~\ref{irredundant-lemma},

1812: extended by setting all $C^j$ to false, and $c^j$,

1813: $a^j$, and $b^j$ to true.

1814: 

1815: For the clause $a^j \vee c^j \vee \gamma^j_g$, we

1816: choose the model evaluating all $c^j_i$ and $c^{j+1}_i$

1817: to true, all variables of $\Pi^j$ and $\Pi^{j+1}$

1818: according to their respective models, both $a^j$ and

1819: $c^j$ to false, and $b^j$ to true. This model does

1820: not satisfy $a^j \vee c^j \vee \gamma^j_g$ by

1821: construction, but satisfies all other clauses. Indeed,

1822: all clauses of $\Pi^j[C^j] \cup \Pi^{j+1}[C^{j+1}]$ are satisfied

1823: because we have chosen the models of $\Pi^j$ and $\Pi^{j+1}$,

1824: the clause $b^j \vee c^j \vee \gamma^j_g$ is satisfied

1825: because of $b^j$, and the clauses

1826: $c^{j+1}_i \vee [\neg] a^j \vee [\neg] b^j \vee \gamma^j_g$

1827: are satisfied because of $c^{j+1}_i$. For the clause

1828: $b^j \vee c^j \vee \gamma^j_g$, the model with the

1829: values of $a^j$ and $b^j$ swapped works in the same way.

1830: 

1831: The clause $c^{j+1}_i \vee a^j \vee \neg b^j \vee \gamma^j_g$

1832: is falsified by the model that evaluates $c^{j+1}_i$

1833: to false, $a^j$ to false, $b^j$ to true, $c^j$ to

1834: true, all $c^j_i$ to true, all $c^{j+1}_z$ with

1835: $z \not= i$ to true, and the variables of

1836: $\Pi^j$ and $\Pi^{j+1}$ according to their respective

1837: models. This model satisfies all other clauses:

1838: indeed, the clauses of $\Pi^j[C^j] \cup \Pi^{j+1}[C^{j+1}]$ 

1839: are satisfied by the choice of the variables of

1840: $\Pi^j$ and $\Pi^{j+1}$; all clauses with $b^j$ or

1841: $c^j$ are satisfied as well; the only remaining

1842: clauses are those of the form

1843: $c^{j+1}_z \vee a^j \vee \neg b^j \vee \gamma^j_g$,

1844: with $z \not= i$, which are however satisfied by

1845: the truth value of $c^{j+1}_z$.~\qed

1846: 

1847: 

1848: 

1849: 

1850: 

1851: 

1852: 

1853: %%%%%%%%%%%%% quer %%%%%%%%%%%%%%

1854: \section{Query Equivalence}

1855: 

1856: The definition of equivalence that is most commonly

1857: used is that of logical equivalence: two formulae

1858: are equivalent if and only if they have the same sets

1859: of models. This definition is the same as the following

1860: one.

1861: 

1862: \begin{quote}

1863: 

1864: two formulae $\Pi_1$ and $\Pi_2$ are logically

1865: equivalent if and only if, for any formula $\Gamma$,

1866: it holds $\Pi_1 \models \Gamma$ if and only if

1867: $\Pi_2 \models \Gamma$.

1868: 

1869: \end{quote}

1870: 

1871: This definition is formally equivalent to the previous

1872: one, but emphasizes a common use of propositional formulae:

1873: if a formula $\Pi_1$ represents a piece of knowledge,

1874: reasoning is usually (but not always) done in terms of

1875: queries. In turns, querying a knowledge base means

1876: checking whether some facts follow from it or not.

1877: Formally, given a piece of knowledge represented by

1878: a formula $\Pi_1$, querying it means checking whether

1879: a fact represented by another formula $\Gamma$ follows

1880: from it, that is, whether $\Pi_1 \models \Gamma$. If

1881: the above condition on $\Pi_1$ and $\Pi_2$ holds, we

1882: can say that $\Pi_2$ represents the same knowledge as

1883: $\Pi_1$ as these two formulae are

1884: indistinguishable from the point of view of reasoning.

1885: 

1886: This new definition of equivalence is of interest because

1887: it can be extended in many directions. Namely, if not all

1888: formulae are possible queries, it

1889: does not coincide any more with logical equivalence. Two

1890: cases have been considered in the past:

1891: 

1892: \begin{enumerate}

1893: 

1894: \item we are only interested in queries

1895: that are in a particular syntactic form, for example,

1896: the Horn form~\cite{cado-doni-97};

1897: 

1898: \item we are only interested in formulae about a

1899: subset of variables

1900: \cite{cado-etal-97-c,lang-etal-03}.

1901: 

1902: \end{enumerate}

1903: 

1904: On the other hand, we may also interested in a set

1905: of queries that {\em strictly include} the

1906: set of propositional formulae. This is the case, for

1907: example, when queries can be conditional formulae

1908: like $\Gamma > \Sigma$, which means ``if $\Gamma$ were

1909: true, would $\Sigma$ holds?''

1910: 

1911: \begin{enumerate}

1912: 

1913: \setcounter{enumi}{2}

1914: 

1915: \item we are interested into all possible

1916: conditional queries \cite{libe-zhao-03}.

1917: 

1918: \end{enumerate}

1919: 

1920: Intuitively, $\Gamma > \Sigma$ is entailed by $\Pi$

1921: if and only if $\Sigma$ follows from the formula

1922: that is obtained by revising $\Pi$ with $\Gamma$.

1923: This motivates this kind of equivalence: two

1924: formulae are equivalent if and only if they are

1925: logically equivalent, and remain so regardless of updates.

1926: This kind of equivalence is related to strong equivalence

1927: in logic programming \cite{lifs-pear-valv-01}, and

1928: has been defined for propositional logic by

1929: Liberatore and Zhao~\cite{libe-zhao-03}.

1930: 

1931: We call any form of equivalence that is based on a

1932: particular set of consequences {\em query equivalence}

1933: (this name has been used by Cadoli et al.

1934: \cite{cado-etal-97-c} for the definition based on

1935: a subset of variables, but it is somehow inappropriate

1936: as other sets of queries make sense.) The two

1937: forms of equivalence above (based on considering subsets

1938: of propositional formulae) are called Horn equivalence

1939: and var-equivalence, respectively. The form of equivalence

1940: based on conditional statements is instead called

1941: strong equivalence or conditional equivalence.

1942: 

1943: Since redundancy is defined in terms of equivalence

1944: (a set is redundant if and only if it is equivalent

1945: to a proper subset of its,) using a definition of

1946: equivalence that is different from the logical one

1947: leads to different properties and results.

1948: Using query equivalence, redundancy

1949: tells which clauses are really necessary \wrt\  a given

1950: set of queries. We only consider two kinds of equivalence:

1951: var-equivalence and conditional equivalence. The two

1952: corresponding forms of redundancy are called

1953: var-redundancy and conditional redundancy.

1954: 

1955: \let\subsectionnewpage=\newpage

1956: %%%%%%%%%%%%% var %%%%%%%%%%%%%%

1957: \subsection{Var-Redundancy}

1958: 

1959: Var redundancy is defined in the same way as logical

1960: redundancy, but using var-equivalence instead of

1961: logical equivalence. This kind of equivalence

1962: is called {\em query equivalence} by Cadoli et al.

1963: \cite{cado-etal-97-c} and {\em var-equivalence} by

1964: Lang, Liberatore, and Marquis \cite{lang-etal-03}.

1965: We prefer the second name, and reserve the first one

1966: for the more general concept of equivalence based on

1967: an arbitrary set of queries. Formally, var-equivalence

1968: is defined as follows.

1969: 

1970: \begin{definition}[Var-Equivalence \cite{lang-etal-03}]

1971: 

1972: Two formulae $\Pi_1$ and $\Pi_2$ are var-equivalent

1973: \wrt\ a set of variables $V$ if and only if, for

1974: each formula $\Gamma$ over variables $V$, it holds

1975: $\Pi_1 \models \Gamma$ if and only if $\Pi_2 \models \Gamma$.

1976: We denote var-equivalence between $\Pi_1$ and $\Pi_2$

1977: by $\Pi_1 \qequiv{V} \Pi_2$.

1978: 

1979: \end{definition}

1980: 

1981: If $V$ is the set of all variables,

1982: $\equiv$ and $\qequiv{V}$ coincide. On the other

1983: hand, if $V$ is only composed of a subset of the

1984: variables, these two kinds of equivalence are

1985: different. In particular, while checking equivalence

1986: is \conp-complete, checking var-equivalence is

1987: \P{2}-complete \cite{lang-etal-03}. As a result,

1988: checking var-redundancy is expected to be different

1989: from redundancy, and to be harder. The following

1990: equivalent condition of var-equivalence simplifies

1991: the subsequent proofs.

1992: 

1993: \begin{theorem}

1994: 

1995: $\Pi_1 \qequiv{V} \Pi_2$ holds if and only if, for any

1996: cube $\delta$ over $V$ (\ie, a non-tautological

1997: clause containing all variables over $V$),

1998: it holds $\Pi_1 \models \delta$ if and only if

1999: $\Pi_2 \models \delta$.

2000: 

2001: \end{theorem}

2002: 

2003: \proof Follows from the fact that any formula over

2004: variables $V$ can be expressed as a conjunction of

2005: cubes over $V$.~\qed

2006: 

2007: This theorem simply tells us that equivalence can be

2008: checked by looking at the cubes over $V$, rather than

2009: checking all possible formulae. This theorem also

2010: implies that all formulae that are var-equivalent are

2011: also var-equivalent to some formulae that only

2012: contain variables of $V$: one such formula is the

2013: disjunction of all cubes over $V$ that are implied.

2014: This formula is called the forgetting of the variables

2015: that are not in $V$ \cite{lang-etal-03}.

2016: 

2017: Since cubes correspond to models, a

2018: similar property based on partial models holds. To

2019: this aim, we have however to give a special definition

2020: of model satisfaction.

2021: 

2022: \begin{definition}[Var-models]

2023: 

2024: A model $\omega_V$ over variables $V$ is a var-model

2025: of $\Pi$ if and only if the set of literals implied

2026: by $\omega_V$ is consistent with $\Pi$. We denote this

2027: fact as $\omega_V \stackrel{V}{\models} \Pi$.

2028: 

2029: \end{definition}

2030: 

2031: In other words, $\omega_V$ is a var-models of $\Pi$

2032: if and only if there exists another model $\omega'$ 

2033: over the set of variables not in $V$ such that

2034: $\omega_V \omega' \models \Pi$. Using this definition

2035: of models, we can give a semantical characterization

2036: of var-equivalence.

2037: 

2038: \begin{theorem}

2039: 

2040: $\Pi_1 \qequiv{V} \Pi_2$ holds if and only if,

2041: for any model $\omega_V$ over $V$ it

2042: holds $\omega_V \stackrel{V}{\models} \Pi_1$

2043: if and only if $\omega_V \stackrel{V}{\models} \Pi_2$.

2044: 

2045: \end{theorem}

2046: 

2047: The definition of var-redundancy differs from

2048: that of redundancy only because logical equivalence

2049: is replaced by var-equivalence.

2050: 

2051: \begin{definition}[Var-Redundancy of a Clause]

2052: 

2053: A clause $\gamma$ is var-redundant in $\Pi$

2054: \wrt\  variables $V$ if and only if

2055: $\Pi \backslash \{\gamma\} \qequiv{V} \Pi$.

2056: 

2057: \end{definition}

2058: 

2059: The fact that var-redundancy is different from

2060: redundancy can be seen from the following formula

2061: using $V=\{x\}$:

2062: 

2063: \[

2064: \Pi = \{ x, y \}

2065: \]

2066: 

2067: $\Pi$ is logically irredundant. However, the clause $y$

2068: is var-redundant in $\Pi$ \wrt\

2069: $V=\{x\}$: if queries are restricted to formulae

2070: built on the variable $x$ only, then the clause $y$

2071: is not needed. Note that var-redundancy does not

2072: depend only on the variables a clause contains:

2073: the clause $\gamma = \neg y$ is not var-redundant

2074: in the set $\Pi=\{x \vee y, \neg y\}$ \wrt\

2075: $V=\{x\}$ even if it does not mention any variable in $V$.

2076: 

2077: \begin{definition}[Var-Redundancy of a Set]

2078: 

2079: A set of clauses is var-redundant if and only

2080: if it contains a clause that is var-redundant

2081: in it.

2082: 

2083: \end{definition}

2084: 

2085: Since entailment is monotonic, var-irredundancy

2086: of all clauses of $\Pi$ is the same as the non-equivalence

2087: of $\Pi$ with one of its proper subsets. The problem is

2088: therefore not harder than the problem of equivalence, as

2089: a linear number of equivalence checks that can be done

2090: in parallel are as hard as a single one.

2091: 

2092: Since var-equivalence is harder than logical equivalence

2093: (\P{2}-complete \cite{lang-etal-03} vs.\  \conp-complete),

2094: we expect var-redundancy to be harder than logical redundancy.

2095: However, it is also easy to prove that redundancy is in the same

2096: class of the corresponding equivalence problem, as it

2097: amounts to solve a number of equivalence problems that can

2098: be done in parallel. Proving that var-redundancy is hard for

2099: the same class, instead, is slightly more difficult.

2100: The following property is useful.

2101: 

2102: \begin{lemma}

2103: 

2104: A clause $\gamma$ is var-redundant in $\Pi$ \wrt\

2105: $V$ if and only if any var-model of

2106: $\Pi \backslash \{\gamma\}$ over $V$ is a also a

2107: var-model of $\Pi$.

2108: 

2109: \end{lemma}

2110: 

2111: If a clause $\gamma$ only contains variables of $V$,

2112: checking redundancy is relatively easy, as it amounts

2113: to checking whether $\gamma$ is logically implied by

2114: the other clauses. As a result, the \P{2}-hardness of

2115: the problem of redundancy of a single clause can only

2116: be proved if the clause contains some literals not in

2117: $V$.

2118: 

2119: \begin{theorem}

2120: 

2121: Checking whether a clause

2122: is var-redundant \wrt\  $V$ in a set

2123: is \P{2}-complete.

2124: 

2125: \end{theorem}

2126: 

2127: \proof Membership follows from the fact that checking

2128: var-equivalence is in \P{2}. Hardness is proved by

2129: showing that $(\neg a \vee \Sigma) \cup \{a\}$

2130: is var-equivalent \wrt\  $X$ to $(\neg a \vee \Sigma)$

2131: if and only if $\forall X \exists Y . \Sigma$, where

2132: $(\neg a \vee \Sigma)$ denotes the set

2133: $\{\neg a \vee \gamma ~|~ \gamma \in \Sigma\}$.

2134: 

2135: \begin{description}

2136: 

2137: \item[Assume $\forall X \exists Y ~.~ \Sigma$.]

2138: This assumption can be rephrased as: all partial

2139: models over $X$ can be extended to form a model of

2140: $\Sigma$. All models over $X$

2141: can then be extended to form a model that satisfies

2142: both $(\neg a \vee \Sigma) \cup \{a\}$ and

2143: $(\neg a \vee \Sigma)$ by simply adding the

2144: evaluation of $a$ to $\true$, that is, all var-models

2145: of $\neg a \vee \Sigma$ are var-models of

2146: $(\neg a \vee \Sigma) \cup \{a\}$.

2147: 

2148: \item[Assume $\exists X \forall Y ~.~ \neg \Sigma$.]

2149: We prove that $(\neg a \vee \Sigma) \cup \{a\}$ and

2150: $(\neg a \vee \Sigma)$ are not equivalent.

2151: Let $\omega_X$ be the model over $X$ such that

2152: $\Sigma$ is false regardless of the value of $Y$.

2153: We show that $\omega_X$ is a var-model of

2154: $(\neg a \vee \Sigma)$, but not of the other

2155: formula. Extending the model $\omega_X$ with the model

2156: that sets $a$ to $\false$ and $Y$ to any value, we

2157: obtain a model of $(\neg a \vee \Sigma)$ simply

2158: because all clauses in this set contains $\neg a$.

2159: 

2160: Let us now prove that $\omega_X$ is not a var-model

2161: of $(\neg a \vee \Sigma) \cup \{a\}$, \ie, it

2162: cannot be extended

2163: to form a model of $(\neg a \vee \Sigma) \cup \{a\}$.

2164: By the contrary, let $\omega_Y$ be the partial model

2165: of $Y$ such that $\omega_X \omega_Y \omega_a$ satisfies

2166: this formula. Since the formula contains $a$, the

2167: model $\omega_a$ must set $a$ to true. As a result,

2168: the formula can be reduced to $\Sigma$. This implies

2169: that there exists $\omega_Y$ that extends $\omega_X$

2170: to form a model of $\Sigma$, contradicting the

2171: assumption.

2172: 

2173: \end{description}~\qed

2174: 

2175: The following theorem shows the complexity of

2176: var-redundancy of a set of clauses. This problem

2177: has the same complexity of var-redundancy

2178: of a single clause, as in the case of logical

2179: redundancy.

2180: 

2181: \begin{theorem}

2182: 

2183: Checking var-redundancy of a set of clauses

2184: is \P{2}-complete.

2185: 

2186: \end{theorem}

2187: 

2188: \proof Membership follows from the fact that a set

2189: is var-redundant if and only if

2190: $\Pi \backslash \{\gamma\} \qequiv{V} \Pi$ holds

2191: for some clause $\gamma \in \Pi$. These queries can

2192: be done in parallel. Therefore, the problem is in

2193: the same class of the single test, which is in \P{2}.

2194: 

2195: Hardness is proved by showing that

2196: $\forall X \exists Y ~.~ \Sigma$ holds if and only if 

2197: the following set $\Pi$ is var-redundant \wrt\

2198: $V = X \cup B \cup C$, where

2199: $\Sigma=\{\gamma_1,\ldots,\gamma_m\}$. We assume,

2200: without loss of generality, that $\Sigma$ contains

2201: at least two clauses, and it does not contain any

2202: tautological clause.

2203: 

2204: \begin{eqnarray*}

2205: \Pi &=& 

2206: \{\pi\} \cup

2207: \bigcup_{i=1,\ldots,m} \Pi_i

2208: \\

2209: && \mbox{where}

2210: \\

2211: \pi &=&

2212: \neg c_1 \vee \cdots \vee \neg c_m \vee a

2213: \\

2214: \Pi_i &=&

2215: \{c_i \rightarrow \neg a \vee \gamma_i\} \cup

2216: \{\neg a \rightarrow b_i\} \cup

2217: \{l_j \rightarrow b_i ~|~ l_j \in \gamma_i\}

2218: \end{eqnarray*}

2219: 

2220: Each set $\Pi_i$ entails the clause $c_i \rightarrow b_i$

2221: This is indeed the result of resolving all clauses of

2222: $\Pi_i$ together. As a result, $c_i \rightarrow b_i$ is

2223: a consequence of $\Pi$. Being composed of variables of $V$

2224: only, this clause must also be entailed by any

2225: var-equivalent formula.

2226: 

2227: \begin{description}

2228: 

2229: \item[All clauses of $\Pi_i$ are irredundant in $\Pi$.]

2230: This is proved by showing that, removing one clause of

2231: $\Pi_i$ from $\Pi$, a new var-model is created. Since

2232: $\Pi$ entails $c_i \rightarrow b_i$, the following partial

2233: model cannot be extended to form a var-model of $\Pi$,

2234: as it evaluates $c_i$ to $\true$ but $b_i$ to $\false$.

2235: 

2236: \[

2237: \omega_{BC} = \{c_i,\neg b_i\} \cup

2238: \{\neg c_j, b_j ~|~ j \in \{1,\ldots,m\} \backslash i\}

2239: \]

2240: 

2241: We prove that, removing a clause $\delta \in \Pi_i$,

2242: this model can be extended to form a model, that is,

2243: $\omega_{BC}$ can be extended to form a model of

2244: $\Pi \backslash \{\delta\}$. Since $m \geq 2$ by

2245: assumption, $\omega_{BC}$ evaluates a variable

2246: $c_j$ to $\false$, and the clause $\pi$ is therefore

2247: satisfied. The model $\omega_{BC}$ also satisfies all

2248: sets $\Pi_j$ with $j \not= i$. We therefore

2249: only have to prove that, removing a clause

2250: from $\Pi_i$, the model $\omega_{BC}$ can be

2251: extended to form a model of the other clauses of $\Pi_i$.

2252: 

2253: \begin{description}

2254: 

2255: \item[$c_i \rightarrow \neg a \vee \gamma_i$\rm :]

2256: the model $\omega$ with $\omega(a)=\true$ and

2257: $\omega(l_j)=\false$ for any $l_j \in \gamma_i$

2258: is such that

2259: $\omega_{BC}\omega \models \Pi_i \backslash

2260: \{c_i \rightarrow \neg a \vee \gamma_i\}$;

2261: 

2262: \item[$\neg a \rightarrow b_i$\rm :] the model

2263: $\omega$ with $\omega(a)=\false$ and

2264: $\omega(l_j)=\false$ for any $l_j \in \gamma_i$

2265: is such that

2266: $\omega_{BC}\omega \models \Pi_i \backslash

2267: \{\neg a \rightarrow b_i\}$;

2268: 

2269: \item[$l_j \rightarrow b_i$\rm :] we use the

2270: model $\omega$ with $\omega(a)=\true$,

2271: $\omega(l_j)=\true$, and $\omega(l_k)=\false$

2272: for any $l_k \in \gamma_i$ with $k \not= j$.

2273: Indeed,

2274: $\omega_{BC}\omega \models \Pi_i \backslash

2275: \{l_j \rightarrow b_i\}$.

2276: 

2277: \end{description}

2278: 

2279: As a result, all clauses of $\Pi_i$ are irredundant

2280: in $\Pi$. In other words, $\Pi$ is redundant if and

2281: only if $\pi$ is redundant in $\Pi$.

2282: 

2283: \item[Assume $\exists X \forall Y ~.~ \neg \Sigma$.]

2284: We prove that $a$ is irredundant. This is proved by

2285: showing that $\Pi \backslash \{\pi\}$ has a var-model

2286: that $\Pi$ has not. This var-model is $\omega_X\omega_{BC}$,

2287: where $\omega_X$ is the value of $X$ that makes

2288: $\Sigma$ falsified, while $\omega_{BC}$ evaluates

2289: all variables in $B$ and $C$ to $\true$. This model

2290: can indeed by extended to form a model of

2291: $\Pi \backslash \{\pi\}$ by simply setting $a$ to

2292: false. On the other hand, assume that there exists

2293: $\omega_Y\omega_a$ such that

2294: $\omega_X\omega_{BC}\omega_Y\omega_a \models \Pi$.

2295: Since $\pi \in \Pi$, and $\omega_{BC}$ evaluates

2296: all $c_i$'s to $\true$, we have $\omega_a(a)=\true$.

2297: As a result, all clauses $c_i \rightarrow \neg a \vee \gamma_i$

2298: can be simplified to $\gamma_i$. We can therefore

2299: conclude that $\omega_X\omega_Y \models \Sigma$,

2300: contrarily to the assumption.

2301: 

2302: \item[Assume that $\pi$ is irredundant in $\Pi$.]

2303: We show that there exists $\omega_X$ that falsifies $\Sigma$

2304: regardless of the value of $\omega_Y$. By assumption, there

2305: is a var-model of $\Pi \backslash \{\pi\}$ that is not

2306: a var-model of $\Pi$. Let $\omega_X\omega_{BC}$ be

2307: such a var-model.

2308: 

2309: If $\omega_{BC}(c_i)=\false$ for some $i$, then

2310: $\omega_{BC} \models \pi$. Since $\omega_{BC}$ is 

2311: a var-model of $\Pi \backslash \{\pi\}$, there exists

2312: $\omega$ such that

2313: $\omega_{BC}\omega \models \Pi \backslash \{\pi\}$. Since

2314: $\omega_{BC} \models \pi$, we also have that

2315: $\omega_{BC}\omega \models \Pi$, contradicting the

2316: assumption that $\omega_{BC}$ is not a var-model of

2317: $\Pi$. As a result $\omega_{BC}(c_i)=\true$

2318: for all indexes $i$. Since $c_i \rightarrow b_i$ is

2319: entailed by $\Pi_i$ and, therefore, by

2320: $\Pi \backslash \{\pi\}$, we can conclude that

2321: $\omega_{BC}$ evaluates to $\true$ all variables

2322: of $B \cup C$.

2323: 

2324: As a result, all formulae $\neg a \rightarrow b_i$

2325: and $l_j \rightarrow b_i$ are satisfied by

2326: $\omega_{BC}$.

2327: Moreover, $c_i \rightarrow \neg a \vee \gamma_i$

2328: simplifies to $\neg a \vee \gamma_i$, and $\pi$

2329: simplifies to $a$. Since $\omega_X\omega_{BC}$

2330: is not a var-model of $\Pi$, then $\omega_X$ is not

2331: a var-model of $\{\neg a \vee \gamma_i\} \cup \{a\}$,

2332: which is equivalent to $\Sigma$. In other words,

2333: $\omega_X$ cannot be extended to form a model of

2334: $\Sigma$.

2335: 

2336: \end{description}~\qed

2337: 

2338: 

2339: 

2340: %%%%%%%%%%%%% cond %%%%%%%%%%%%%%

2341: \subsection{Conditional Equivalence}

2342: 

2343: Conditional equivalence (or strong equivalence) of

2344: two formulae holds whenever the two formulae are

2345: equivalent and remain so regardless of updates.

2346: This definition depends on how revisions of knowledge

2347: bases are done. If the semantics of revision is

2348: syntax-independent \cite{dala-88},

2349: then conditional and logical equivalence coincide.

2350: On the other hand, objections to the principle of

2351: the irrelevance of syntax have been raised

2352: \cite{fuhr-91,nebe-91,bess-etal-99,wass-01}, and some

2353: revision semantics that depend on the syntax exist. They are

2354: mainly motivated by the fact that the syntactic form in which

2355: a formula is expressed tells more than its set of models.

2356: In this section, we only consider the basic definition

2357: of revision by Fagin, Ullman, and Vardi

2358: \cite{fagi-ullm-vard-83} and by Ginsberg \cite{gins-86}.

2359: 

2360: \begin{definition}

2361: 

2362: $Max(\Pi,\Gamma)$ is the set of the maximal subsets

2363: of $\Pi$ that are consistent with $\Gamma$. Revision

2364: of $\Pi$ with $\Gamma$ is defined as follows:

2365: 

2366: \[

2367: \Pi * \Gamma = \bigvee Max(\Pi,\Gamma)

2368: \]

2369: 

2370: \end{definition}

2371: 

2372: We now give an equivalent characterization of this form of

2373: revision. Given a set of clauses $\Pi$, let $S_\Pi(\omega)$

2374: be the set of clauses of $\Pi$ that are satisfied

2375: by the model $\omega$.

2376: 

2377: \begin{definition}[Satisfied Subset]

2378: 

2379: The subset of $\Pi$ satisfied by $\omega$ is:

2380: 

2381: \[

2382: S_\Pi(\omega) = \{\gamma \in \Pi ~|~ \omega \models \gamma\}

2383: \]

2384: 

2385: \end{definition}

2386: 

2387: The result of revision can be characterize in terms

2388: of the set of models of the result.

2389: 

2390: \begin{lemma}

2391: \label{revision-maximal}

2392: 

2393: The models of $\Pi * \Gamma$ are exactly the

2394: models $\omega$ of $\Gamma$ whose set $S_\Pi(\omega)$

2395: is maximal with respect to set containment.

2396: 

2397: \end{lemma}

2398: 

2399: \proof By definition, only models of $\Gamma$ have

2400: to be taken into account. The set $S_\Pi(\omega)$ is the

2401: set of formulae of $\Pi$ that are satisfied

2402: by $\omega$. Since $\omega$ is a model of $\Gamma$, we have

2403: that $S_\Pi(\omega) \cup \Gamma$ is consistent. As

2404: a result, the only case in which $\omega$ is not a model

2405: of the revision is when this set is not one of those

2406: maximally consistent with $\Gamma$, that is, there

2407: exists a maximal $\Pi'$ such that $\Pi' \cup \Gamma$

2408: is consistent, and $S_\Pi(\omega) \subset \Pi'$. Since

2409: $\Pi' \cup \Gamma$ is consistent, it has models:

2410: let $\omega'$ be a model of $\Pi' \cup \Gamma$. Since

2411: all clauses of $\Pi'$ satisfy $\omega'$, and $\Pi'$

2412: is maximally consistent, we have

2413: $\Pi' = S_\Pi(\omega')$. This proves that $\omega$ is

2414: not a model of $\Pi * \Gamma$ if and only if there

2415: exists $\omega'$ with $S_\Pi(\omega) \subset S_\Pi(\omega')$.~\qed

2416: 

2417: We can now formally give the definition of conditional

2418: redundancy of a clause, and of a set of clauses.

2419: 

2420: \begin{definition}[Conditional Redundancy of a Clause]

2421: 

2422: A clause $\gamma$ is conditionally redundant

2423: in $\Pi$ if and only if $\Pi$ is conditionally

2424: equivalent to $\Pi \backslash \{\gamma\}$.

2425: 

2426: \end{definition}

2427: 

2428: The definition of conditional redundancy of a

2429: whole set can be defined in two different ways:

2430: first, a set is conditionally redundant if it

2431: contains a redundant clause; second, a set

2432: is conditionally redundant if it is equivalent

2433: to one of its proper subsets. We use the first

2434: definition.

2435: 

2436: \begin{definition}[Conditional Redundancy of a set of Clauses]

2437: 

2438: A set of clauses $\Pi$ is conditionally redundant

2439: if and only if it contains a redundant clause.

2440: 

2441: \end{definition}

2442: 

2443: This definition is not equivalent to the other

2444: one. For example, the set

2445: $\Pi = \{a \vee b, a \vee \neg b,

2446: a \vee c, a \vee \neg c\}$ does not contain any

2447: conditionally redundant clause, but is conditionally

2448: equivalent to its subset $\Pi'=\{a \vee b, a \vee \neg b\}$.

2449: This difference is caused by the fact that revision

2450: is a non-monotonic operator: most, but not all,

2451: non-monotonic logics show this phenomena \cite{libe-redu-3}.

2452: 

2453: Lemma~\ref{revision-maximal} tells that a clause is redundant

2454: if and only if its removal modifies the ordering

2455: on models defined by $\subseteq$ on $S_\Pi(.)$. On

2456: the other hand, it may be that two models are incomparable

2457: before the removal of a clause and equal afterwards.

2458: As a result, the difference of the orderings caused

2459: is only a necessary condition to equivalence, not

2460: a sufficient one.

2461: 

2462: \begin{lemma}

2463: \label{conditional-ordering-necessary}

2464: 

2465: If $\gamma$ is irredundant in $\Pi$, then there exists two

2466: models $\omega$ and $\omega'$ such that the containment

2467: relation between $S_\Pi(\omega)$ and $S_\Pi(\omega')$

2468: is different from that between

2469: $S_{\Pi \backslash \{\gamma\}}(\omega)$ and

2470: $S_{\Pi \backslash \{\gamma\}}(\omega')$.

2471: 

2472: \end{lemma}

2473: 

2474: \proof Trivial consequence of Lemma~\ref{revision-maximal}:

2475: if the ordering is the same, then all revision results

2476: are the same.~\qed

2477: 

2478: This condition is however not a sufficient one, in

2479: general: indeed, it may be that the ordering is different

2480: only because two sets that are incomparable becomes

2481: equal. If this is the case, the result of revision is

2482: always the same. On the other hand, such a case is not

2483: possible if the two formulae only differ for one clause.

2484: 

2485: \begin{lemma}

2486: \label{conditional-ordering}

2487: 

2488: $\gamma$ is irredundant in $\Pi$ if and only if

2489: there exists two

2490: models $\omega$ and $\omega'$ such that the containment

2491: relation between $S_\Pi(\omega)$ and $S_\Pi(\omega')$

2492: is different from that between

2493: $S_{\Pi \backslash \{\gamma\}}(\omega)$ and

2494: $S_{\Pi \backslash \{\gamma\}}(\omega')$.

2495: 

2496: \end{lemma}

2497: 

2498: \proof The ``only if'' part is

2499: Lemma~\ref{conditional-ordering-necessary}. We only

2500: have to prove that, if the containment

2501: relation between $S_\Pi(\omega)$ and $S_\Pi(\omega')$

2502: is different from that between

2503: $S_{\Pi \backslash \{\gamma\}}(\omega)$ and

2504: $S_{\Pi \backslash \{\gamma\}}(\omega')$, then

2505: $\gamma$ is irredundant.

2506: 

2507: If both $\omega$ and $\omega'$ satisfy $\gamma$, then

2508: its removal does not change the relationship between

2509: $S_\Pi(\omega)$ and $S_\Pi(\omega')$, as $\gamma$ is

2510: removed from both. On the other hand, if none of these

2511: models satisfy $\gamma$, then the sets $S_\Pi(\omega)$

2512: and $S_\Pi(\omega')$ are not modified at all.

2513: 

2514: The only remaining case is therefore that one of these

2515: two models satisfy $\gamma$ while the other does not.

2516: Without loss of generality, assume that $\omega$

2517: satisfies $\gamma$ while $\omega'$ does not. As an

2518: immediate result, we have that

2519: $S_\Pi(\omega) \not\subseteq S_\Pi(\omega')$, since the

2520: first set contains a clause the other one does not.

2521: Moreover, we have that

2522: 

2523: \begin{eqnarray*}

2524: S_{\Pi \backslash \{\gamma\}}(\omega)

2525: &=&

2526: S_\Pi(\omega) \backslash \{\gamma\}

2527: \\

2528: S_{\Pi \backslash \{\gamma\}}(\omega') &=& S_\Pi(\omega')

2529: \end{eqnarray*}

2530: 

2531: In other words, the only effect of removing $\gamma$

2532: is to remove $\gamma$ from the set of clauses that

2533: are satisfied by $\omega$, while the clauses satisfied

2534: by $\omega'$ are the same.

2535: 

2536: We prove that the inverse containment is not modified

2537: by the removal of $\gamma$. Formally, we prove that

2538: $S_\Pi(\omega') \subseteq S_\Pi(\omega)$ if and only

2539: if $S_{\Pi \backslash \{\gamma\}}(\omega') \subseteq

2540: S_{\Pi \backslash \{\gamma\}}(\omega)$.

2541: 

2542: \begin{enumerate}

2543: 

2544: \item If $S_\Pi(\omega') \subseteq S_\Pi(\omega)$ holds,

2545: using the equations above we have that

2546: $S_{\Pi \backslash \{\gamma\}}(\omega') \subseteq

2547: S_{\Pi \backslash \{\gamma\}}(\omega) \cup \{\gamma\}$.

2548: Since $\gamma \not\in S_{\Pi \backslash \{\gamma\}}(\omega')$,

2549: this is equivalent to

2550: $S_{\Pi \backslash \{\gamma\}}(\omega') \subseteq

2551: S_{\Pi \backslash \{\gamma\}}(\omega)$.

2552: 

2553: \item If

2554: $S_{\Pi \backslash \{\gamma\}}(\omega') \subseteq

2555: S_{\Pi \backslash \{\gamma\}}(\omega)$, by using the

2556: equations above, we have that

2557: $S_\Pi(\omega') \subseteq S_\Pi(\omega) \backslash \{\gamma\}$,

2558: which implies that

2559: $S_\Pi(\omega') \subseteq S_\Pi(\omega)$.

2560: 

2561: \end{enumerate}

2562: 

2563: We can therefore conclude that the only possible

2564: change of relationship between the clauses that

2565: are satisfied by $\omega$ and those satisfied by

2566: $\omega'$ is that 

2567: $S_\Pi(\omega) \not\subseteq S_\Pi(\omega')$

2568: but $S_{\Pi \backslash \{\gamma\}}(\omega) \subseteq

2569: S_{\Pi \backslash \{\gamma\}}(\omega')$, while

2570: the set containment in the other direction is preserved.

2571: 

2572: Let $\Gamma$ be the formula that has $\omega$ and $\omega'$

2573: has its only two models. We prove that the revision

2574: by $\Gamma$ is affected by the presence of $\gamma$. Formally,

2575: we show that $\Pi * \Gamma$ is different from

2576: $\Pi \backslash \{\gamma\} * \Gamma$. We have already shown

2577: that $S_\Pi(\omega) \not\subseteq S_\Pi(\omega')$,

2578: and that the inverse containment is not changed by the

2579: removal of $\gamma$. Since the containment relation

2580: changes by assumption, we also have that

2581: $S_{\Pi \backslash \{\gamma\}}(\omega) \subseteq

2582: S_{\Pi \backslash \{\gamma\}}(\omega')$. Two cases are

2583: possible: either $S_\Pi(\omega') \subseteq S_\Pi(\omega)$

2584: or not. Let us consider each case separately.

2585: 

2586: \begin{itemize}

2587: 

2588: \item

2589: If $S_\Pi(\omega') \subseteq S_\Pi(\omega)$, since

2590: $S_\Pi(\omega) \not\subseteq S_\Pi(\omega')$,

2591: we have $S_\Pi(\omega') \subset S_\Pi(\omega)$. As

2592: a result $\Pi * \Gamma$ has $\omega$ as its only model.

2593: On the other hand,

2594: $S_{\Pi \backslash \{\gamma\}}(\omega) \subseteq

2595: S_{\Pi \backslash \{\gamma\}}(\omega')$. As a result,

2596: $\omega$ and $\omega'$ are evaluated in the same

2597: way by $S_{\Pi \backslash \{\gamma\}}(.)$.

2598: As a result, $\Pi \backslash \{\gamma\} * \Gamma$ has both

2599: of them as models.

2600: 

2601: \item

2602: If $S_\Pi(\omega') \not\subseteq S_\Pi(\omega)$,

2603: since $S_\Pi(\omega) \not\subseteq S_\Pi(\omega')$,

2604: we have that $\omega$ and $\omega'$ are incomparable

2605: in $\Pi$. As a result, $\Pi * \Gamma$ has both of them

2606: as models.

2607: 

2608: On the other hand, we have that

2609: $S_{\Pi \backslash \{\gamma\}}(\omega) \subseteq

2610: S_{\Pi \backslash \{\gamma\}}(\omega')$, and therefore

2611: $S_{\Pi \backslash \{\gamma\}}(\omega) \subset

2612: S_{\Pi \backslash \{\gamma\}}(\omega')$. As a result,

2613: $\omega'$ is strictly preferred over $\omega$ in

2614: $\Pi \backslash \{\gamma\}$. As a result,

2615: $\Pi \backslash \{\gamma\} * \Gamma$ has $\omega'$ as its

2616: only model.

2617: 

2618: \end{itemize}

2619: 

2620: We have therefore proved the following: if the removal

2621: of $\gamma$ changes the relationship between two models

2622: $\omega$ and $\omega'$, then the only possible change

2623: is that $S_\Pi(\omega) \not\subseteq S_\Pi(\omega')$ and

2624: $S_{\Pi \backslash \{\gamma\}}(\omega) \subseteq

2625: S_{\Pi \backslash \{\gamma\}}(\omega')$, while the

2626: inverse containment relationship is not changed. We have

2627: then proved that such a change leads to different

2628: results when $\Pi$ and $\Pi \backslash \{\gamma\}$ are

2629: both revised by the same formula $\Gamma$. As a result,

2630: $\gamma$ is irredundant.~\qed

2631: 

2632: This lemma proves that the irredundancy of a clause

2633: is related to the modification of the set containment

2634: of the sets of clauses that are satisfied by the models.

2635: On the other hand, this condition is only about the

2636: redundancy of a single clause. If we allow removing

2637: two clauses, the ordering can be modified while

2638: conditional equivalence is preserved.

2639: 

2640: \begin{theorem}

2641: \label{cond-one-more-not}

2642: 

2643: The following two sets of clauses are conditionally

2644: equivalent, but the ordering they induce are different,

2645: and all clauses of $\Pi$ are irredundant.

2646: 

2647: \begin{eqnarray*}

2648: \Pi &=&

2649: \{a \vee b, a \vee \neg b,

2650: a \vee c, a \vee \neg c\} \\

2651: \Pi' &=& \{a \vee b, a \vee \neg b\}

2652: \end{eqnarray*}

2653: 

2654: \end{theorem}

2655: 

2656: \proof We prove that $\Pi$ does not contain any

2657: redundant clause. Its symmetry allows proving it

2658: for a single clause only. Let us therefore show

2659: that $a \vee b$ is irredundant. Consider the

2660: following revising formula $\Gamma=\neg a$. The maximal

2661: subsets of $\Pi$ that are consistent with $\Gamma$

2662: are composed of exactly one clause between

2663: $a \vee b$ and $a \vee \neg b$, and one clause

2664: between $a \vee c$ and $a \vee \neg c$. As a

2665: result, $\Pi * \Gamma = \neg a$.

2666: 

2667: Let us now consider $\Pi \backslash \{a \vee b\} * \Gamma$.

2668: The maximal subsets of $\Pi \backslash \{a \vee b\}$

2669: that are consistent with $\neg a$ contains the

2670: clause $a \vee \neg b$, and one clause between

2671: $a \vee c$ and $a \vee \neg c$. As a result, all

2672: maximal subset contains $a \vee \neg b$, which is

2673: therefore in $\Pi \backslash \{a \vee b\} * \Gamma$. We

2674: can therefore conclude that

2675: $\Pi \backslash \{a \vee b\} * \Gamma = \neg a \wedge \neg b$.

2676: Since this is different from $\Pi * \Gamma$, the clause

2677: $a \vee b$ is irredundant in $\Pi$.

2678: 

2679: We now prove that $\Pi'$ is conditionally equivalent

2680: to $\Pi$. Let $\omega$ and $\omega'$ be two models.

2681: If they both satisfy $c$ or they both satisfy

2682: $\neg c$, the set of satisfied clauses are modified

2683: in the same way. On the other hand, if one of them

2684: implies $c$ and the other one implies $\neg c$, then

2685: they are incomparable in $\Pi$, but equal in $\Pi'$.

2686: The only difference is therefore that some pairs of

2687: models are incomparable in $\Pi$ but equal in $\Pi'$.

2688: As a result, the maximal ones are always the same.

2689: 

2690: While $\Pi$ and $\Pi'$ are conditionally equivalent,

2691: there exist two models that are compared

2692: differently in $\Pi$ and $\Pi'$.

2693: Let $\omega$ and $\omega'$ be the models such

2694: that $\omega \models \neg a \wedge \neg b \wedge \neg c$

2695: and $\omega' \models \neg a \wedge \neg b \wedge c$.

2696: The sets $S_\Pi(\omega)$ and $S_\Pi(\omega')$

2697: are not comparable: the first contains $a \vee \neg c$

2698: but not $a \vee c$, while the second contains the second

2699: one but not the first. As a result, the ordering is

2700: changed.~\qed

2701: 

2702: The following lemma makes the statement of

2703: Lemma~\ref{conditional-ordering} more precise: not

2704: only there is a pair of models whose ordering is

2705: modified: this ordering is modified in a very

2706: specific way.

2707: 

2708: \begin{lemma}

2709: \label{conditional-onemore}

2710: 

2711: $\gamma$ is conditionally irredundant in $\Pi$ if and

2712: only if there exists two models $\omega$ and $\omega'$

2713: such that:

2714: 

2715: \[

2716: S_\Pi(\omega) \backslash S_\Pi(\omega') = \{\gamma\}

2717: \]

2718: 

2719: \end{lemma}

2720: 

2721: \proof If two such model exists, then we have that

2722: $S_\Pi(\omega) \not\subseteq S_\Pi(\omega')$, since

2723: $S_\Pi(\omega)$ contains a clause that is not in

2724: $ S_\Pi(\omega')$; on the other hand, since $\gamma$

2725: is the only clause that is in  $S_\Pi(\omega)$ but not

2726: in $S_\Pi(\omega')$, removing it from both sets leads to

2727: $S_{\Pi \backslash \{\gamma\}}(\omega) \subseteq

2728: S_{\Pi \backslash \{\gamma\}}(\omega')$. This result

2729: tells us that the removal of $\gamma$ modifies the

2730: relationship between the set of clauses that are

2731: satisfied by $\omega$ and by $\omega'$. By

2732: Lemma~\ref{conditional-ordering}, this implies that

2733: $\gamma$ is irredundant.

2734: 

2735: \iffalse

2736: The formal

2737: proof, however, requires showing that such a change

2738: modifies the maximal models for some updating formula $\Gamma$.

2739: 

2740: Let $\Gamma$ be the formula that has $\omega$ and

2741: $\omega'$ as its only two models. We show that

2742: revising $\Pi$ with $\Gamma$ is affected by the presence

2743: of $\gamma$. Two cases are possible: either

2744: $S_\Pi(\omega') \subset S_\Pi(\omega)$ or

2745: $S_\Pi(\omega')$ and $S_\Pi(\omega)$ are incomparable.

2746: In both cases, the removal of $\gamma$ does not affect

2747: the set of clauses that are satisfied by $\omega'$,

2748: as this model does not satisfy $\gamma$. Formally,

2749: $S_\Pi(\omega') = S_{\Pi \backslash \{\gamma\}}(\omega')$.

2750: 

2751: If $S_\Pi(\omega') \subset S_\Pi(\omega)$,

2752: then $\omega$ is the only model of $\Pi * \Gamma$.

2753: Since $\gamma$ is the only clause that $S_\Pi(\omega)$

2754: has more than $S_\Pi(\omega')$ its removal leads to

2755: $S_{\Pi \backslash \{\gamma\}}(\omega) =

2756: S_{\Pi \backslash \{\gamma\}}(\omega')$. As a result,

2757: $\Pi \backslash \{\gamma\} * \Gamma$ has both models

2758: $\omega$ and $\omega'$, while only $\omega$ is

2759: a model of $\Pi * \Gamma$. This proves that $\gamma$ is

2760: irredundant.

2761: 

2762: If $S_\Pi(\omega)$ and $S_\Pi(\omega')$ are incomparable,

2763: then $\Pi * \Gamma$ has both models $\omega$ and $\omega'$.

2764: On the other hand, since $\gamma$ is the only clause

2765: that is satisfied by $\omega$ but not by $\omega'$,

2766: removing it from $S_\Pi(\omega)$ leads to a proper

2767: subset of $S_\Pi(\omega')$, that is,

2768: $S_{\Pi \backslash \{\gamma\}}(\omega) \subset

2769: S_{\Pi \backslash \{\gamma\}}(\omega')$. As a result,

2770: $\Pi \backslash \{\gamma\} * \Gamma$ has $\omega'$ as its

2771: only model. This proves that $\gamma$ is not redundant

2772: in this case either.

2773: 

2774: \fi

2775: 

2776: Let us assume that $\gamma$ is irredundant. By

2777: Lemma~\ref{conditional-ordering-necessary},

2778: there are two models $\omega$ and $\omega'$ such that

2779: the containment relation between $S_\Pi(\omega)$

2780: and $S_\Pi(\omega')$ is affected by the presence of

2781: $\gamma$ in $\Pi$.

2782: If $\omega$ and $\omega'$ evaluate

2783: $\gamma$ in the same way (\ie, either both or none

2784: of them satisfy it), then removing $\gamma$ modifies their

2785: sets $S_\Pi(.)$ in the same way (either $\gamma$ is

2786: removed from both, or it is not in either already.)

2787: 

2788: As a result, either $\omega$ or $\omega'$ satisfy

2789: $\gamma$, but not both. Without loss of generality,

2790: we can assume that $\omega$ is the model that

2791: satisfy $\gamma$. As a result, we have that

2792: $\gamma \in S_\Pi(\omega) \backslash S_\Pi(\omega')$.

2793: We therefore only have to prove that no other

2794: clause is in this difference. On the converse, assume

2795: that $S_\Pi(\omega) \backslash S_\Pi(\omega')$

2796: contains another clause $\gamma'$, that is

2797: $\{\gamma, \gamma'\} \subseteq S_\Pi(\omega) \backslash S_\Pi(\omega')$.

2798: The only effect of removing $\gamma$ is that $\gamma$

2799: disappears from the set of clauses satisfied by

2800: $\omega$; on the other hand, $\gamma'$ is still

2801: there. As a result, the relationship between the

2802: set of satisfied clauses remains the same. Formally,

2803: two cases are possible: either $\omega$ satisfies

2804: all clauses that are satisfied by $\omega'$, or

2805: $\omega'$ satisfies some clauses more. In the first

2806: case, the removal of $\gamma$ does not change the

2807: relationship because $\omega$ still satisfies all

2808: clauses of $\omega'$ and $\gamma'$. In the second

2809: case, the sets of satisfied clauses are still

2810: incomparable, as $\omega'$ satisfies the same clauses,

2811: while $\omega$ satisfies $\gamma'$.~\qed

2812: 

2813: We have now all technical tools to prove the

2814: complexity of checking redundancy of a single

2815: clause in a set.

2816: 

2817: \begin{theorem}

2818: \label{theorem-conditional-one}

2819: 

2820: Checking whether $\gamma$ is conditionally redundant

2821: in $\Pi$ is \conp-complete.

2822: 

2823: \end{theorem}

2824: 

2825: \proof Membership: a clause is redundant if and only

2826: if there exists two models such that their ordering

2827: is affected by the presence of the clause.

2828: 

2829: Hardness: the set of clauses $\Pi$ is satisfiable if

2830: and only if the clause $a$ is conditionally redundant

2831: in $\Sigma=(a \vee \Pi) \cup \{a\}$, where

2832: $a \vee \Pi$ is a shorthand for

2833: $\{a \vee \gamma ~|~ \gamma \in \Pi\}$. We divide the proof

2834: in two parts: first, we consider the case in which $\Pi$

2835: is satisfiable, and prove that $a$ is irredundant;

2836: second, we show that the irredundancy of $a$ implies the

2837: satisfiability of $\Pi$.

2838: 

2839: If $\Pi$ is satisfiable, it has a model $\omega_X$.

2840: We show that $\gamma$ is irredundant in $\Sigma$ by

2841: considering two models: the first one is $\omega$,

2842: which is obtained by adding the evaluation $a=\false$ to

2843: $\omega_X$; the second one is $\omega_T$, the model

2844: that sets all variables to $\true$. The first model

2845: satisfies all clauses but $a$; the second model

2846: satisfies all clauses. As a result, we have that

2847: $a$ is the only clause satisfied by $\omega_T$ that

2848: is not satisfied by $\omega$, that is:

2849: $S_\Sigma(\omega_T) \backslash S_\Sigma(\omega) = \{a\}$.

2850: By Lemma~\ref{conditional-onemore}, this implies that

2851: $a$ is irredundant.

2852: 

2853: Let us now assume that $a$ is irredundant. By

2854: Lemma~\ref{conditional-onemore},

2855: $S_\Sigma(\omega) \backslash S_\Sigma(\omega')$

2856: is equal to $\{a\}$ for some pair of models

2857: $\omega$ and $\omega'$. This condition implies that

2858: $\omega$ satisfies $a$ while $\omega'$ does not.

2859: Since $\omega$ satisfies $a$ we have that

2860: $S_\Sigma(\omega)=\Sigma$ since all clauses of $\Sigma$

2861: contains $a$. As a result,

2862: $S_\Sigma(\omega') = \Sigma \backslash \{a\}$, that

2863: is, $\omega'$ satisfies all clauses of $a \vee \Pi$.

2864: Since $\omega'(a)=\false$, the model $\omega'$ satisfies

2865: all clauses of $\Pi$.~\qed

2866: 

2867: We now prove that checking whether a formula

2868: contains a redundant clause is \conp-complete

2869: as well. Note that the redundancy of a formula

2870: is defined as the presence of a redundant clause

2871: in the set, and not as the property of being

2872: equivalent to a proper subset. These two definitions

2873: are not equivalent, as shown by

2874: Theorem~\ref{cond-one-more-not}.

2875: 

2876: \begin{theorem}

2877: \label{theorem-conditional-all}

2878: 

2879: Checking redundancy (\ie, presence of a redundant

2880: clause) of a set of clauses is \conp-complete.

2881: 

2882: \end{theorem}

2883: 

2884: \proof Membership is proved as usual: we have to

2885: check the redundancy of some clause; these tests

2886: can be done in parallel, and therefore the whole

2887: problem is in \conp.

2888: 

2889: Hardness is proved as follows: we prove that the clause

2890: $a$ is redundant in the following set $\Sigma$ if and

2891: only if $\Pi$ is unsatisfiable:

2892: 

2893: \[

2894: \Sigma =

2895: \{\neg c_i \vee a \vee \gamma_i ~|~ \gamma_i \in \Pi \} \cup

2896: \{c_i \vee a ~|~ \gamma_i \in \Pi \} \cup

2897: \{a\}

2898: \]

2899: 

2900: We indeed prove the following: first, all clauses but $a$

2901: are irredundant. Second, that $a$ is redundant if and only

2902: if $\Pi$ is satisfiable.

2903: 

2904: \begin{description}

2905: 

2906: \item[All clauses of $\Sigma \backslash \{a\}$ are irredundant.]

2907: This is proved by showing, for each of them, a possible

2908: revising formula $\Gamma$ such that $\Sigma * \Gamma$ is different

2909: than $\Sigma \backslash \{\delta\} * \Gamma$ for each clause

2910: $\delta$ of $\Sigma$ that is not $a$.

2911: 

2912: \begin{description}

2913: 

2914: \item[$\neg c_i \vee a \vee \gamma_i$\rm .] The formula

2915: is $\Gamma=\neg a \wedge c_i \wedge \{\neg c_j ~|~ j \not= i \}$.

2916: This formula satisfies $c_i \vee a$ and all clauses

2917: $\neg c_j \vee a \vee \gamma_j$, and falsifies $a$ and

2918: all clauses $c_j \vee a$. As a result, the only clause

2919: that is not satisfied neither contradicted is

2920: $\neg c_i \vee a \vee \gamma_i$. As a result, the result

2921: of the revision entails $\gamma_i$ if and only if this clause

2922: is present.

2923: 

2924: \item[$c_i \vee a$\rm .] We use the formula

2925: $\Gamma = \neg a \wedge \{\neg c_j ~|~ j \not= i\} \wedge \gamma_i$.

2926: This formula falsifies $a$, all clauses $c_j \vee a$

2927: with $j \not= i$, and implies the clause

2928: $\neg c_i \vee a \vee \gamma_i$ because of $\gamma_i$,

2929: and all clauses $\neg c_i \vee a \vee \gamma_j$ for any

2930: $j \not= i$ because $\Gamma \models \neg c_j$. As a result,

2931: the only clause that is not falsifies nor entailed is

2932: $c_i \vee a$. Its presence is needed to allow deriving

2933: $\neg c_i$ from the revised theory.

2934: 

2935: \end{description}

2936: 

2937: \item[If $\Pi$ is satisfiable $a$ is irredundant.] This

2938: is proved by showing a revising formula that makes $a$

2939: needed for the entailment of some formulae. Namely,

2940: since $\Pi$ is satisfiable it has a model $\omega$.

2941: Let $\Gamma$ be defined as follows:

2942: 

2943: \[

2944: \Gamma = \{c_i ~|~ \gamma_i \in \Pi \} \cup

2945: \{x_i ~|~ \omega(x_i) = \true \} \cup

2946: \{\neg x_i ~|~ \omega(x_i) = \false \}

2947: \]

2948: 

2949: In words, we set all $c_i$'s to $\true$, and give to any

2950: $x_i$ the sign that is in the model $\omega$. This formula

2951: is clearly satisfiable. Moreover, it is almost complete,

2952: since the only variable that is not forced to have a specific

2953: value is $a$. Moreover, $\Gamma$ implies all clauses:

2954: $\neg c_i \vee a \vee \gamma_i$ is implied because $\omega$

2955: satisfies all clauses $\gamma_i$, while $c_i \vee a$ is

2956: entailed because $\Gamma$ contains $c_i$. On the other hand, $a$

2957: is not falsified nor it is entailed. As a result, the presence

2958: of $a$ in the result of revision is related to its presence

2959: in the original theory.

2960: 

2961: \item[If $a$ is irredundant, $\Pi$ is satisfiable.] This

2962: is proved by using the characterization of irredundancy

2963: provided by Lemma~\ref{conditional-onemore}: since $a$

2964: is irredundant, there exists two models $\omega$ and

2965: $\omega'$ such that:

2966: 

2967: \[

2968: S_\Sigma(\omega) \backslash S_\Sigma(\omega') = \{a\}

2969: \]

2970: 

2971: Therefore, $\omega \models a$ and $\omega' \not\models a$.

2972: We can now proceed by using the following rules:

2973: 

2974: \begin{enumerate}

2975: 

2976: \item every clause but $a$ that is satisfied by $\omega$

2977: is also satisfied by $\omega'$ (otherwise $a$ would not

2978: be the only clause that is satisfied by $\omega$ but

2979: not by $\omega'$);

2980: 

2981: \item every clause that is not satisfied by $\omega'$

2982: is not satisfied by $\omega$ as well (same reason);

2983: 

2984: \item if a model satisfies some clauses, it also

2985: satisfies all their consequences.

2986: 

2987: \end{enumerate}

2988: 

2989: This leads to the pictorial proof of

2990: Figure~\ref{condred-sat}.

2991: 

2992: \begin{figure}[!htb]

2993: \begin{center}

2994: %%%%%%%%%%%%% condred-sat.latex %%%%%%%%%%%%%%

2995: \setlength{\unitlength}{4144sp}%

2996: %

2997: \begingroup\makeatletter\ifx\SetFigFont\undefined%

2998: \gdef\SetFigFont#1#2#3#4#5{%

2999:   \reset@font\fontsize{#1}{#2pt}%

3000:   \fontfamily{#3}\fontseries{#4}\fontshape{#5}%

3001:   \selectfont}%

3002: \fi\endgroup%

3003: \begin{picture}(6268,6064)(-675,-6149)

3004: \thinlines

3005: \put(3691,-331){\vector( 0,-1){540}}

3006: \put(1171,-331){\vector( 0,-1){990}}

3007: \put(1801,-1681){\vector( 2,-1){1350}}

3008: \put(721,-196){\line(-1, 0){720}}

3009: \put(  1,-196){\line( 0,-1){4050}}

3010: \put(  1,-4246){\vector( 1, 0){315}}

3011: \put(1801,-4381){\vector( 2,-1){1170}}

3012: \put(4771,-1006){\line( 1, 0){810}}

3013: \put(5581,-1006){\line( 0,-1){5040}}

3014: \put(5581,-6046){\vector(-1, 0){1395}}

3015: \put(4771,-1006){\line( 0,-1){2520}}

3016: \put(4771,-3526){\vector(-1, 0){585}}

3017: \put(4366,-2536){\vector( 1, 0){405}}

3018: \put(4231,-1006){\vector( 1, 0){540}}

3019: \put(3691,-3661){\line( 0,-1){540}}

3020: \put(3691,-4201){\vector( 1, 0){1890}}

3021: \put(4501,-5146){\vector( 1, 0){1080}}

3022: \put(1171,-241){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega \models a$}}}

3023: \put(3691,-241){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega' \not\models a$}}}

3024: \put(3691,-1051){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega' \models \neg a$}}}

3025: \put(1171,-1591){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega \models c_i \vee a$}}}

3026: \put(3691,-2581){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega' \models c_i \vee a$}}}

3027: \put(3691,-3571){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega' \models c_i$}}}

3028: \put(1171,-4291){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega \models \neg c_i \vee a \vee \gamma_i$}}}

3029: \put(3691,-5191){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega' \models \neg c_i \vee a \vee \gamma_i$}}}

3030: \put(3691,-6091){\makebox(0,0)[b]{\smash{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}$\omega' \models \gamma_i$}}}

3031: \end{picture}

3032: 

3033: \end{center}

3034: \caption{If $a$ is irredundant then $\Pi$ is satisfiable}

3035: \label{condred-sat}

3036: \end{figure}

3037: 

3038: In words, the proofs proceeds as follows, using the

3039: rules above and the fact that $\omega \models a$ and

3040: $\omega' \not\models a$. The latter is equivalent to

3041: $\omega' \models \neg a$. Since $\omega \models a$ we

3042: have that $\omega \models c_i \vee a$. As a result,

3043: the same clause is satisfied by $\omega'$, that is,

3044: $\omega' \models c_i \vee a$. Since $\omega' \models \neg a$,

3045: we can conclude that $\omega' \models c_i$ for all

3046: indexes $i$.

3047: 

3048: Since $\omega \models a$, we also have that

3049: $\omega \models \neg c_i \vee a \vee \gamma_i$. As

3050: a result, $\omega'$ satisfies the same clause,

3051: that is $\omega' \models \neg c_i \vee a \vee \gamma_i$.

3052: But we have already proved that $\omega' \models \neg a$

3053: and that $\omega' \models c_i$. As a result, we have

3054: that $\omega' \models \gamma_i$ for all $i$. This

3055: proves that $\omega'$ is a model of all clauses

3056: $\gamma_i \in \Pi$. As a result, $\Pi$ is satisfiable.

3057: 

3058: \end{description}

3059: 

3060: We can therefore conclude that all clauses of $\Sigma$

3061: but $a$ are irredundant, and that $a$ is redundant if

3062: and only if $\Pi$ is unsatisfiable. As a result, $\Sigma$

3063: is redundant if and only if $\Pi$ is unsatisfiable.~\qed

3064: 

3065: 

3066: \let\subsectionnewpage=\relax

3067: 

3068: 

3069: %%%%%%%%%%%%% conc %%%%%%%%%%%%%%

3070: \section{Conclusions}

3071: 

3072: We have presented a study of the semantical and

3073: computational properties of concepts related to the

3074: redundancy of CNF propositional formulae. Namely, we have

3075: considered the problem of checking whether a formula is

3076: redundant and some problems related to removing

3077: redundancy from it. The computational analysis has shown

3078: that checking redundancy is \conp-complete. We have then

3079: defined an \ies\  as an irredundant equivalent

3080: subset of a formula, and studied some problems

3081: related to \ies's: checking, size, uniqueness, and

3082: membership of clauses to some or all \ies's.

3083: All problems have been given an exact characterization

3084: within the polynomial hierarchy, that is,

3085: we have found classes these problems are complete for.

3086: The problem of redundancy has also been studied for the

3087: case of two alternative forms of equivalence based on

3088: particular sets of possible queries.

3089: 

3090: Some problems are still open. Namely, irredundancy is only

3091: one way of defining minimal representation of a formula,

3092: but other ones exist. In the Horn case, several

3093: different definitions of minimality have been used, both

3094: by Meier~\cite{maie-80} and by Ausiello et

3095: al.~\cite{ausi-etal-86}, including irredundancy and

3096: number of occurrences of literals. In the

3097: general (non-Horn) case, only the number of occurrences

3098: of literals (and, in this paper, irredundancy) have been

3099: considered. An open problem is whether the other notions

3100: of minimality used in the Horn case make sense in the

3101: general case as well.

3102: 

3103: Some other problems have not been considered in this paper,

3104: and are analyzed in two other papers. In the first

3105: one \cite{libe-redu-2}, the complexity of the problem of

3106: redundancy has been analyzed for the case of Horn and

3107: 2CNF formulae. The analysis of 2CNF, in particular, has

3108: shown a very interesting pattern: while the properties of

3109: redundancy and irredundancy are different depending on

3110: whether the formula implies some literals or not, a concept

3111: of {\em acyclicity} makes often the difference between

3112: tractability and intractability. In the other paper

3113: \cite{libe-redu-3} some non-classical logics have been

3114: considered: non-monotonic logics, multi-valued logics,

3115: and logics for reasoning about actions. An interesting

3116: issue of non-classical logics is that equivalence can be

3117: defined in different ways, and that the irredundancy of

3118: all parts of a knowledge base does not always imply the

3119: irredundancy of the knowledge base.

3120: 

3121: \comment

3122: 

3123: Open problem:

3124:   decide the existence of an equivalent subset of size <= k,

3125:   where the size is number of occurrence of literals

3126: 

3127: \endcomment

3128: 

3129: 

3130: 

3131: %%%%%%%%%%%%% acks %%%%%%%%%%%%%%

3132: \subsection*{Acknowledgments}

3133: 

3134: \iffalse

3135: 

3136: Many thanks to Marco Schaerf for his comments

3137: on a previous version of this paper, and to the

3138: anonymous reviewers for their very detailed

3139: comments.

3140: {\bf Thanks to: Chopra, Sattler, Furbach,

3141: Van Harmelen, Farinas del Cerro?}

3142: 

3143: \else

3144: 

3145: [...]

3146: 

3147: \fi

3148: 

3149: 

3150: 

3151: % \def\sectionnewpage{\vskip 3cm}

3152: % appendix

3153: % input{othe}

3154: 

3155: \bibliographystyle{alpha}

3156: \begin{thebibliography}{BGMS99}

3157: 

3158: \bibitem[ADS86]{ausi-etal-86}

3159: G.~Ausiello, A.~D'Atri, and D.~Sacc{\`a}.

3160: \newblock Minimal representation of directed hypergraphs.

3161: \newblock {\em {SIAM} Journal on Computing}, 15(2):418--431, 1986.

3162: 

3163: \bibitem[BG82]{blas-gure-82}

3164: A.~Blass and Y.~Gurevich.

3165: \newblock On the unique satisfiability problem.

3166: \newblock {\em Information and Control}, 55(1--3):80--88, 1982.

3167: 

3168: \bibitem[BGMS99]{bess-etal-99}

3169: B.~Bessant, E.~Gr\'egoire, P.~Marquis, and L.~Sa{\"\i}s.

3170: \newblock Iterated syntax-based revision in a non-monotonic setttings.

3171: \newblock In M.-A. Williams and H.~Rott, editors, {\em Frontiers of belief

3172:   revision}. Kluwer Academic Publisher, 1999.

3173: 

3174: \bibitem[CD97]{cado-doni-97}

3175: M.~Cadoli and F.~M. Donini.

3176: \newblock A survey on knowledge compilation.

3177: \newblock {\em {AI} Communications---The European Journal on Artificial

3178:   Intelligence}, 10:137--150, 1997.

3179: 

3180: \bibitem[CDLS99]{cado-etal-99}

3181: M.~Cadoli, F.~M. Donini, P.~Liberatore, and M.~Schaerf.

3182: \newblock The size of a revised knowledge base.

3183: \newblock {\em Artificial Intelligence}, 115(1):25--64, 1999.

3184: 

3185: \bibitem[CDSS97]{cado-etal-97-c}

3186: M.~Cadoli, F.~M. Donini, M.~Schaerf, and R.~Silvestri.

3187: \newblock On compact representations of propositional circumscription.

3188: \newblock {\em Theoretical Computer Science}, 182:183--202, 1997.

3189: 

3190: \bibitem[Dal88]{dala-88}

3191: M.~Dalal.

3192: \newblock Investigations into a theory of knowledge base revision: Preliminary

3193:   report.

3194: \newblock In {\em Proceedings of the Seventh National Conference on Artificial

3195:   Intelligence (AAAI'88)}, pages 475--479, 1988.

3196: 

3197: \bibitem[Fuh91]{fuhr-91}

3198: A.~Fuhrmann.

3199: \newblock Theory contraction through base contraction.

3200: \newblock {\em Journal of Philosophical Logic}, 20:175--203, 1991.

3201: 

3202: \bibitem[FUV83]{fagi-ullm-vard-83}

3203: R.~Fagin, J.~D. Ullman, and M.~Y. Vardi.

3204: \newblock On the semantics of updates in databases.

3205: \newblock In {\em Proceedings of the Second ACM SIGACT SIGMOD Symposium on

3206:   Principles of Database Systems (PODS'83)}, pages 352--365, 1983.

3207: 

3208: \bibitem[GF93]{gott-ferm-93}

3209: G.~Gottlob and C.~G. {Ferm\"uller}.

3210: \newblock Removing redundancy from a clause.

3211: \newblock {\em Artificial Intelligence}, 61:263--289, 1993.

3212: 

3213: \bibitem[Gin86]{gins-86}

3214: M.~L. Ginsberg.

3215: \newblock Conterfactuals.

3216: \newblock {\em Artificial Intelligence}, 30:35--79, 1986.

3217: 

3218: \bibitem[Gin88]{gins-88-a}

3219: A.~Ginsberg.

3220: \newblock Knowledge base reduction: A new approach to checking knowledge bases

3221:   for inconsistency \& redundancy.

3222: \newblock In {\em Proceedings of the Seventh National Conference on Artificial

3223:   Intelligence (AAAI'88)}, pages 585--589, 1988.

3224: 

3225: \bibitem[Got95]{gott-95-jacm}

3226: G.~Gottlob.

3227: \newblock {NP} trees and {C}arnap's modal logic.

3228: \newblock {\em Journal of the {ACM}}, 42(2):421--457, 1995.

3229: 

3230: \bibitem[HK93]{hamm-koga-93}

3231: P.~Hammer and A.~Kogan.

3232: \newblock Optimal compression of propositional {H}orn knowledge bases:

3233:   Complexity and approximation.

3234: \newblock {\em Artificial Intelligence}, 64(1):131--145, 1993.

3235: 

3236: \bibitem[HW97]{hema-wech-97}

3237: E.~Hemaspaandra and G.~Wechsung.

3238: \newblock The minimization problem for {Boolean} formulas.

3239: \newblock In {\em Proceedings of the Thirtyeighth Annual Symposium on the

3240:   Foundations of Computer Science (FOCS'97)}, pages 575--584, 1997.

3241: 

3242: \bibitem[Liba]{libe-redu-2}

3243: P.~Liberatore.

3244: \newblock Redundancy in logic {II}: {2-CNF} and {H}orn propositional formulae.

3245: \newblock Forthcoming.

3246: 

3247: \bibitem[Libb]{libe-redu-3}

3248: P.~Liberatore.

3249: \newblock Redundancy in logic {III}: Non-classical logics.

3250: \newblock Forthcoming.

3251: 

3252: \bibitem[Lib00]{libe-00}

3253: P.~Liberatore.

3254: \newblock Compilability and compact representations of revision of horn

3255:   knowledge bases.

3256: \newblock {\em ACM Transactions on Computational Logic}, 1(1):131--161, 2000.

3257: 

3258: \bibitem[LLM03]{lang-etal-03}

3259: J.~Lang, P.~Liberatore, and P.~Marquis.

3260: \newblock Propositional independence: Formula-variable independence and

3261:   forgetting.

3262: \newblock {\em Journal of Artificial Intelligence Research}, 2003.

3263: \newblock To Appear.

3264: 

3265: \bibitem[LPV01]{lifs-pear-valv-01}

3266: V.~Lifschitz, D.~Pearce, and A.~Valverde.

3267: \newblock Strongly equivalent logic programs.

3268: \newblock {\em {ACM} Transactions on Computational Logic}, 2(4):526--541, 2001.

3269: 

3270: \bibitem[LZ]{libe-zhao-03}

3271: P.~Liberatore and X.~Zhao.

3272: \newblock Strong equivalence in propositional logic.

3273: \newblock Forthcoming.

3274: 

3275: \bibitem[Mai80]{maie-80}

3276: D.~Maier.

3277: \newblock Minimum covers in relational database model.

3278: \newblock {\em Journal of the {ACM}}, 27(4):664--674, 1980.

3279: 

3280: \bibitem[MS72]{meye-stoc-72}

3281: A.~Meyer and L.~Stockmeyer.

3282: \newblock The equivalence problem for regular expressions with squaring

3283:   requires exponential space.

3284: \newblock In {\em Proceedings of the Thirteenth Annual Symposium on Switching

3285:   and Automata Theory (FOCS'72)}, pages 125--129, 1972.

3286: 

3287: \bibitem[Neb91]{nebe-91}

3288: B.~Nebel.

3289: \newblock Belief revision and default reasoning: Syntax-based approaches.

3290: \newblock In {\em Proceedings of the Second International Conference on the

3291:   Principles of Knowledge Representation and Reasoning (KR'91)}, pages

3292:   417--428, 1991.

3293: 

3294: \bibitem[SM73]{stoc-meye-73}

3295: L.~J. Stockmeyer and A.~R. Meyer.

3296: \newblock Word problems requiring exponential time.

3297: \newblock In {\em Proceedings of the Fifth ACM Symposium on Theory of Computing

3298:   (STOC'73)}, pages 1--9, 1973.

3299: 

3300: \bibitem[SS97]{schm-snyd-97}

3301: J.~Schmolze and W.~Snyder.

3302: \newblock Detecting redundant production rules.

3303: \newblock In {\em Proceedings of the Fourteenth National Conference on

3304:   Artificial Intelligence (AAAI'97)}, pages 417--423, 1997.

3305: 

3306: \bibitem[Uma98]{uman-97}

3307: C.~Umans.

3308: \newblock The minimum equivalent {DNF} problem and shortest implicants.

3309: \newblock In {\em Proceedings of the Thirtynineth Annual Symposium on the

3310:   Foundations of Computer Science (FOCS'98)}, pages 556--563, 1998.

3311: 

3312: \bibitem[Was01]{wass-01}

3313: R.~Wassermann.

3314: \newblock On structured belief bases.

3315: \newblock In M.-A. Williams and H.~Rott, editors, {\em Frontiers in Belief

3316:   Revision}. Kluwer Academic Publisher, 2001.

3317: 

3318: \end{thebibliography}

3319: 

3320: \end{document}

3321: 

3322: