- From: Harry Halpin <hhalpin@ibiblio.org>
- Date: Sat, 21 Apr 2007 12:48:08 -0400 (EDT)
- To: Dan Connolly <connolly@w3.org>
- Cc: Pat Hayes <phayes@ihmc.us>, www-archive@w3.org
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
Received on Saturday, 21 April 2007 16:48:12 UTC