FOL Quantifiers and TAKE Expressiveness
Alex Zhang
Is it possible to express FOL quantifiers (universal and existential)
in TAKE script? If I understand it correctly, all TAKE rules having
the form of "if ... then ..." can be regarded as having univeral
quantifiers for all its atomic terms. If that is correct, then my
question becomes is it possible to have existential quantifiers in
TAKE script? e.g. to express "some people love sports".
More genernally, Does TAKE have the same expressiveness as FOL? if not
what is the difference?
Thanks a lot,
Alex
Jens Dietrich
Yes, in take the rules have implicit universal quantifiers. However, if
you only want to test whether there are people that love sport, you
could query for this predicate and check whether the result set is not
empty. Because take is based on on-demand computing (iterators), this
will not compute all solutions but only one.
Cheers, Jens
Jens Dietrich
Just to add to my previous post - an easy way to add existential
quantifier support might be to implement it as an aggregation function,
similar to the existing count function.
Cheers, Jens
Alex Zhang
pretty easy to add existential quantifiers in the queries. It is
similar to a "count" query. How about rules or facts? Is it possible
to assert rules or facts with an existential quantifier? I read in
some materials that existential quantifiers can be eliminated with the
use of Skolem functions. However I don't fully understand how Skolem
functions are used. Is it easy to add these kind of things in TAKE?
I am interested in this question because we want to use TAKE for
reasoning in our Chinese language application. And I want to
understand what can and can not be done using TAKE. And how hard is it
to extend TAKE to fill our needs.
Cheers,
Alex
>
> - Show quoted text -
Jens Dietrich
> Thanks for the explanation, Jens. So I understand that it will be
> pretty easy to add existential quantifiers in the queries. It is
> similar to a "count" query. How about rules or facts? Is it possible
> to assert rules or facts with an existential quantifier? I read in
> some materials that existential quantifiers can be eliminated with the
> use of Skolem functions. However I don't fully understand how Skolem
> functions are used. Is it easy to add these kind of things in TAKE?
>
Lets say you have a predicate p(x,y) and you want to build a rule
if exists x:p(x,y) then q(y)
then what you could do is define an aggregation function
aggregation *f** *= count x *p***[x,y]
and rewrite the rule as
if f(y)>0 then q(y)
This is a form of Skolemization - to get rid of an existentially quantified variable by introducing a new function symbol.
The only problem is that count is not very effective - you count ALL x such that p(x,y). It would therefore be better to define
another aggregation function exists very similar to count but only looking whether there is one x. The rule would then simply be:
aggregation *f2** *= exists x *p*[x,y]
if f2(y)=='true' then q(y)
It should be easy to add some syntactic sugar to the scripting language and add simplify this further to:
if f2(y) then q(y)
essentially treating f2 as a predicate.
I will add this as an issue to take, but cannot promise to get this done
soon. Its not difficult though. If you want to do it feel free to do so
and send me the code so that I can qa it and commit it.
Cheers, Jens
Alex Zhang
Thanks for the clarification. Now I understand how Skolemization
works :) I would imagine that once we get our next phase of project
going on TAKE, we will need to extend TAKE to fit our needs. This
skolemization issue should be one of it. Other issues might include 1)
adding multi-line support for defining rules. 2) adding support for
multiple take files forming a "take project". 3) better Eclipse plugin
automations.
If we actually get these extensions done, I will sure send the source
code to you to be considered for adding to TAKE.
Cheers,
Alex