Re: N3->IKL translation seems to work... bug policy rules and log:includes are hairy

>Dan Connolly wrote:
>>   http://www.w3.org/2000/10/swap/n3absyn.py
>>   v 1.13 2007/04/21 06:29:19
>
>I took a look at our hello-world policy
>example, i.e. "if your homepage says you're a vegetarian,
>you're a vegetarian". It comes out having
>log:includes be a relation between propositions,
>not between quoted formulas.
>
>log:includes is supposed to have computational
>characteristics like =p, so this is somewhat
>of a concern. I can't quantify over
>that-sentences in KIF, can I?


Yes, you can :-)

>i.e. to write
>rules like this?
>
>(forall ((a sentence) (b sentence))
>   (if (and (that a) (that b))
>       ((that (and a b)) ) )

Yes, though this syntax is wrong. In fact, you don't even need to 
restrict the quantifiers unless you really want to, since any name 
can be used to refer to a proposition. But here's how you do it. You 
don't use 'that' when quantifying: you just quantify over the actual 
propositions directly. And, IKL treats a proposition as a zero-ary 
relation, so 'caling' it with no arguments, like this (p) , gives you 
its value, ie the truth-value. So to sum up

<sentence>           a sentence, and sentences denote truth-values.
(that <sentence>)     a proposition name, and propnames denote propositions
(p)       where p denotes a proposition, *is* a(n atomic) sentence, 
so has a truth-value.

So for example

((that (exists (x)(R x a)) ))

is an atomic sentence, which is a call of the proposition (=zero-ary relation)

(that (exists (x)(R x a)) )

with no arguments; and this proposition is required by IKL to be true 
just when the 'inner sentence' of its name is, ie just when

(exists (x)(R x a))

is. So these two sentences (only one of which uses a proposition 
name) have the same truthvalue:

((that (exists (x)(R x a))))
          (exists (x)(R x a))

In fact, in general (see the IKL slideshows) for any sentence, these 
are equivalent:

                 <sentence>                         ((that <sentence>))

So, here's how to write the above example:

(forall (a b)(if (and (a)(b)) ((that (and (a)(b)) )) ))

Here,

  (a) , (b) , (and (a)(b)) , ((that (and (a)(b)) ))

are all sentences, and

a  b  (that (and (a)(b)))

are all names of propositions. See?  If it helps, imagine putting an 
argument in all the zero-ary relation calls, and then it would look 
like this:

(forall (a b)(if (and (a x)(b x)) ((that (and (a x)(b x))) x) ))

Hope this helps. Its a bit brain-twisting at first, but you rapidly 
get used to it.

Pat

>
>
>Veg case details...
>
>input is conf_reg_ex.n3 from
>http://www.w3.org/2000/10/swap/test/reason/
>
>output is:
>
>(forall
>  (WHO PG )
>  (and
>   (if (exists
>        (g6 )
>        (and (holds "http://xmlns.com/foaf/0.1/homepage" WHO PG )
>	    (holds
>	     "http://www.w3.org/2000/10/swap/log#includes"
>	     g6
>	     (that
>	      (holds
>	       ('http://www.w3.org/1999/02/22-rdf-syntax-ns#type' c5489120)
>	       WHO
> 
>('file:///Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/conf_reg_ex#Vegetarian' 
>c5489120)
>	       )
>	      ) )
>	    (holds "http://www.w3.org/2000/10/swap/log#semantics" PG g6 )
>	    )
>        )
>       (holds "http://www.w3.org/1999/02/22-rdf-syntax-ns#type"
>	     WHO
> 
>"file:///Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/conf_reg_ex#Vegetarian"
>	     )
>     )
>   (holds
>    "http://xmlns.com/foaf/0.1/homepage"
>
>"file:///Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/joe_profile.n3#joe"
>
>"file:///Users/connolly/w3ccvs/WWW/2000/10/swap/test/reason/joe_profile.n3"
>    )
>   )
>  )
>
>
>
>
>
>--
>Dan Connolly, W3C http://www.w3.org/People/Connolly/


-- 
---------------------------------------------------------------------
IHMC		(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32502			(850)291 0667    cell
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes

Received on Sunday, 22 April 2007 20:33:48 UTC