|
|
|
|
|
|
by JadeNB
2378 days ago
|
|
|
> I'm pretty sure quantification exists implicitly, but I'm too rusty. Indeed, as in most informal logic, all free variables are implicitly universally quantified. I think the thing that makes it seem like it's not so is that people see a clause like: p(X) :- q(X).
and think "oh, that X isn't really universally quantified, because p(X) isn't always true", but it really is universally quantified; what we're saying is: ∀X, p(X) ← q(X).
i.e., for all X values, in order to prove p(X), it suffices to prove q(X). See, for example, https://en.wikipedia.org/wiki/Horn_clause#Definition , which says> In the non-propositional case, all variables[note 2] in a clause are implicitly universally quantified with the scope being the entire clause. Prolog's resolution exactly follows this proof strategy; see, for example, https://en.wikipedia.org/wiki/SLD_resolution . |
|
|