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
