Draft notes for our approach to reasoning with defaults
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)
Sisukord
-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.
