I should wait for Pat to answer this, but just so I understand the
question - why is this a problem? I thought the entire point of "that" in
IKL was that it wasn't a quoted proposition, so you can quantify over it
just like anything else.
'Since propositions are first-class objects, they can be quantified over
in the usual way, so one can write general axioms about propositions. For
example, we can define a function on propositions corresponding to
disjunction, similarly to the one defined earlier for unary relations."
[1]
What precisely do you mean by "computational"? Anyways, I think you can do
that in IKL (maybe not KIF), but again, Pat should answer.
[1]http://www.ihmc.us/users/phayes/IKL/GUIDE/GUIDE.html#propositionNames
On Sat, 21 Apr 2007,
Dan Connolly wrote:
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? i.e. to write
rules like this?
(forall ((a sentence) (b sentence))
(if (and (that a) (that b))
((that (and a b)) ) )
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"
)
)
)
--
--harry
Harry Halpin
Informatics, University of Edinburgh
http://www.ibiblio.org/hhalpin
