11/17 - Defaults and Diagnosis

Today:
- Default logic
- Nixon triangle 
- Diagnosis

Last class:

Given two models M1 and M2, define
	M1 <=[abnormal] M2
M1[ab] subset M2[ab]

M is a MINIMAL MODEL of F with respect to abnormal if M is a model of F, and there is
not a model M' of F such that M' < M2 (strictly smaller extension)

Then we say F minimally entails G (with respect to abnormal)
	F |=[abnormal] G  
if G holds in all model of F that are minimal with respect to abnormal.

*******************************************************************

Default logic: this is an alternative approach to solving the problem with
generalizing negation as failure to full FOL.  The idea is generalize our ordinary
logical proof rules:

ASSUMPTIONS
-----------
CONCLUSION

to ones of the form:	
	
ASSUMPTIONS : CONSISTENCY_CONDITION
-----------------------------------
CONCLUSION

The idea is that the rule can be applied ONLY if ASSUMPTIONS are proved, and the
CONSISTENCY_CONDITION is consistent with the new KB that is reached by applying ALL
the rules that can possibly be applied.  

For example, we could replace the axioms we had about birds with the following
default rule:

bird(x) : flies(x) & ~penguin(x)
--------------------------------
      flies(x)

Explain what this means.
Alternatively, we can use the "abnormal" axioms we had:

bird(x) & ~ab(x) => flies(x)
penguin(x) => ab(x)

and add the following as a default proof rule:

   : ~ab(x)
-----------------
    ~ ab(x)

Suppose we know 

bird(tweety)
bird(opus)
penguin(opus)

We can now prove flies(tweety), because it is CONSISTENT to conclude ~ab(x).
Similar, we CANNOT prove flies(opus), because the KB U {~ab(opus)} is inconsistent.

So far this looks just like negation as failure.  What happens if we have some
DISJUNCTIVE information?

bird(tweety)
bird(bert)
bird(sam)
penguin(bert) v penguin(sam)

It looks like it is okay to apply the default rule to infer ~ab(bert).
However, once we have done so, we can conclude by ordinary logical inference
that 
	~penguin(bert)
so therefore
	penguin(sam)
	ab(sam)
At this point we CANNOT apply the default rule a second time to infer ~ab(sam),
because that would result in an inconsistent set of formulas.

The result of applying the default rule the first time is the following set of
formulas and all of its logical consequences:

{bird(x) & ~ab(x) => flies(x)
penguin(x) => ab(x)
bird(tweety)
bird(bert)
bird(sam)
penguin(bert) v penguin(sam)
~ab(bert)}

At this point no more defaults can be applied.  We call this set of formulas an
EXTENSION.

Now, suppose we had tried to apply the default rule to sam BEFORE we applied it to
bert.  Then we would get a DIFFERENT EXTENSION:

{bird(x) & ~ab(x) => flies(x)
penguin(x) => ab(x)
bird(tweety)
bird(bert)
bird(sam)
penguin(bert) v penguin(sam)
~ab(sam)}

In summary: in default logic, different mutually incompatible sets of conclusions may
be inferred.  We call each an EXTENSION.

So, how do we define ENTAILMENT in default logic?  
There are two notion:
Where KB is a set of FOL formulas and D is a set of default rules, 

KB  |-<D>  F          iff  F is entailed (by ordinary FOL) by SOME extension of KB
KB  |-[D]  F          iff  F is entailed (by ordinary FOL) by ALL extensions of KB

We can think of the first as "risky" default reasoning, and the second as "cautious"
default reasoning.  In this example, 

KB |-<D> fly(bert)
KB |-<D> fly(sam)
KB |-[D] fly(bert) v fly(sam)

So, using a very different basis for reasoning, cautious default logic gets us to the
same conclusions as CIRCUMSCRIPTION.

*********************************************

Example: NIXON DIAMOND

quaker(x) def===> pacifist(x)
repubican(x) def===> ~pacifist(x)
quaker(nixon)
republican(nixon)

*********************************************
DIAGNOSIS

An important application area for methods of default reasoning is called "Model Based
Diagnosis".  The idea in MBD is the intended functioning of a mechanism is
represented in logic.  The actual inputs and outputs of the device are also represented
logically.  If the device is malfunctioning, we want to infer the possible CAUSES
of the malfunction.  That is, instead of reasoning from causes to effect, we want to
reason "backwards" from effects to POSSIBLE causes.  

Model based diagnosis is used in some commercial products, such as Xerox
photocopies.  It also has been employed by NASA in the control systems for some of
their space missions.  About ten years ago, DEEP SPACE ONE used a model based
diagnosis system that monitored its propulsion system, and could automatically fix
certain faults, for example, if a valve appeared broken, it would activate a parallel
valve.

I'll describe what the chapter I had handed out calls "consistency based diagnosis",
using a simple example.

Circuit with two gates:
          g1 w  g2
in1 ----- OR---NOT----out1
in2 ------|  |--------out2

Let's give a label to the wire coming out of the OR gate, call it w.

Each gate can either be NORMAL (okay) or ABNORMAL.
gate(g1)
gate(g2)

gate(x) : ~ab(x)
----------------
      ~ab(x)

Now, we define the proper functioning of the circuit:

~ab(g1) => ( w <=> (in1 v in2) )
~ab(g2) => ( out1 <=> ~w )
out2 <=> w

Next, we observe the device in operation, and decide whether what we are seeing is
CONSISTENT with the device operating normally.  We do this by computing an EXTENSION
of 
	DEVICE MODEL U OBSERVATIONS

Suppose we observe 
in1, ~in2, ~out1      [out2 is not measured]

We can compute only ONE extension, which is 
	DEVICE MODEL U OBSERVATIONS U {~ab(g1), ~ab(g2)}
	
Suppose instead we observe
in1, ~in2, out1       [out2 is not measured]

We can compute TWO DIFFERENT extensions (go through the steps):

	DEVICE MODEL U OBSERVATIONS U {~ab(g1), ab(g2)}
	DEVICE MODEL U OBSERVATIONS U {~ab(g2), ab(g1)}

So we have TWO POSSIBLE DIAGNOSIS, either g1 has failed or g2 has failed.

Suppose instead we observe
in1, ~in2, out1, out2

Now we have only ONE diagosis:
	DEVICE MODEL U OBSERVATIONS U {~ab(g1), ab(g2)}