next up previous
Next: Complexity Up: Well-Founded Semantics for Extended Previous: Adding Preferences

A Legal Reasoning Example

In this section we want to show that the additional expressiveness provided by our approach actually helps representing real world problems. We will use an example first discussed by Gordon (1993, p.7). We somewhat simplified it for our purposes. The same example was also used in [4] to illustrate the approach presented there.

Assume a person wants to find out if her security interest in a certain ship is perfected. She currently has possession of the ship. According to the Uniform Commercial Code (UCC, § 9-305) a security interest in goods may be perfected by taking possession of the collateral. However, there is a federal law called the Ship Mortgage Act (SMA) according to which a security interest in a ship may only be perfected by filing a financing statement. Such a statement has not been filed. Now the question is whether the UCC or the SMA takes precedence in this case. There are two known legal principles for resolving conflicts of this kind. The principle of Lex Posterior gives precedence to newer laws. In our case the UCC is newer than the SMA. On the other hand, the principle of Lex Superior gives precedence to laws supported by the higher authority. In our case the SMA has higher authority since it is federal law.

The available information can nicely be represented in our approach. To make the example somewhat shorter we use the notation

as an abbreviation for the rule

where is the complement of c, i.e. if c is an atom and a if . Such rules thus correspond to semi-normal or, if m = 0, normal defaults in Reiter's default logic [20].

We use the ground instances of the following named rules to represent the relevant article of the UCC, the SMA, Lex Posterior (LP), and Lex Superior (LS). The symbols and are parameters for rule names:

The following facts are known about the case and are represented as rules without body (and without name):

Let's call the above set of literals H. Iterated application of yields the following sequence of literal sets (in each case ):

The iteration produces no new results besides the facts already contained in the program. The reason is that UCC and SMA block each other, and that no preference information is produced since also the relevant instances of Lex Posterior and Lex Superior block each other. The situation changes if we add information telling us how conflicts between the latter two are to be resolved. Assume we add the following information:gif

Now we obtain the following sequence:

This example nicely illustrates how in our approach conflict resolution strategies can be specified declaratively, by simply asserting relevant preferences among the involved conflicting rules.

next up previous
Next: Complexity Up: Well-Founded Semantics for Extended Previous: Adding Preferences

Gerd Brewka
Thu Feb 8 10:26:15 MET 1996