On the Semantics of Supernormal Defaults

1 Introduction

In this paper, we consider "supernormal" [Brewka, 1991) defaults, i.e. defaults of the form (true : 6)/6. For 6 :: --.p(X1, ... , Xn) these are REITER's CWA-defaults which formalize the common implicit assumption of negations. But we allow any quantifier-free formula for 6, e.g.

The intuitive semantics is that this rule should be as­ sumed for as many X as possible. Although these defaults are very simple compared to the full default logic [Reiter, 1980), surprisingly many examples can be formalized with them. This restriction was suggested and investigated in [Poole, 1988; Brass and Lipeck, 1989; Brewka, 1991; Delgrande and Jackson, 1991; Dix, 1992). The advantages are that the definitions are much sim­ pler, certain abnormalities can be avoided, and there are reasonably efficient theorem provers [Przymusin­ ski, 1989; Ginsberg, 1989; Baker and Ginsberg, 1989; Brass, 1992a; Brass and Lipeck, 1992].

·This work was partially supported by the CEC under the ESPRIT Working Group 6071 IS-CORE (Information Systems - COrrectness and REusability), coordinated by AMILCAR SERNADAS.

Of course, it is also possible to specify axioms ~~ i.e. formulae which have to be fully satisfied {and usually there are many more axioms than defaults). In the flying ability example, the following axioms could be used:

bird( tweety). penguin (polly) . bird(X) +- penguin(X). --.jlies(X) +- penguin(X).

Given defaults ~ and axioms ~~ one can answer queries f/J. In the classical example the query could be

("which birds can fly?") . Now a correct answer is a sub­ stitution() for the variables of the query, e.g. {X<ltweety) , such that the corresponding instance of the query follows from the axioms and the defaults, i.e.

Of course, the consequence relation ~ ~ respecting the defaults ~ still has to be defined.

In the above example, it seems clear that any rea­ sonable semantics should allow to conclude flies( tweety) and not jlies(polly). But as soon as we have conflicts be­ tween defaults, e.g. because of disjunctive or incomplete information, there are different solutions. Probably ev­ erybody knows the credulous and the skeptical seman­ tics, but there are other possible definitions of~~ (see section 2). And, of course, we have to ask whether there are reasonable semantics which we do not know yet.

Therefore we try to approach this problem in a more abstract way, and look at the space of all possible de­ fault semantics. We can classify them by means of the valid deduction rules (and other properties, such as the preservation of consistency). There is a rich literature on nonmonotonic consequence relations (e.g. [Gabbay, 1985; Shoham, 1987; Makinson, 1989; Kraus et a/., 1990; Brass, 1990; Dix, 1991; Makinson, 1992]), but our way of deriving a default semantics from given properties seems to be novel.

Of course, the soundness of certain deduction rules has been proved or disproved for the known default seman­ tics. The aim of this paper is to show the completeness of deduction systems for different default semantics. For automated theorem provers, the algorithms in the above cited literature may be better suited. But for proofs "by hand" the rules discussed here allow a much higher level with far less steps.

Additionally, our results show that if we require cer­ tain natural properties, the corresponding default se­ mantics is uniquely determined. So the default semantics that we know are not as casual as it may seem at first.

2 Default Semantics

In this section, we define the notion of a default seman­ tics and give some concrete examples.

We assume a signature E as given, which declares the predicates and constants of the application area. As a useful and common simplification, we exclude function symbols and require that E is finite. Instead of clauses, we allow arbitrary quantifier-free formulae, because they may be built by the deduction rules (also conjunctive de­ faults are sometimes useful, and 61 1\62 is not equivalent to the two single defaults).

Definition 2.1 (Default): A default is a quantifier­ free E-formula 6.

Definition 2.2 (Consequence Relation): A con­ sequence relation is any relation f-v between sets 41 of quantifier-free E-formulae (the axioms) and variable-free E-formulae t/J (the query after replacing the variables by the answer-constants).

We do not consider answers containing variables. This is again a simplification, but it is very natural, at least if the axioms, the defaults and the query are range­ restricted (see [Brass, 1992b]).

Definition 2.3 (Default Semantics): A default se­ mantics is a mapping which assigns to every set ~ of defaults a consequence relation f-v A .

Most default semantics refer to the single instances of the defaults, not to the default rules themselves:

Definition 2.4 (Default Instances): We write~· for the set of ground instances of formulae from ~.

One can view ~ as a mere shorthand for ~ ·, since in the following, we will only refer to ~ · (and call the 6 E ~ · "defaults", too).

The simplest default semantics is the CWA [Reiter, 1978], which assumes a default instance 6 (e.g., a nega­ tive ground literal) iff it is consistent with the axioms 41, i.e. its negation does not follow from 41:

It is well known that this definition may lead to incon­ sistencies if there are conflicting defaults. The simplest example is 41 := {p V q} and~:= {--,p, --,q}.

Therefore, we have to check the consistency of a set of defaults at a time:

Definition 2.6 (Extension): E ~ ~ · is a ~-extension of41 iff

• 41 U E is consistent, and
• 41 U E U { 6} is inconsistent for every 6 E ~ · -E.

So an extension is simply a ~-maximal set of default instances which is consistent with 41. Note that our ex­ tensions are not closed under logical consequences. But if one takes Th(41 U E), one gets exactly the original extensions from [Reiter, 1980], as proven in [Dix, 1992].

Of course, there may be more than one extension, but we need a single f---A· There are different solutions to this problem, e.g. the careful, skeptical, and credulous semantics, and the CWA-semantics also fits nicely in this scheme (see lemma 2.8):

Definition 2. 7 (Different Default Semantics):

Note that the careful semantics is not the same as the skeptical one: For instance, in the above example, we have the two extensions { --,p} and { ...,q}. Then the skep­ tical semantics will allow us to conclude --,p V --,q. The careful semantics may only use defaults contained in the intersection of the extensions (which is empty in this case). Given a set of negation defaults, the skeptical semantics turns disjunctions into "exclusive or", while the careful semantics interprets them as "inclusive or" (corresponding to the GCWA [Minker, 1982]) 1 .

Of course, the above list is not complete. For instance, it is common to select one of the extensions by some external means (e.g., "implementation defined", or by priorities between the defaults, etc.).

We now prove the above characterization of the CWA:

Proof: The CWA assumes those 6 E ~ · s.t. 41 If --,6, i.e. 41 U { 6} is consistent. But every consistent set of de­ faults can be extended to an extension [Brass and Lipeck, 1989]. The other direction is even simpler . 0

3 N onmonotonic Consequence Relations

In this section, we will consider deduction rules for non­ monotonic consequence relations and comment on their validity for the default semantics of the last section. The rules REF, RW, AND, EQ, OR are taken from [Kraus et a/., 1990].

1 JiiRGEN DIX pointed out that 4> := {p V q, r +- p A q}, ~ := { -.p, -.q, -.r} shows that sometimes even the careful se­ mantics turns "V" into exclusive or ( -.r is assumed and allows to conclude -.p V -.q) . This is another indication that there may be many more useful default semantics than we currently know. (WGCWA protects disjunctions, but violates EQ (see later) and cannot be directly generalized to arbitrary ~.)

First, we should expect that f-.-.o. allows at least to conclude the (instances of) preconditions, so that no in­ formation is lost:

Definition 3.1 (REF): f-.-.o. is reflexive iff

In this and all of the following definitions we of course re­ quire that the implication holds for all sets of quantifier­ free formulae ~ and all variable-free formulae ..P ( tp ranges over all quantifier-free formulae, and 6 over the elements of 6 .. ).

All of the default semantics from section 2 have the property REF and it is hard to think of any reason why it should be violated (at least if~ is consistent).

Next, we should require that f-.-.o. behaves "logical" in the following sense:

Definition 3.2 (RW): f-.-.o. allows right weakening iff

This rule is sound for all of the above default semantics. A stronger requirement would be to allow arbitrary logical consequences of what we have already derived:

This follows from RW together with the following rule:

Definition 3.3 (AND): f-.-.o. is closed under conjunc­ tion iff

All of the proposed semantics except the credulous one are closed under conjunction. �iven~:= {p V q}, Ll := { ...,p, ...,q}, we can credulously conclude ...,p and q (from E1 := {-,p}) and ...,q and p (from E2 := {-,q}) ; but we cannot conclude p 1\ -,p, i.e. false.

The following is a weaker property, which is satisfied also by the credulous semantics:

Definition 3.4 (CLC): f-.-.o. allows conjunction with logical consequences iff

The credulous semantics satisfies also the following re­ striction of AND to non-conflicting defaults:

Definition 3.5 (DA): f-.-.o. is closed under conjunction for non-conflicting defaults iff

Of course, a default semantics should only look at the logical contents of ~, not at the way the axioms are written down:

Definition 3.6 (EQ): f-.-.o. is compatible with left logical equivalence iff

The following property allows a case analysis for disjunc­ tive preconditions:

Definition 3. 7 (OR): the preconditions iff f-.-.o. supports disjunctions in

The careful semantics does not have this property, as can be seen in the standard example with Ll := {-,p, ...,q}: Here {p} f-.-care/(.0.) -,pV-,q and {q} f-.-care/(.0.) -,pV-,q both hold, but {pV q} f-.-care/(.0.) -,pV -,q does not.

A weaker property, which is satisfied by the careful semantics, is the following:

Definition 3.8 (DOR): f-.o. supports disjunctions in the preconditions for deriving defaults iff

Of course, there are many more such rules, e.g. cumula­ tion. But we do not need them in the results of section 4.

What is missing are ·properties allowing to conclude certain defaults. Up to now, the logical implication !­ would be perfect - it satisfies all the rules. But, of course, it is not a reasonable default semantics.

Naturally, we should only require that a default is as­ sumed if this is really obvious. The results would be void if we use the default semantics itself in its own charac­ terization.

We believe that the original CWA is the only sensi­ ble semantics if it is consistent. Obviously, we cannot assume more defaults, because this would immediately ruin the consistency (even if we would assume no other default) . But there is also no reason why we should not adopt a default contained in the consistent CWA. And intuitively, a default should be assumed if there is no evidence to the contrary.

Definition 3.9 (CWA): f-.o. is weakly compatible with the CWA iff

This property is satisfied by all the default semantics of section 2, which is an additional argument for its ade­ quacy.

If we want to use it in deductions, we need a global consistency proof for the CWA, which might be quite difficult . The following property avoids this and looks only at the default we want to conclude and at possibly conflicting defaults:

Definition 3.10 (UCD}: f-.-.o. satisfies uncritical de­ faults iff~ f-.- .o. 6 for every 6 E Ll· and consistent ~ such that there are no 61, . . . , 6n E Ll·, n ~ 0 with

• ~ U { 61, ... , 6n} is consistent, and

This property is satisfied by all the known default se­ mantics. And it is very natural, because one typically explains the applicability of a default by an argument like "well, there is no way to conclude -.6, so we can as­ sume 6". The property UCD formalizes this (especially the "no way" has to take into account other defaults) .

But the property UCD is strictly stronger than the CWA property, so it is automatically more questionable.

Lemma 3.11: If f-.o. has the property UCD, then it has also the property CWA.

Proof: The original CWA is consistent if and only if there are no defaults 61, ... , 6m E ~ ·, m ~ 2, such that f) 1- -.61 V · · · V -.6m and f) ~ -.6, for i = 1, ... , m (this is a simple generalization of a result from [Shepherdson, 1984]). Then obviously only the case n = 0 in defini­ tion 3.10 is interesting and it collapses to the definition ~~em. o

The property UCD in fact requires that at least all the defaults contained in the intersection of the extensions can be concluded by the default semantics:

Lemma 3.12: If 6 E ~ · can be concluded by the property UCD, then it is contained in every extension.

Proof: Suppose it would not be contained in an ex­ tension E . Then choose { 61, ... , 6n} = E ( E is finite because of our constraints on E, but this lemma holds also in the general case, one only has to apply the com­ pactness theorem). By definition f)UE is consistent and f) U E U { 6} is inconsistent, i.e. f) U E 1- -.6. 0

Therefore characterizations of the careful semantics us­ ing UCD are not very interesting (we will give one using CWA and DOR).

Finally, the following rule formalizes the idea that de­ faults are assumed in the absence of information to the contrary:

Definition 3.13 (IMD): f-.o. is inverse monotonic for defaults iff

This is a very strong property, since it ignores con­ flicts with additionally assumable defaults. The original CWA and the credulous semantics have this property, the skeptical and the careful semantics violate it (con­ sider f):= {pVq}, <p :=p, and~:= {-.p,-.q}).

Table 1 summarizes which deduction rules are valid for which default semantics. We see that the interesting properties for classifying default semantics are AND, OR and IMD. All other deduction rules hold for all of the four semantics (but they are needed in the completeness proofs of the next section).

·

Table 1: Validity of deduction rules

4 Characterizations

This section contains our main results which characterize the default semantics by their properties.

These characterizations are of the form "the seman­ tics X is the weakest one satisfying the properties Y". We call a default semantics weaker than another one iff all the conclusions valid with respect to the former are also valid with respect to the latter:

Definition 4.1 (Weaker Than): f-.o. is (non-strictly) weaker than f-~ iff

For instance, the semantics studied here form a chain in the sequence f- caref(.O.), f-,kept(.O.), f- cred(.O.), f- cwa(.O.) (from weakest to strongest) .

The weakest default semantics satisfying certain de­ duction rules is that one which allows to conclude exactly the derivable formulae. Therefore a characterization of this form simply states the soundness and completeness of the deduction rules.

Theorem 4.2: f-,kept(.O.) is the weakest consequence relation satisfying REF, RW, AND, EQ, OR, and CWA.

Proof: The soundness of these rules is trivial or already proven in the literature. So we only have to prove the completeness, i.e. that there is no weaker semantics.

Let f- .o. be any other consequence relation with these properties, and let f) f-,kept(.O.) 1/J. We have to show that f) f--..o. 1/J. The proof is by induction on the number of extensions of cl> (there are only finitely many because of our restrictions on E).

If there is only one extension E, then the CWA is consistent, so we get all 6 E E by the property CWA. Since cl> U E 1- t/1, by HERBRAND's theorem c~>· U E 1- 1/J, and it is easy to derive t/J with REF, RW and AND.

Now assume that there are at least two extensions and let E be one of them. Let 61 , ..· , 6n E ~ · be those defaults which are not contained in E , but in some other extension. Then we consider cl>; := cl> U { 6;} and cl>' := cl> U { -.61 A · · · A -.6n}.

Obviously, an extension of one of the cl>i is also an extension of cl>. So it cannot have more extensions and it follows that eli; 1-d:ept(.O.) 1/J. On the other hand, eli; has at least one fewer extension, namely E . Therefore we can apply the inductive hypothesis and conclude eli; 1-.o. 1/J .

The only remaining case is eli'. It has the extension E and only that (all defaults not contained in E are ex­ plicitly excluded) . So we get eli' 1-.o. 1/J (as in the base step) .

Now we apply iteratively the property OR to "disjoin" eli1, ... , elin, eli'. This results in the formula

which is a tautology, and therefore can be removed by the property EQ. So we finitely get eli 1-.o. 1/J. 0

We can use also the property UCD instead of CWA:

Corollary 4.3: 1-.A:ept(.O.) is the weakest consequence relation satisfying REF, RW, AND, EQ, OR, and UCD.

Proof: This follows directly from theorem 4.2 be­ cause on the one hand, UCD implies CWA (lemma3.11), and on the other hand, 1-.A:ept(.O.) has this property (lemma 3.12). 0

A characterization of the careful semantics uses the weaker property DOR instead of OR:

Theorem 4.4: l-caref(.O.) is the weakest consequence re­ lation satisfying REF, RW, AND, EQ, DOR, and CWA.

Proof: The proof is very similar to that of theorem 4.2. But instead of directly trying to conclude 1/J, we derive the defaults 61, .. . , 6n E ~ · which are contained in the intersection of the extensions and were used to derive 1/J. For them, we can use DOR instead of OR. The rest di­ rectly follows from REF, RW, and AND. 0

As explained above, a characterization of the careful se­ mantics through the property UCD is nearly trivial:

Corollary 4.5: l-caref(.O.) is the weakest consequence relation satisfying REF, RW, AND, and UCD.

The credulous and the CWA semantics allow the use of the rule IMD:

Theorem 4.6: l-cred(.O.) is the weakest consequence relation satisfying REF, RW, CLC, DA, CWA, and IMD. This result holds also with CWA replaced by UCD.

Proof: Let eli l-cred(.O.) 1/J. So there is an extension E of eli with eli U E f- 1/J, i.e. there are 61, ... , 6n E E and !f'1, . . . , rpm E eli* with IP1 /1. . . . /1. lf'm /1.61 /1. . .. /1. 6n f- 1/J. We have to show that eli 1-.o. 1/J for any consequence relation 1-.o. with the given properties.

Let 6~, . . . , 6~ be those defaults not contained in E, but in some other extension. Let eli' := eli U { -,6~, . .. , -,6A,} . As above, we find that eli' has only one extension, namely E . So the CWA-property or the UCD-property allow to conclude eli' 1-.o. 6; fori= 1, ... , n .

But then we get eli 1-.o. 6; for i = 1, . .. , n by the rule IMD. Since the 6; are contained in the same ex­ tension, there is no conflict between them and rule DA

results in eli 1-.o. 61 /1. · · · /1. 6n. Now we use CLC to derive eli f-.o. rp1 /1. . . . /1. rp~; /1. 61 /1. · · · /1. 6n and finitely RW to get eli 1-.o. 1/J. 0

If we require the stronger property AND instead of CLC and DA, we get the CWA:

Theorem 4.7: l-cwa(.O.) is the weakest consequence re­ lation satisfying REF, RW, AND, CWA, and IMD. This result holds also with CWA replaced by UCD.

Proof: Let eli f- cwa( .o.) 1/J, so there are 61, ... , 6n E ~ · and !f'1,····1f'm E eli* with eli V -,6; (i = 1, ... ,n) and rp1 /1. · · · /1. !f'm /1. 61 /1. · · · /1. 6n f- 1/J. Because of lemma 2.8, there are extensions E; containing 6; (i = 1, . . . , n).

We again have to show eli 1-.o. 1/; for any consequence relation satisfying the properties of the theorem. As in the proof of theorem 4.6, we get eli 1-.o. 6; (i = 1, ... , n) by means of CWA (or UCD) and IMD. Property REF allows to conclude eli 1-.o. 1/J; (i = 1, ... , m), so AND results in eli f- .o. rp1 /1. · · · /1. !f'm /1. 61 /1. · · · /1. 6n, and RW does the rest. D

So the properties REF, RW, AND, CWA, and IMD are only satisfied by l-cwa(.O.) or a stronger semantics. But l-cwa(.O.) already destroys the consistency, so in effect we cannot require all these properties together.

5 Conclusions

In this paper we considered different semantics for super­ normal defaults and their properties as nonmonotonic consequence relations. Our main results are complete­ ness proofs for certain deduction systems. On the one hand, this should help to better understand and motivate these semantics, and on the other hand, the deduction systems have some practical use for proofs "by hand".

Of course, we are still at the beginning of a general theory of default semantics. Many interesting extensions remain to be explored.

For instance, defaults with priorities are practically very important. If we use a prioritized CWA as basis, the characterizations of the skeptical and the careful seman­ tics can be generalized [Brass, 1992b]. But the extension of the CWA to partially ordered defaults is not as clear as it might seem at first: We noted in [Brass, 1992a] that the constructive semantics proposed in [Brewka, 1991] is in fact different from any "preferential model" approach. So there are at least two incompatible notions of "ex­ tension" in this setting, and we should study properties formalizing the prioritization.

Of course, one should also try to generalize our results to full default logic.

Another direction for future work is to find previously unknown semantics by requiring certain properties. For instance, the rationality or rational monotonicity

is not satisfied by the skeptical and the careful semantics. So what happens if we require this rule in addition?

Note that here reference is made to P£-.o., so we cannot simply take the set of derivable formulae as the stan­ dard semantics. Other properties require that something should not be derivable (e.g., false), or give more indefi­ nite information about the derivable formulae (e.g., the expansion property [Brass, 1990]). With such properties it might be possible to show that there is only a unique default semantics satisfying them - or none at all.

Acknowledgments

I would like to thank Uoo LIPECK for suggesting the development of a system for natural deduction with de­ faults. He supervised my doctoral thesis which contains similar results to the ones presented here (among other things) .

I would also like to thank JURGEN DIX, whose com­ ments were most helpful.