Next: Existential quantifier introduction
Up: Quantifier reasoning
Previous: Universal quantifier introduction
  Contents
If we know that something is true of everything, then
we should be able to conclude that it is true of a particular
individual
. This is called universal elimination because
we go from statements of the form
to
,
thereby removing the universal quantifier. In NDL
this is performed by specialize, whose semantics
are as follows:
It is an error if the universal quantification
is not in the assumption base.
As an example, if
contains (forall x male(father(x))),
then
will produce the conclusion male(father(ann)).
2004-08-06