Re: function terms in Euler, n3, and RDF [was: gedcom-relation e

> > > [Dan Connolly writing:]
[...]
> > >                                                    If you make the
domain
> > > of :of and :and be :Sum (aka :Integer) and recall that = denotes
> > > daml:equivalentTo,
> > > you can write "the sum of 4 and 3 is 7" as
> > >   [ :of 4; :and 3 ] = 7.
>
> And without that qualification, this doesn't work.  Let's rename and
> avoid [] for clarity.  You're saying:
>
>     7 sum_of_2_part_1 4.
>     7 sum_of_2_part_2 3.

No, that's not what [] mean - (you can't just remove them!) they mean (in
this case)

    There exists x such that
         x sum_of_2_part_1 4.
         x sum_of_2_part_2 3.
         x num:equals 7 .

Tim

PS:

I wouldn't use daml:equivalent because 7 and a thing whose LHS is 2 and RHS
is 5 are different for the reasons you menation - you could deduce that 2+4
was 7.

    There exists x such that
         x sum_of_2_part_1 4.
         x sum_of_2_part_2 3.
        x daml:equiavlent 7 .
    There exists y such that
         y sum_of_2_part_1 2.
         y sum_of_2_part_2 5.
        x daml:equivalent 7 .
But
         x sum_of_2_part_2 3.
        x daml:equiavlent 7 .
imply
        7 sum_of_2_part_2 3
and similarly
        7 sum_of_2_part_2 4
and so on...