next up previous contents
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