Lehekülje Draft notes for our approach to reasoning with defaults lähteteksti vaatamine

Ideas for handling default rules with taxonomies


We look at how to handle non-monotonic
https://en.wikipedia.org/wiki/Default_logic
where even a single rule application may
be not computable, since checking the
conditions for default (blockers in the
following) is generally undecidable.


Intro to defaults
------------------

This is the classic example:

bird(tweety)
penguin(pennie)
penguin(X) => not flies(X)   % this holds always 
bird(X) => flies(X)    % this is a default rule
penguin(X) => bird(X)  % this holds always

from which we want to derive 
flies(tweety)
not flies(pennie)

The default logic says that the default rule
bird(X) => flies(X)
application to some object t 
should be blocked if we can derive 
not flies(t)

This is the blocker condition for the rule:
not flies(X)
which can be the same as the conclusion,
but we may want to consider a more generic case with
blockers different from the conclusion. 
Unclear if this more generic case makes much sense.

The probabilistic understanding is that this
situation arises because penguins form a tiny
atypical subset of birds. I.e. almost all birds
fly, but penguins fall outside this "almost all" subset
of birds.

Thus an attempt to give a probability to
the birds rule like
0.95 :: bird(X) => flies(X)   
is not sufficient.

Classic suggestion: ordering of defaults
----------------------------------------

Consider defaults combined with taxonomies:
for most of the higher-level concept cases,
the default rule holds, but for a small percentage
of cases it does not. Knowledge about more specific cases
should overrule knowledge about more general cases:
if the default does not hold for our individual,
we assumed it is in the small percentage
of abnormal cases.

As a suitable example we add a thing concept
to the previous one:

bird(tweety)
penguin(pennie)
penguin(X) => not flies(X)  
bird(X) => flies(X)    % this is a default rule
penguin(X) => bird(X)  % this holds always

thing(car)
thing(X) => not flies(X) % this is a default rule
bird(X) => thing(X)      % this holds always

from which we want to derive 
flies(tweety)
not flies(pennie)
not flies(car)

Notice that there are now several default
rules with contradictory conclusions applicable
to birds.

A classic suggestion is to build an order between
default tules and let lower-level default rules,
which apply to more specific cases, have priority
over higher-level ones, which apply for more
general cases:
https://www.aaai.org/Papers/AAAI/1994/AAAI94-144.pdf
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.79.8458&rep=rep1&type=pdf

Thus, this derivation 

bird(tweety), hence using bird(X) => thing(X)
thing(tweety), hence using the thing(X) => not flies(X)
not flies(tweety) 

should be blocked by

bird(tweety), hence using bird(X) => flies(X)
flies(tweety) 

because the rule
bird(X) => flies(X)
is stronger in the ordering than
thing(X) => not flies(X)

Clearly, the ordering of defaults is generally not
complete, although it should be transitive.

Another classic example where there is no order:

republican(nixon)
quaker(nixon)
republican(X) => not pacifist(X)  % default rule
quaker(X) => pacifist(X)          % default rule

where we should expect that defaults cancel
each other out for nixon and thus we cannot
derive anything about nixon.

I.e. we should assume we can have several different or
partially overlapping hierarchies of defaults:
a transitive, non-cyclical and non-complete order.


Proposed approach to ordering the defaults
------------------------------------------

Put shortly: we push this question to be handled
in the next iterations of the proposal.

For now let us assume that defaults are already ordered
before the proof search starts, i.e. we do not
need to calculate the order during the search.

This may be suboptimal for some scenarios
(maybe the full calculation of order is unfeasible?),
but clearly there are potential ways to build
a mixed calculation scheme, cache some of the order
etc etc: we will not (yet) consider these problems.

We also assume that _normally_ the ordering calculation
is based on the taxonomy rules like in the example
above.



How to handle proof search with defaults
-----------------------------------------

Main issues:

* We need to check if default rule applications are
  blocked or not, which is - generally - not decidable,
  since FOL is only semidecidable.

* A single proof may contain many different default rule
  applications, to different terms.

* A default rule may contain predicates with several arguments,
  not just one, as in the examples above.

* We want to handle contradictory knowledge bases.

* We want to handle confidences.


The main idea proposed is to not try to block defaults 
during proof search: instead, check the proofs for 
blockage after the proofs have been found. 
  
This should be combined with some - obvious and fast -
blockage checking during proof search, purely for
efficiency. Like, find out if there are high-confidence
atomic facts directly blocking a rule application.

The second important point is the technique for recording
default rule applications along with the arguments/terms
they were applied to.
  
The main points of the algorithm: 

* Add a special default rule application atom to each
  default rule, to store the application fact along
  with the term it is applied to.
  
  This atom is formed of the conclusion of the default
  rule along with the id of the default rule, like this:
  
  bird(X) => flies(X) is represented as 
  -bird(X) | flies(X) | $blocker(id_of_rule,-flies(X))
  
  Notice that the $blocker atom is handled like any
  other atom (substitutions are made to X etc) but it
  is really a meta-level object, since it contains a literal
  -flies inside the predicate, which is not OK for FOL.
  
  After a proof (we will say the _main_ proof) is found, 
  the derived object thus contains
  information about all the terms along with the id-s of
  default rules applied to these terms.
  
* Produce all the different main proofs during allocated time,
  i.e. do not stop when one proof is found.
  
* Check for each default rule application to terms in each 
  main proof whether it is blocked: i.e. try to prove 
  that the blocker holds. If some blocker holds, the 
  whole main proof is blocked and is thus discarded.

  Importantly, 
  
  * in the blocker proof search DO NOT USE any default rule applications
    to the default-used terms in the main proof where the rule applied
    is of a lower priority than any of the default rules applied
    to the same term in the main proof. This is why we need the
    rule id-s.
    NB! The details here need some checking: issues with multiple
    default rules applied to different arguments in the proof may
    not be trivial.
  
  * Give less time for the blocker proof search than for the main proof:
    preferrably let us calculate the time limits like this:
    
    N seconds (or milliseconds) for the whole proof search, of which
    N/2 for the search of the main proofs
    N/2 for all the blocker proofs altogether
    Now, when there are M default applications in all the
    main proofs altogether, use
    (N/2)/M seconds for each blocker proof search.
 
  * Recursively check the blocker proofs like the main proof
    above, again both restricting the set of applicable defaults
    and giving less time for the search.
    
  * Eventually the recursive blocker proof searches reach
    a very small time limit after which we do not go any
    deeper into the recursion.
    
* Finally, since we assume a contradictory knowledge base
  and/or confidences attached to clauses,
  do not directly perform the recursive procedure above as explained:
  instead, perform for each search a separate search for positive evidence
  and negative evidence and use the combined result of a positive an
  negative search as an indicator of whether the proof was successful.
  
  In case the confidence of the result is below some given threshold,
  do not consider a proof to be a success.
  
  When checking different main proofs (or recursively lower cases
  of main proofs), initially order the results by starting with the
  ones with the highest confidence. This is not - strictly - necessary,
  but may give options for optimizations.
  
* Do not give full 100% confidence to default rules: this will cause
  the proofs with the fewer defaults to be preferred in checking and
  more likely to be found.
  
  
Examples from above
--------------------

We take the following example from above 
without confidences and without attempting
to find separate negative evidence:

bird(tweety)
penguin(pennie)
penguin(X) => not flies(X)  
bird(X) => flies(X)    % this is a default rule
penguin(X) => bird(X)  % this holds always

thing(car)
thing(X) => not flies(X) % this is a default rule
bird(X) => thing(X)      % this holds always

and will try to prove these, one after another

-flies(car)
flies(tweety)
-flies(pennie)

== -flies(car) task ==

The same KB as clauses with clause ids and blockers attached:

1: bird(tweety)
2: penguin(pennie)
3: -penguin(X) | -flies(X)  
4: -bird(X) | flies(X) | $blocker(4,-flies(X))    % this is a default rule
5: -penguin(X) | bird(X)  % this holds always

6: thing(car)
7: -thing(X) | -flies(X) | $blocker(7,flies(X)) % this is a default rule
8: -bird(X) | thing(X)      % this holds always

Main proof for -flies(car):

Q1: flies(car) % negated question
9 from Q1, 7: -thing(car) |  $blocker(7,flies(car))
10 from 9, 6:  $blocker(7,flies(car))

Attempt to invalidate the main proof:

11 from 10: -flies(car) % negated question from inside blocker
12 from 11, 4: -bird(car) | $blocker(4,-flies(car))
13 from 12: -penguin(car) | $blocker(4,-flies(car))


does not lead to any new clauses being derived, thus blocker
is not proved. Since there are no more blockers, the main
proof is valid.

== flies(bird) task ==

The same KB as clauses with clause ids and blockers attached
(exactly same as in the previous example):

1: bird(tweety)
2: penguin(pennie)
3: -penguin(X) | -flies(X)  
4: -bird(X) | flies(X) | $blocker(4,-flies(X))    % this is a default rule
5: -penguin(X) | bird(X)  % this holds always

6: thing(car)
7: -thing(X) | -flies(X) | $blocker(7,flies(X)) % this is a default rule
8: -bird(X) | thing(X)      % this holds always

Main proof for flies(tweety):

Q1: -flies(tweety) % negated question
9 from Q1, 4: -bird(tweety) |  $blocker(4,-flies(tweety))   
10 from 9, 1: $blocker(4,-flies(tweety))

Attempt to invalidate the main proof:

11 from 10: flies(tweety)  % negated question from inside blocker
12 from 11, 3: -penguin(tweety) % does not lead to any more derivations
13 from 11, 7: thing(tweety)  | $blocker(7,flies(tweety)) IS NOT ALLOWED
   since rule 7 is less powerful (applicable to a more abstract concept) than 4

no more new clauses can be derived, thus blocker
is not proved. Since there are no more blockers, the main
proof is valid.


== -flies(pennie) task ==

The same KB as clauses with clause ids and blockers attached
(exactly same as in the previous example):

1: bird(tweety)
2: penguin(pennie)
3: -penguin(X) | -flies(X)  
4: -bird(X) | flies(X) | $blocker(4,-flies(X))    % this is a default rule
5: -penguin(X) | bird(X)  % this holds always

6: thing(car)
7: -thing(X) | -flies(X) | $blocker(7,flies(X)) % this is a default rule
8: -bird(X) | thing(X)      % this holds always

Main proof for -flies(pennie):

Main proof 1:

Q1: flies(pennie) % negated question
9 from Q1, 3: -penguin(pennie) 
10 from 9, 2: false % proof found, no blockers to check

Main proof 2: (not strictly necessary, since we already have a valid proof above)

Q1: flies(pennie) % negated question
10 from Q1, 7: -thing(pennie) | $blocker(7,flies(pennie))
11 from 10, 8: -bird(pennie) | $blocker(7,flies(pennie))
12 from 11, 3: -penguin(pennie) | $blocker(7,flies(pennie))
13 from 12, 2: $blocker(7,flies(pennie))

Attempt to invalidate the main proof 2:

11 from 13 above: -flies(pennie)  % negated question from inside blocker
12 from 11, 4: -bird(pennie) | $blocker(4,-flies(pennie)) % IS OK
   since rule 4 is not less powerful than rule 7
13 from 12, 5:  -penguin(pennie) | $blocker(4,-flies(pennie))  
14 from 12, 2: $blocker(4,-flies(pennie)) 

Recursive attempt to invalidate the invalidating proof above:

11 from 14 above: flies(pennie)  % negated question from inside blocker
  % observe that it is the same question as the original goal
  % of the main proof: maybe we should terminate the current
  % search when we see this? Unclear at the moment.
12 from 11, 3: -penguin(pennie) 
13 from 12, 2: false % proof found, no blockers to check

Hence the top-level invalidation proof is itself invalidated, hence
the main proof 2 is also valid.

== Nixon triangle example pacifist(nixon) task ==

Observe that an attempt to prove -pacifist(nixon)
behaves symmetrically to pacifist(nixon), hence we
just bring one goal as an example.

The first attempt will create a potentially
infinite recursion with essentially a random
end result of either proving the goal or not.

=== First attempt: potentially infinite recursion ===

1: republican(nixon)
2: quaker(nixon)
3: -republican(X) | -pacifist(X) | $blocker(3,pacifist(X))  % default rule
4: -quaker(X) | pacifist(X)  | $blocker(4,-pacifist(X))  % default rule

Main proof for pacifist(nixon):

Main proof:

Q1: -pacifist(nixon) % negated question
5 from Q1, 4: -quaker(nixon) | $blocker(4,-pacifist(nixon))
6 from 5, 2: $blocker(4,-pacifist(nixon))

Attempt to invalidate the main proof:

Q1 from 6 above: pacifist(nixon) % negated question from inside blocker
7 from Q1, 3: -republican(nixon) | $blocker(3,pacifist(nixon)) % this is OK
  since there is no order between rule 4 and rule 3: 4 is not stronger than 3
8 from 7, 1: $blocker(3,pacifist(nixon))

Attempt to invalidate the invalidating proof above:

Q1: -pacifist(nixon) % negated question from the blocker clause 8 above
   % NB! This is the same goal as in the original proof
   % Maybe we should stop here? Unclear at the moment
...
Here the proof succeeds exactly like the main proof above:
nothing can block any of these two default rules

Hence the invalidating proof is invalidated and we can recursively
invalidate this one, which goes potentially infinitely deep, 
BUT since time limits get at least halved each time, we will
soon run to the minimal time limit, and then the invalidation fails,
thus the layer above succeeds, invalidating layer above it,
i.e. going from success to failure between each layer.

The main top level proof is either invalidated or not, depending
on the random coincidence of at which layer the allocated time
fell below the accepted threshold.

=== Second attempt: can we limit recursion? ===

A hypothesis of how to approach this: let us 
collect the resulting blockers from the branch as
a new set of axioms:

a1: -pacifist(nixon) % from the result of main proof $blocker(4,-pacifist(nixon))
a2: pacifist(nixon) % from the result of the first invalidating proof $blocker(7,pacifist(nixon))

Let us remove all the axioms which have a stronger corresponding blocker as one of the axiom sources.
I.e. we keep only axioms coming from the strongest (or equal or incomparable) blockers.

Here nothing is removed.

When the resulting clause set is contradictory, we invalidate the main proof.

A simplified version of this argument is simply looking up the tree in the
recursive invalidation branch: is there a direct contradiction with a clause coming
from the blockers from one of the layers above, while the corresponding blocker at the layer
above is not weaker than the current lower blocker?

If there is a contradiction, invalidate the main proof and do not recurse
further.




== Modified flies(bird) task with a chain of default rules used ==

We replace bird(tweety) with:

haswings(tweety)
haswings(X) => bird(X) default rule

The clause set is:

1: haswings(tweety)
2: penguin(pennie)
3: -penguin(X) | -flies(X)  
4: -bird(X) | flies(X) | $blocker(4,-flies(X))    % this is a default rule
5: -penguin(X) | bird(X)  % this holds always
6: -haswings(X) | bird(X) | $blocker(6,-bird(X))    % this is a default rule

Here let default rule 6 be stronger than the default rule 4

Main proof for flies(tweety):

Q1: -flies(tweety) % negated question
9 from Q1, 4: -bird(tweety) |  $blocker(4,-flies(tweety))   
10 from 9, 6: -haswings(tweety) | $blocker(6,-bird(tweety)) | $blocker(4,-flies(tweety)) 
11 from 10, 1: $blocker(6,-bird(tweety)) | $blocker(4,-flies(tweety))

We need to do two separate invalidation attempts: when any
of these succeeds, the whole main proof is invalidated:

Invalidation attempt 1 for $blocker(6,-bird(tweety)):

12 from 11: bird(tweety)  % negated question from inside blocker $blocker(6,-bird(tweety))
13 from 12, 4: flies(tweety) | $blocker(4,-flies(tweety)) % this is NOT applicable
  since the main proof result contains a blocker from a stronger default rule 6

However, even if we DID allow the rule application, we would not find a proof anyway,
hence the invalidation attempt fails.

Invalidation attempt 2 for $blocker(4,-flies(tweety)):

12 from 11: flies(tweety)  % negated question from inside blocker $blocker(4,-flies(tweety))
13 from 12, 3: -penguin(tweety) % this does not lead to any more clauses derived

Hence the invalidation fails.

Since both invalidations failed, the main proof is accepted.

Notice that once we have several blockers in the proof, it is not
immediately clear how to exactly use the ordering of the defaults:
this requires some further thinking.