Next: Universal quantifier introduction
Up: Proof semantics
Previous: Conclusion-annotated proofs
  Contents
Quantifier reasoning
There are four remaining syntax forms in NDL, pick-any,
specialize, pick-witness, and ex-generalize.
These perform quantifier reasoning. Specifically, pick-any
and ex-generalize perform universal and existential
quantifier introduction, respectively; while specialize
and pick-witness perform universal and existential
quantifier elimination, respectively. Their precise assumption-base
semantics are presented below.
2004-08-04