In Lambda-Prolog , I see essentially universal quantifier or essentially existential quantifier such terms, I am confused. It seems the universal quantification of a variable in program or goal is not same as essentially universal quantification. why there is such thing, how to identify such quantification type of variables?
is there anyone explain me? why such concept, why?
thanks in advance
Have a look at Amy Felty's $\lambda$-Prolog tutorial. Essentially universal refers to quantification by either a universal quantifier in a positive position in a formula or an existential quantifier in a negative positive. So in $(\exists x(x = 1)) \Rightarrow (\forall y(y = 1))$, both $x$ and $y$ are essentially universally quantified. The point is that during execution essentially universal variables are treated as variables that can be instantiated while essentially existential variables are treated as constants that represent fixed values.
