The functions and::ConsistentW? and and::InferFrom **are similar in structure, and**
are not presented due to space limitations. It is important to note that the **ConsistentW?**
functions return false only to indicate that they are unable **to prove** conclusively **that the**
individual is consistent or inconsistent; if an inconsistency is found, an **InconsistentExcn**
is raised. Also, after an update there may be several individuals about which incompatible information will be asserted. The system only guarantees to **find** one **such case, and then**
rejects the update.

The following is an example of a specialized function for the case Q=all**, which implements the first inference rule presented earlier**
all::Recognizes?(b:<Individual>, all(r:<Role>,vr:<**NormalizedConcept**>),
fillers:<SET(Individual)>, clsd?:<Bool>) returns <**Bool**>
{**if not clsd? then return false** /*More fillers might come later*/
else for every f in fillers do
{if not and**::Recognizes?(f,vr)**
then return false;}
return true }

## 5.2 Reasoning With Incremental Updates

Since updates to individuals are incremental in nature, in order to improve efficiency we want to take into account the fact that the KBMS had already performed all the inferences up to, but not including, the current update. For example, if some individual Tintin has been asserted to be an instance of all(pet,DOG), and already has pet-fillers d1 and d2**, then**
if the current update is assert-fills(Tintin,pet,Fido)**, then we only need to propagate**
the information that pet-fillers are DOGs to Fido**, since the others would have been processed**
earlier. And, if the current update is assert-closed(Tintin,pet)**, then no new role-filler**
information can be inferred from this because of the all **restriction, so we should not even** bother calling all::InferFrom**. We will therefore distinguish the following three variants**
of Q**::InferFrom**:
Q::InferFromClosing(<Individual>,<NormalizedQ-term>,<Role>) **, and**
Q::InferFromAsserting(<Individual>,<NormalizedQ**-Term**>)
plus similar variants of Q::ConsistentW?**. For example**
- all:ConsistentWFilling?(ind, all(r,vr), r, newfiller) invokes and::ConsistentWAsserting?(newfiller,vr) **to check that the new filler does not contradict the**
role restriction vr;
- all::ConsistentWClosing?(ind,all(r,vr),r) **just returns true, and hence is hopefully eliminated by the compiler;**