- 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