Schlechta K. Nonmonotonic Logics: Basic Concepts, Results, and Techniques
Подождите немного. Документ загружается.
114 CHAPTER 3. DEFAULTS AS GENERALIZED QUANTIFfERS
Let TI := U{T~ : ? < fl}, fl large enough, and Tll C_ T! be the set of FOL-
formulas of Tf. By FOL-completeness, Tf has a model M with universe U, where
each u E U is denoted by some c~.
Next, we define Af(U).
Case 1: T/contains no Vzg(x): Set AY(U) := {U}.
Case 2: Otherwise. Let Vzg(x) be in TI, and its children be ?xg(x), ?x(O A
9i)(x), i E I (with Vyr / &yr E T'), so there are 9(c~), (r162 E TI.
Let Xv~r :-- {c~} U {%; : i E/} (we identify the c~ with their interpretation),
and set N'(U) := {V C U: Xv.~r c_ V for some Vx~b(z) E Tr}. Obviously, for
Vx~(x), Vxlbr(x) E T/, Xw~(~) M Xv=r :~ 0, as they have the common child
?x(r h r so N'(U) is a .M-system.
It remains to show that T holds in A4 :=< M,N'(U) > . We show by induction
on the complexity of r that all r E Tf hold in 3/f.
Theorem 3.12 The axioms given in Definition 3.7 are sound and complete for
the semantics of Definition 3.5, "they capture the H-semantics of V."
Proof Let T ~: r Then there is a model M, such that M ~ T A --r Thus,
Con(T A -,r so T V r The other direction is analogous. []
Extension to normal defaults with prerequisites
Definition 3.13 Call N'+(M) =< N(N) : N C M > a ..~/+-system over M iff
for each N C M H(N) is a N-system over N. (It suffices to consider the definable
subsets of M.)
Definition 3.14 Extend the logic of first-order predicate calculus by adding the
axiom schemata
1. a. we(x) ~ W(z = x): r
b. V~(~(~) ~ ,-(~)) A V:~,(x): r -, V,:~-(~) : r
2. Vxr @(x) A Vx(r A %b(x) -~. @(x)) ~;Vx~(z): @(x),
3. Sxr A we(x): r -, ~Vxr :
~r
4. w(r ~ V,(~)) -, we(x): ,e(~:) -, [?~.r ~ ?x(r a ~(x))],
5. &xr r ~ -~w:r
6. Vxr : ,~,(=) ~ rye(y): w(y) (under the usual caveat for substit,,tion)
(for all r ~, ~, ~, ~).
Lemma 3.15 The following are derivabIe:
a) the axioms of Definition 3.7, and the formulae of Lemma 3.8 (via the above
Definition 3.i4 i.a. and the corresponding relativized versions),
b) the relativized versions of Lemma 3.8, where the existential statements have
to be weakened by an existential assumption as in Definition 3.14, 4. []
3.2. DEFAULTS AS GENERALIZED QUANTIFIERS 115
Definition 3.16 Let Z: be a first-order language, and M a s Let
Af+(M) be a N'+-system over M.
Define < M,N'+(M) > ~ r for any formula inductively as usual, with the addi-
tional induction steps:
1. < M,N'+(M) > ~ Vxr iff there is A E N'(M) such that ga E A (<
M,N'+(M) > D r
2. < M,N'+(M) > ~ &xr iff {a E M: < M,N'+(M) > ~ -~r r A/'(M),
3. < M,N'+(M) > ~ Vzr : ~b(x) iff there is d E N'({x :< M,N'+(M) >~
r such that Va E A (< M,Y+(M) > D ~b[a]),
4. < M,N'+(M) > ~ &xr : ~b(z) iff {a E M: < M,N'+(M) > ~ r
r N'({z :< M,N'+(M) >~ r
Theorem 3.17 The axioms of Definition 3.14 capture N "+ -semantics of V.
Extension to N'-families
So far, we can describe normal cases and the classical situation. We would like
to generalize now to X-families, sequences of N'-systems of increasing strength,
i.e. "approaching" hard=classical information. For a motivation, the reader is
referred to a semantics for defensible inheritance, discussed in [Sch90].
Definition 3.18 1) Let ~/be any ordinal. Call < N}(c) : i < 7 >, Af/(c) _C P(c)
a N'-family over ciff
a. c E N~i(c) for all i,
b. aEH~(c),aCbCc--,bE~(c)forall/<%
c. < H~(c): i < ~, > is decreasing, i.e. a E Hi(c),j < i --+ a E H3(c),
d. a E H/(c), b E N'j(c) --+ a n b -/(~ for all i,j, if c r {a.
2) Call N'+(M) =< N'(N) : N _C M > a N'+-family over M iff for each N C M
A/'+(N) is a H-family over N.
Remark 3.19 We have now formalized 7 degrees of rmrmality. Condition d.
says, that all H~(c) (Aft(c)) are A/" (Y+)-systems over c.
Definition 3.20 We introduce 7 * 2 quantifiers V i, &i, i < 7 into first-order
predicate calculus, and the following axioms: Let any axiomatization of predicate
calculus be given. Augment this with the axiom schemata
l) For N-families
1. v'~C(x) A w(r
-+ r -~
v'~r
a. vxr ~ v~.r --+ ?xC(x),
4. Vixr ~ VJxr for j < i,
5. &ixr ~ ~Vix~r (for all r ~b, i,j < 7),
6. Vixr ~ Viyr for safe substitution.
2) For A/+-families:
1. a. v~zr ~ v~(~ = x): r
b. w(~,(x) ~ ~(~)) A V'z~(~) : 4(~) -, W~-(~) : r
116
CHAPTER 3. DEFAULTS AS GENERALIZED QUANTIFIERS
2. Vixd2(x):
~(x) A Vx(r A @(x) --~ O(x)) -+ Vixr ~)(x),
3 ~xr A V~xr r -~ ~V~xr ~r
4. W(r -~ r -~ V~r : 0(~) -+ [3~r -~ ~.~(r
A
~(~))],
5. Wxr : r ~ VJxC(x): ~)(z) for j < i,
6. ~.~zr r ~ ~v~xr ~(~),
7. V~xr r ~ V~yr ~b(y) for safe substitution
(for all r r t~, ~, r, i, j < 7).
Definition 3.21 Let s be a first-order !anguage, and M a s Let
N'(M) (2V+(M)) be a X (N'+(M))-family over M. The definitions of <
M,N'(M)
> ~ r etc. are straightforward, like <
M,N'(M)
> ~ V{xr iff
there is A E A/'{(M) such that Va E A (< M,N'(M) > b r etc.
Theorem 3.22 1) The axioms of Definition 3.20,1) capture N-family-semantics
of V ~.
2) The axioms of Definition 3.20,2) capture H+-family-semantics of V {.
Proof Analogous to the proofs of Lemma 3.11 and Theorem 3.17. []
Remark:
To improve performance of a system, we might have several layers of informa-
tion. The very general (and simple) information might be formulated with V ~
quantifiers, the more specific one with V 1- quantifiers etc., and the most specific
(and hard) information classically, and all levels kept apart in the axiomatisation.
Thus, when pressed for a fast answer, the system might "jump to a conclusion" by
using only the V~ without checking consistency (i.e. without using
V ~- (i > 0) and hard information).
3.2.2 Strengthening the axioms
Overview of this section
In this section, we discuss various strengthenings of the axioms. They consist
in adding properties to the single H-systems (corresponding to part of "iterabil-
ity" - see below), in particular making X-systems filters, or coherence properties
between the H-systems over different subsets of the universe for the relativized
case. They are motivated partly by the common "use of defaults, partly by dis-
cussion elsewhere in the literature. In particular, we show how to interpret.the
axiom systems P and R of [KLM90] and [LM92] in our first order setting, several
of those axioms trivially hold in our system, "And" corresponds again to the fil-
ter property, and others translate into more subtle interdependencies among the
N'-systems of different subsets.
The ease with which we can incorporate these strengthenings is, of course, due
to the fact that our system was chosen so weak at the outset, while making the
language very expressive.
3.2. DEFAULTS AS GENERA LIZED Q UANTIFIERS 117
The details
In the introduction to this chapter, we have discussed problems of homogeneity
and iterability. What do they look like in Normal Case language? But, this
is simple, iterability will be discussed presenty, and homogeneity with respect to
o'(z) amounts to Vzr --+ Vzc~(z) : r We can add these as single axioms, or
as axiom schemata for all formulae o-, and all defaults V4, V~, when justified. So,
we are allowed to apply the conjunction of two defaults only if we have deduced
Vz(~b A ~b)(z). And, if we know something which is more than a mere tautology
about a, let's say T t- ~(a), then we are allowed to apply the default Vr only if
we can deduce T l- Vx~z(z) : ~b(z).
We can now give a formal definition of iterability within our extended language.
If a default theory is closed under iterability, and the defaults are of a simple
form, then the construction of a model is especially easy, this is the content of
the subsequent lemma.
Definition 3.23 (Iterability for defaults without prerequisites) We call the fol-
lowing axiom schema Iterability fbr defaults without prerequisites:
Vs162163 A Vs163 --~ Vs162 A @)(s
Lemma 3.24 Let D be a finite set of defaults of the form Vz~bi(z), i < n, where
r is a classical formula, and let Tt be a set of classical formulae, and suppose
that D is closed under iterability. Then D U T! is consistent iff T/U {3z(q~lA
... A~b,~_l)(z)} is consistent.
In the presence of defaults with prerequisites, iterability takes a slightly extended
form. In addition, "normal use" of defaults sanctions still another axiom schema,
which we call chaining. Again, we have a simplified model construction for simple
defaults closed under iterability.
Definition 3.25 (Iterability for defaults with prerequisites) We call the following
axiom schemata Iterability for defaults with prerequisites:
We(z) A W,:,(z) : ~(~') ~ Vzo(z) : (r A ~)(z),
V=~(=) : e(~) A W~-/(x) : ~,/(=) ~ V~(~ A o'0(~) : (~' A ~,/)(.).
Definition 3.26 (Chaining) We call the following axiom schemata Chaining:
Vxr A Vxr r -~ We(x),
wdx): r we(x): r ~ vx~(z) : §
Lemma 3.27 Let D be a finite set of defaults of the form Vzr i < n, let P
be a finite set of defaults of the form Vz~ri(x) : ~Pi(x), i < m, where all r c~i, r
are classical formulae, and let T/be a set of classical formulae, and suppose that
D and P are closed under iterability.
Then D U P U Tl is consistent iff the following set of (classical) formulae is con-
sistent:
c := T~ u {3~(A{r : i < ~})(~)} u { 3~(A{~ : i ~ p})(~.) ~ ~(A{~+ : i c p}
A A{@i:iEP} A A{r pCm }
1t8 CHAPTER 3. DEFAULTS AS GENERALIZED QUANTIFtERS
Definition 3.28 (Smoothness) Call jV+(M) a smooth H+-system over M, iff it
is a N'+-system over M, and for each N, N/C_ M, N C_ NI, A E N'(NI), A C_ N
implies A E N'(N).
This will be captured by adding the axiom schema
Vxr : r
A
Vx(~(x) -~ r A W(r
A.~(x)
-* ~(x)) -~ W~(x): ~(z).
An alternative semantics for a
predicate logic
version of P
and
R
We conclude by giving predicate logic versions of the systems P and R (see
[KLM90] and [LM92]) an alternative semantics by translating r ~(x) into
re(x) :
We see that Right Weakening, Reflexivity, and Left Logical Equivalence are al-
ready built into our system.
The others have to be introduced by additional axiom schemata, like
Vxc~(x) : fl(x) --~ (Vxc~(x) : -~7(z) V V,(o~ A 7)(x) : 3(x) ) for Rational
Monotony.
The translation is obvious, so we discuss the semantical counterparts.
"And" says that H-systems are closed under finite intersections, i.e. w-complete
filters. (This is part of the above iterability.)
"Or", Cautious and Rational Monotony concern the relation of the H-systems of
the subsets:
Or: A S 7V'(X), B r Af(Y) --+ A U B r A/'(X U Y),
Cautious Monotony: A, B e H(X) -+ d r]B E H(A),
Rational Monotony: A E Af(X), B __ X --+ B e H(X) or A - B e N'(X - B).
3.3
Sceptical revision of partially ordered
defaults
Overview of this section
Recollect from Section 3.1 that the LILOG setting consisted of an order sorted
language, which determines the strength of default information through the speci-
ficity of the sort to which the default is applied. This partial order on the default
information will now be exploited to select, in case of conflict, a reasonable con-
sistent subset of the information. Recall also that "conflict" is made precise as
inconsistency in our generalized quantifier logic introduced in Section 3.2.
We present and discuss four alternative approaches to theory revision, and decide
for the third, which seems to present the intuitively best results. More precisely,
this solution is a generic one, as it still leaves much liberty of choice for the
"parameters" f and -~ 9 (see below).
As usual in theory revision, we try to retain as much information as possible -
under some restrictions. In particular, when two formulas of equal strength are
in conflict, we will be fair and exclude both. On the other hand, if 4; and
are in conflict, and so are ~ and c~, we will sometimes like to preserve 4; and
or, eliminating just '44 and thus preserve a maximum of information. This is
3.3. SCEPTICAL REVISION OF PARTIALLY" ORDERED DEFAULTS 119
basically the problem we investigate here: Given such r ~b, # and the partial
order on formulas, what are the intuitions that might guide us in the selection
of a subset {r162 and how can we formalize our choice? In our proposed
solution, not only the relation between {r and {~b, cr} - e.g., is r stronger
than ~r? - will enter the picture, but also the certainty (to be called definiteness
of choice below) with which we would eliminate e.g. '~b from {r ~}.
3.3.1
Introduction
We will treat here a special case of theory revision based on axiom systems. Con-
sider a situation of a (possibly inconsistent) partially ordered set of defaults. Our
task will be to choose a consistent subset of those defaults, - where consistency
is determined by the above discussed logic - using the given partial order, but
being fair otherwise. Consequently, we will proceed sceptically, i.e. not neces-
sarily choose a maximal consistent subset, as two contradictory defaults of the
same or incomparable quality should both be excluded - as fairness dictates. The
reader may as well assume that all formulae considered are classical ones, and the
notion of consistency is the usual one. As a matter of fact, logic will play only a
marginal role, being restricted to the notion of consistency.
First, we will introduce some basic definitions, and subsequently discuss several
approaches to making a good and fair choice.
The reader will find many ideas from nonmonotonic inheritance theories applied
to and generalized in the following.
3.3.2 Basic definitions and approaches
Let ~ be a set of sorts S, partially ordered by <_, and/X a set of defaults, where
each 8 E A belongs to some sort s, written s ~ 8, thus A inherits the order <
from the sorts. To avoid inessential complications, we assume 2 and A to be
finite. % ~ 8" is supposed to read something like "normally, all elements of the
sort s, have the property 8(x)." ( In addition, at sorts s we might have classical
information, but we shall always assume that the total classical information is
consistent, and also that the defensible information written directly to some s is
always consistent too (even when taking the classical information into account).
This will simplify matters, but is not essential. ) Thus, for some x C s, s < t < u,
t ~ r u ~ r it is natural to consider r to be the stronger information than
~b(x), because it is the more specific information: In case of conflict, ~ should
win over ~b. (Thus, quality decreases with increase by <!) If, however, t and u
are incomparable, fairness dictates that a conflict between r and r should result
in disbelief of both r and r We thus consider f := 5C'(A) - {1~} --+ 7)(ZX) with
C
.f(~) r % where f is supposed to choose the "best" elements of a - if there are
none, f(c~) will be empty. Let further f(~) := ~ - ]'(o 0.
Any such ]" gives rise naturally to a notion of quality of the choice: Suppose
card(s) > 1. If ca'cd(-f(c~)) = 1, then f(c 0 is a very definite choice, if f(c~) = ~, i.e.
120
CHAPTER 3. DEFAULTS AS GENERALIZED QUANTIFIERS
card(f (a)) = card(a), f(a)
is very indefinite. We can thus define the definiteness
of the choice f(a) by
1 iff
card(a) = 1
d(f(a))
:= ~d(/(~))
~a(~)-i otherwise
(Thus, in the first case, d(f(a)) = 1, in the second one
d(f(a))
= 0.) Speaking in
terms of defensible inheritance,
d(f(a))
= 1 corresponds to preclusion,
d(f(a)) =
0 to contradiction. We shall not use the notion of definiteness until the third
approach, when we need a relation -~ 9 on minimal inconsistent subsets.
Examples: Let g(a) be the greatest element of a- i.e. for all z E a, x r g(a),
z < 9(a) - if it exists.
a- {g(a)}, iff 9(a)is defined
fl (a):= (D otherwise
f (a)
{ z E a: x is no non-trivial maximum, i.e.
? ,y e < y) or e a(y < }
0
iff there are x,y E a
such that x < y
otherwise
f3Cc~) := { x e a: x is a non-maximal element, i.e. 3y E c~(z < y) }.
By f(a) C a, f(a) will be consistent, if c~ is minimal inconsistent.
This suggests the probably simplest
Approach 1
Iterate some fixed f, starting on A, until consistency is reached. By finiteness
of A and antitony of f, this will always work. This approach has some effects
which may not always be desirable: Let s < t < u, s ~ d, t ~ -~q~, u ~ r
where I- ~b --+ ~b. ~ being the weakest information, it should always be eliminated
first by f. On the other hand, one might argue that {r ~b} is a good choice, as q5
should be accepted by being the best information, thus -~b should be out, leaving
the way open to ~.
Approach 2
We shall leave momentarily the above introduced function f, and even the order
_< on sorts and defaults, and discuss a quite different way. We now consider
arguments, which we identify with subsets of A, choosing the best ones, and
hoping that the union of the best arguments is consistent. This meets with some
problems. An order -4 on arguments should respect the following properties: Let
c~, fl etc be subsets of A. (Again, strength will decrease with increasing -~ .)
1. -4 should be transitive, i.e. a -4 fl -4 7 -~ a -4
2. c~ -4 fl C 7 --~ a -4 7. Reason: simply adding some information to an argument
should not make it stronger. Adding the truth 2 + 2 = 4 to an argument should
3.3. SCEPTICAL REVISION OF PARTIALLY ORDERED DEFAULTS 121
not give it more power. It is rather that the weakest part should determine its
force.
3. Vi E I(a~. -< /5) -+ U{a~/E i} -~/3: just putting arguments together should
not violate a common upper bound. This seems to be well in accord with many
natural definitions based purely on an order < as given above - though not on
all. ( Consider e.g. c~ -</3 :+-+ 3x E/3Vy E a(y < x). )
4. The inverse seems to be very doubtful: /3 --< U{a~ :i E I} --+ 3i E I(/3 -~ c~).
This is already violated by a -< ,3 :~ gx E c~3y E/3(x < y).
Yet rule 4 seems to suggest itself in our present approach, when trying to prove
consistency: Let %/3, 3' be pairwise consistent, but -,Con(oeU/3U7). If c~ -</3 and
/3 "< 7, then by 3., c~ U 3' -4 3', and 7 will be omitted in the inductive procedure,
resulting in a consistent choice. If, however, c~.L 7 (incomparable), and fl_l_7, then
maybe 7 "~ c~ U/3 (unless 4. holds), so c~ U/3 will not be chosen, but maybe each
of a,/3, 7, resulting iil an inconsistent theory.
Approach 3
We now work more closely again with the introduced functions f. First, a com-
binatorial result.
Definition 3.29 Let D be a finite set, MI C_ 7)(D), -< , an acyclic binary relation
on MI, for A E MI let 0 r XA C A be defined. Define inductively for i E co:
Mll := { A E M/: A -~ 9 in MI- U{MIj :j < i} },
Mi:= {AEM'i: Vj<iVBEMj(B-~9 },
Xi := U{XA :A E M;} and
M :=U{M; :i Ew},x :=u{x~ :i Ew},D~:= D-X.
Let, in the sequel, the situation of the definition be given.
Lemma 3.30 For all A E Mf, A 19 X • (~.
Remark 3.31 1) It suffices to choose --< 9 well-founded in the above Definition,
D and MI can then be infinite, too. We do not need the more general result,
however.
2) Evidently, -~ 9 may be chosen as the empty relation.
3) LetAEMI. ThenAEM ~VB-<9
Proof by induction on i: Let A E M/~ be minimal such that the result fails.
"---+": If A E Mi and 3B --< 9 E M, An XB • {~), then B E Mj for
some j < i, and A ~ 3/Ii by construction. %-': Let A E MI~ - M~ such that
VB -~ .A(B E M ~ AMXB = (~). Thus, tbr all j < i, B E Mj, B < |
A N XB = 0, and A E Mi by construction again. []
Corollary 3.32 Let D be a finite set of formulae, MI C_ T'(D) the set of min-
imal inconsistent sets of formulae from D. If X is defined as above, DI will be
consistent. []
122 CHAPTER 3. DEFAULTS AS GENERALIZED QUANTIF[ERS
Thus, letting f be as above, defining XA := A- f(A), any acyclic --4 9 on minimal
inconsistent subsets of A will give a consistent subset Af C_ A. Choosing -4 9 non-
empty will lead to some inconsistencies "being invisible", since some elements
responsible are eliminated already. The effect can be seen easily when looking
back at the example discussed in the first approach: Letting {r -4 9 ~b},
~q5 might be eliminated (by suitable f and X) as {r ~qS} is -4 9 leaving
{~qS, ~b} out of consideration. The discussion of --< 9 will be resumed in a moment.
Next, we look at the compatibility of this approach with an order on arguments
(subsets of A).
It is natural to define for c,, fl C_ A: c~ --4 fl :~ c~ C_ f(c, Ufl) - leaving all
logic aside for the moment. We have discussed the Postulates 1.-3. for orders
on arguments above, and examine now which of the above introduced fi satisfy
some or M1 of these postulates, fl will violate 2., as the addition of any element,
such that the largest element does not exist any more, will show. Consider f2,
and let c~ := {de}, fl := {Z/,z}, ordered by 9 < z (as defaults) only. Then
f(~ U fl) = {x,y}, thus ~ -< fl (as arguments), which seems very unnatural.
Looking at f = fa, which preserves all non-maximal elements, we see that the
order on arguments generated by f satisfies indeed 1.-3. This is immediate by
c~ -4 /3 ee c~ C_ fa(c~ U/3) ~ V:~ 6 c~By E c~ U/3(x < y) ~ Vz E
~?y C
/3(x < !/),
the last equivalence by transitivity of the partial order on E;
We have now for ~5 E A (-4 9 = ~ again, MI being the set of minimal inconsistent
subsets of A, thus by -4 9 = ~ M = MI):
6EA/~VAEM@5~XA) ~ VA E Mt(a 6 A ~ ~S c f(A)) ~ VA E MI(6 E A
---, {~5} -< A - {~}) ~ V/3 g A(-,Co.rz(a, 5) -+ {~5} -4/3). In the last equivalence,
we use property 2.: " +--" is trivial. "-+": Suppose there is/3, -~Cor@5,/3), -~{~5} -4
/5. Take 13I C /3 such that {~5} U ~ql is minimal inconsistent, so by prerequisite,
{c5} -4 fit, and by property 2. {~5} -4 ~.
Moreover, for a C_ At, we have =Corz(c~ tO/3) --+ a -< /3: Let /3t C_ /3 such that
a U/3t is minimal inconsistent. As a C A4 X~uo, R c~ = (~, thus a C f(a tO/30
and ~ -4 fit, by 2. r -4 ft.
Let us resume the discussion of -4 9 What are the meaning and properties of
the -4 o-relation? Let A -4 oB. Thus, the elimination of the inconsistency A
by eliminating the elements of XA is estimated so strong that the inconsistency
B need not be considered any more. In other words, the argument B - XB
against XB looses its importance. Now, we have by f a relation --4 on arguments.
Moreover, we have a notion of definiteness, resulting from f as well, as introduced
at the beginning of the Section. A natural definition (suggested by S.Lorenz) of
-4
9
will be
e.g.:
A -4 9 :~ 1. f(A) C_ B, 2. A- B -4 B, 3. d(f(A)) = 1, d(f(B)) 7s 1.
By 3., any such -4 9 will be acyclic, by the same reason, we can't have A < 9
| To conclude A -4 oB C_ C -+ A -4 9 for C such that d(f(C)) # 1, we need
A - C -4 C, which will not always hold. (It will hold for -4 defined by fa.)
3.3. SCEPTICAL REVISION OF PARTIALLY ORDERED DEFAULTS
123
Approach 4
As a last alternative, we shall discuss a more "procedural approach", which tries
to directly find a suitable subset A/C LX. Again we suppose some subset function
f to be given. Let
~1 < q52 "~ ~3 , ~1 < @ < r 0 <~ ~4
be defaults ordered by
their sorts. The ~b, p are (logically) unimportant here and might be tautologies.
Suppose further {r r r and {r Ca} are the minimal inconsistent subsets.
Suppose further f({r r ~4}) = {r f({~b2, ~a}) = {r which seems a nat-
ural choice. Proceeding now by the rank of the r in the <-order, at rank 2 Ca
will be eliminated, as the elimination of r and r will be discovered only at rank
3. In other words, we have here a result similar to the one discussed in the first
approach. (It corresponds again to choosing the empty order --< * on minimal
inconsistent subsets.)