Next: Existential quantifier elimination
Up: Quantifier reasoning
Previous: Universal quantifier elimination
  Contents
If we know that a particular object
has a certain property
,
then we should be able to conclude that there exists something
that has the property
. This is called existential quantifier
introduction. In NDL, it is performed with proofs of the form
whose semantics are as follows:
For instance, assuming that the assumption base contains the
atomic formula odd(3), the deduction
will produce the conclusion (exists x odd(x)).
2004-08-06