00:00:23 the backcvahiner in closed world prover,closed world refuter,unification laws 00:00:24 SeanP has joined #rdfig 00:00:26 SeanP has quit 00:00:29 dajobe has quit 00:00:31 sbp has quit 00:00:39 sbp has joined #rdfig 00:00:44 xena has quit 00:01:05 well that is what i am doing now.. fighting logicians to prove the system is sound 00:01:21 Heh. 00:01:27 hopefull i wont get into tooo much hot water 00:01:55 right now the system is operationg 100% sound 00:02:02 by ALL of their tests 00:02:14 but they hate how it worksd becasue its very confussing 00:02:41 I'll beleive it. 00:02:45 It *sounds* confusing. 00:02:54 well let me send you 2 emails.. 00:03:11 you dont have to read them over.. but later can use it for refernce 00:03:24 Heh :) 00:03:35 iut explains how each partition gets filled by n3/suo 00:04:00 xena has joined #rdfig 00:04:06 xena has quit 00:04:28 tim has joined #rdfig 00:04:31 timbl has quit 00:04:39 xena has joined #rdfig 00:04:43 Tim! Get a stable connection! Xena too! 00:05:35 tim has quit 00:05:35 timbl has joined #rdfig 00:05:38 turn off parts and joins ;) 00:05:58 ok mail is sent 00:06:06 Cool. 00:06:43 Aaron, you need to get involved more with #rdfig...I'm in danger of overtaking you in the stats list. 00:06:52 Uh oh! 00:06:56 tim has joined #rdfig 00:07:03 I'm trying to cut down on my IRC. 00:07:07 And I *realy* don't want that to happne. 00:07:08 NO! 00:07:13 Concentrate it *all* here. 00:07:18 Heh heh heh. 00:08:48 timbl has quit 00:08:54 timbl has joined #rdfig 00:10:08 tim has quit 00:10:10 tim has joined #rdfig 00:10:13 timbl has quit 00:11:08 timbl has joined #rdfig 00:13:12 tim has quit 00:13:39 nephLAB is now known as dmiles 00:13:55 tim has joined #rdfig 00:14:09 timbl has quit 00:14:38 timbl has joined #rdfig 00:14:41 tim has quit 00:15:30 timbl has quit 00:15:32 tim has joined #rdfig 00:15:51 tim has quit 00:15:56 timbl has joined #rdfig 00:16:26 timbl has quit 00:16:27 tim has joined #rdfig 00:16:51 timbl has joined #rdfig 00:16:51 tim has quit 00:17:07 timbl has quit 00:17:11 timbl has joined #rdfig 00:17:41 bijan: i am going to write a doc on how the proof proceddure works over the 7 partitions.. i'll forward that to you as well.. i think cwm uses proving and prove and indentity 00:18:04 Ah! 00:18:12 tim has joined #rdfig 00:18:13 timbl has quit 00:18:16 You're not actually using N3 in sigma are you? 00:18:29 will be.. the work order was sent in 00:18:44 Heh. Guess I should put a licence on my code :) 00:18:49 but it was "convert n3 to sigma" 00:18:51 timbl has joined #rdfig 00:19:03 but that is going to ber done by a javba developer 00:19:14 and i'll not have to parse n3 00:19:20 Ah :) 00:19:23 timbl has quit 00:19:33 tim has quit 00:19:34 They going to convert it to Kif or something? 00:19:55 timbl has joined #rdfig 00:20:03 exacly .. so i sent the example DanC gave me for the java guy 00:20:08 Aha! 00:20:17 oh that was rdf to KIF 00:20:30 heh. *not* the same deal, mon ami. 00:20:39 but n3 is going to get embeded in rdf i am assumeiong and needs to work as well 00:20:58 Well, if you trust the n3-->RDF converter in cwm :) 00:21:27 tim has joined #rdfig 00:22:14 tim2 has joined #rdfig 00:22:14 tim has quit 00:22:15 well, if there are some things that dont work right.. i'll be able to say it's not my fayult and the java guy can troubleshoot hopefully 00:22:16 timbl has quit 00:22:21 heh. 00:23:09 * tim2 tries switching wireless cards 00:23:10 just doing the kif is a whole person job 00:23:15 parseType="log:Quote", sheesh. 00:23:30 Woops. timforreal is here :) 00:24:52 cool in you rdf/4 database.. you keep context 00:24:52 tim2 has quit 00:26:01 if you have a _:term.. that defaults to the 4 th argument? 00:26:20 haven't dealt with _:terms yet. 00:26:35 ah.. well it wont be hard anyways 00:26:38 Nope. 00:27:02 You're email is interesting. 00:27:24 i am just wondering from a discussion a few weeks ago with Sean .. if there will be a differnce between _:term and this:term 00:27:39 Er...*has* to be, yes? 00:27:51 _:term is Anonymous isn't it? 00:28:09 well probly peole dont need it.. but any feature like that could be usefull 00:28:18 yes as in all contexts 00:28:50 this:term would be current_module(X),X:term 00:29:35 current_context? 00:29:53 (reussing swi's module system) but yes the 4th argument to the rdf/4 00:29:59 right. 00:30:17 Hmm. I'm not following. 00:30:39 its not important really.. but it has to how legal equivantTo will be 00:30:48 I thought that _:term dc:foo "bar". is the same as [dc:foo "bar"]. in terms of what gets generated. 00:30:50 or where it can be applied 00:31:13 yeah thats right .. so remopve the word 'this' 00:31:44 this:term would be scoped to a context....the term woudl have to be defined in that context? 00:31:51 oh but hi think _:term and :term are differnt right? 00:32:12 Yes they are. 00:32:27 :term is prefixed with the empty namespace which defaults to teh docuemtn namespace. 00:32:36 ok then i guess the inference system needs two way s of unifying outsiude of context 00:34:00 i am just thinking of how/why your own iunifiaction proceedure is actually going to be required 00:34:29 and seems like you want to keep that control 00:34:36 Yep. 00:34:38 (wwhich you have) 00:34:53 I presume that CWM style inference isn't the only kind one might want to do with N3. 00:35:30 sigma if able to use n3 at some time is not closed world 00:35:40 * sbp has managed to get key generation into CWM... with a few hacks along the way 00:35:47 Congrats! 00:36:00 Now learn some prolog and help me :) 00:36:02 * AaronSw needs someone to explain ProofBasedAuthorization to him sometime... 00:37:05 okj.. picking up my dad at greyhound.. bbl 00:37:15 Take care. 00:37:21 Thanks for the Prolog talk :) 00:37:24 oh i gues i am here for 15 jmore minutes 00:37:42 Damn, I'd gotten my slander muscle all tensed up! ;) 00:37:45 speaking of which.. did you see the bug 40 part of the email? 00:38:11 i pasted it at the very bottem 00:38:55 Looking at it. 00:39:41 timbl has joined #rdfig 00:40:12 * timbl apologizes for bad connection earlier 00:40:22 the part that i need to really confrim is that my canonicalization is correct 00:40:24 We forgive you, timbl. 00:40:27 Catching up.. 00:40:51 No, all kinds of inference can be doine with N3. Jos' Euler does backward chaining for example. 00:41:35 _:term is very different from :term. :term is just a idenifier like foo:term. 00:41:42 in n3 is there a log:entails ? 00:41:47 dmiles, My eyes are throbbing. Couldn't confirm that cheese smelt good at the moment. 00:42:28 What would you want log:entails to do? 00:42:56 it woiuld be without contropositves that implies creates 00:43:09 for example: 00:43:10 * sbp notes that he has key generation working in CWM, but it getting quite stuck 00:43:18 s/it/is/ 00:44:03 Sean, I've checked in your earlier math and crypto modules. 1e6 thanks! 00:44:22 ah, thanks for checking them in 00:44:36 I managed to install amx Crypto... 00:44:37 ?x log:implies ?y == ?x log:entails ?y .. [log:not ?y] log:entails [log:not ?x] 00:44:51 Eww. 00:45:06 Er...maybe not eww. 00:45:10 throbbing eyes and all that. 00:45:28 ".."? 00:45:44 timbl: i am not very good at n3 syntax yet 00:46:13 Well, no one has witten "not" in it yet! 00:46:27 oh .. hrrm 00:47:19 i have found entailment is better for backchain. thats why i am asking 00:47:38 implies has too many bumpynesses 00:48:21 implies just 'works' .. but there could be more 00:48:22 So an entailment statement in hte store would be something you can use for inference to fire a rule? 00:48:33 exacly 00:48:43 That, implies does. 00:49:01 Theer are other thingfs one could do with implies |entails. 00:49:10 yes.. but that renders it incapable of modus-tollens 00:49:27 1. test whether given a set of axioms and F you can deduce G. 00:49:33 (refering to using only implies for bachaining) 00:49:55 * bijan is *so* glad dmiles and timbl understand each other; /me can generally only understand one of them at a time :) 00:50:08 * timbl :) 00:50:18 * timbl is only pretending to understand 00:50:32 * dmiles notes this is very interesting but will have to leave in 5 minutes :( *cries* 00:50:43 2. do manipulation of implies using axioms for implies. 00:50:46 Yes, but i can only pretend with one of you. But when you are pretending to understand *each other*, my pretence fails! 00:51:03 i think i am saying that implies is authorial and entailment is actually what infernce does 00:51:07 * timbl will have to leave too 00:51:18 and come back and leave and come back and leave... :) 00:51:35 Then I'll be talking to myself again, and *still* not understanding! 00:51:36 * timbl sighs 00:51:39 i see so by keeping an authorial 'implies' you can do dififernt sort of inference 00:52:02 if you lket people use entailment they would end up probly not ussing it the way inference would 00:52:06 * timbl suspects bijan thinks he doesn't understand cos he is the only one who really does 00:52:26 Yes, my wisdom is socratic only :) 00:52:49 Theer is no "not" in n3 but there are some operators which have converses. log:includes is one. 00:53:05 If it's good enough for Socrates, it's good enough for me! Er..unless it's hemlock. I'd prefer something a bit quicker and less painful, thanks. 00:53:09 but 'implies' gives the logician user more power 00:53:33 whould you agrree that log:implies has a converse? 00:53:50 I don't understand what you would have entailment do in an inference engine. 00:53:57 (although only deducaable) 00:54:01 And what is the bumpines of implies? 00:54:25 And other questions which I can't listen to the answers for :-((( 00:54:28 one sec.. let me opehn a port.. so i can show you.. 00:54:31 Heh. 00:54:32 * timbl cries too 00:54:36 Just as I was understadning too! 00:54:50 I was even composing a line to clarify *everything*. 00:54:55 Wasted. 00:55:21 here: http://216.39.172.56:8080/inference/skb.jsp?req=SA&skb=Merge&id=889 00:55:26 the => is implies 00:55:57 * timbl will check the log -- i am sure you are on the verge of resolving all. 00:56:04 timbl has quit 00:56:19 ooo, why the manner attribute switch?! 00:56:25 then here is the next one; http://216.39.172.56:8080/inference/skb.jsp?req=SA&skb=Merge&id=338 00:56:29 Are those *alternative* compiled forms? 00:56:39 i am not sure actually.. that is authorial 00:56:53 those are the xcompliled prolog usable forms 00:56:53 I wish it were intelligible! 00:57:01 Ah. 00:57:03 (entails ?X ?Y) means Y:-X. 00:57:21 Ah, so the second compiles to three phrases? 00:57:33 And the first to two? 00:57:36 yes.. three prolog staments come pout of it 00:57:41 correct 00:57:55 thats the bumpiness of implies 00:58:08 What is entails again? 00:58:20 its the prolog operator :- 00:58:25 (I.e., implies forces all those entails, it'd be nice to have the entails directly) 00:58:39 Right...Hmm. 00:58:40 my exact point 00:59:09 yes, but is => actually log:implies? 00:59:15 often people misuse 'implies'.. to mean 'entails' ! 00:59:18 i guess that's what you were warning about. 00:59:36 What does implies mean (for you)? 00:59:37 yes, => is actually log:implies 00:59:51 I tend to use implies to mean syntactic implication, i.e., |- 00:59:58 |= 01:00:00 And entails for semantic entailment |= 01:00:15 oh.. i may have my |=,|- switched ;) 01:00:17 This is what logic books do :) 01:00:42 but the concept .. is the poly-interpretaion of 'implies' 01:00:46 So I always have a *terrible* time with all these others :) 01:00:57 poly-interpretation? 01:01:15 is that implies never consequants into only one rule 01:01:40 inless you use (possible (implies A B)) 01:01:50 then it is enailment 01:01:58 yes, but then it has to be that we mean something different by implies and entailment than the logic book version :) 01:02:06 Hmm. 01:02:09 Oh I see. 01:02:13 no i mean the logic book version 01:02:16 I'm getting my metalogic and my logic messed up. 01:02:26 You mean that to do a implication you need a proof. 01:02:36 Whereas for an entailment you can use resolution. 01:02:50 correct 01:03:03 Hmm. 01:03:07 is the system complete? 01:03:07 and unification and triples are all aboiut resolution 01:03:15 yes.. and soiund ;) 01:04:24 I'm not sure that log:implies is, in fact, implies. 01:04:34 nope.. i am just adding modus-tollens logic.. 01:04:40 nope.. i am just adding modus-tollens logic.. 01:04:44 oops 01:04:52 i was scrooled up 01:04:56 Well, one person's modus tollens, etc. 01:04:59 scooled up 01:05:24 oh so maybe log:implies is a logicians entailment 01:05:44 not implication 01:05:51 I think it's just ambiguous ;) 01:06:20 oops.. *ding* my dad bus .. pulled in 01:06:28 must run bbl 01:06:42 Must ask the euler folks ;) 01:06:49 i'll be back in a couple hours 01:06:56 I'll be gone...I hope :) 01:07:05 yes.. this is an important topiuc (for me) 01:07:18 i'll be around tomorrow. 01:07:34 tim-gone has quit 01:07:39 here is another interesting one: http://216.39.172.56:8080/inference/skb.jsp?req=SA&skb=Merge&id=558 01:07:46 log:implies 01:07:47 This implication links two formulae@@. The cwm engine recognises implies as a primitive, and will, when asked to process a rule file, look for any top level implication and find all matches in the store with the left hand side, generating the corresponding 01:08:01 <=> is log:equivance 01:08:21 THat's a totally useless definition, afaict :) 01:08:31 that define 'enatils' 01:08:34 Yep. 01:08:36 err 'entails' 01:08:40 That's waht I was saying :) 01:08:47 CWM just forward chains on it. 01:08:55 ok then so .. we need a real implies as well :) 01:09:21 bbl 01:09:24 tim-gone has joined #rdfig 01:09:37 tim-wavering is back :) 01:12:33 oierw` has joined #rdfig 01:27:04 I was thinking CWM should be re-backronymed to mean CWM works magic (or maybe miracles). 01:29:06 what do you think, sbp? 01:33:12 sbp has quit 01:34:27 sbp has joined #rdfig 01:40:10 chaals has joined #rdfig 01:40:19 * chaals waves 01:51:22 * sbp waves 01:51:27 * oierw waves 02:44:48 chaals has quit 03:00:08 http://infomesh.net/2001/cwm/ 03:00:09 A: http://infomesh.net/2001/cwm/ from sbp 03:00:21 A:|Information about CWM - TimBL's Closed World Machine 03:00:22 titled item A 03:00:37 A:An anthology of information about CWM, what you need to get to run it, related file and work, and so on 03:00:38 commented item A 03:00:48 You better watch out, sbp. Soon you'll be CWM's lead developer! 03:01:22 well, the built-ins are quite easy. I wouldn't touch the inference stuff 03:01:47 So you say... but we'll give you time. 03:01:59 And you said you'd do an inference engine for the Plex. 03:02:39 when you come up with an inference syntax, I told you :-) 03:02:53 We just need to schedule a time... 03:03:29 a time for what? 03:03:41 To design one. 03:04:11 It'd probably best if bijan is around... 03:04:15 bijan, you around? 03:06:44 A:A "How to Download" section would be good, with precise instructions (and even better, a .zip!) 03:06:44 commented item A 03:07:20 er... there is one 03:07:33 there's no zip, just instructions :-) 03:07:55 I could tar.gz my working directory, I suppose 03:08:16 Hmm, I must have missed that bit. 03:08:32 "CWM has managed to get implemented in a few projects." sounds wrong to me... 03:08:36 s/implemented/used/? 03:08:55 yeah, I wondered about, but it was another late night bit of writing... 03:09:04 .time 03:09:04 2001/12/03 03:09:08.41716 Universal 03:09:14 Oh dear... 03:09:52 Yeah, the Installing CWM isn't what I thought of as "precise"... 03:10:16 get the files, put them in a directory. What else do you need to know? 03:10:26 it's hardly rocket science 03:10:35 Getting the files is sort of non-trivial for most people. 03:10:45 Since a) they don't know how many there are, or their names 03:10:55 huh? there's a list on the page! 03:10:58 b) it's annoying to download the 20 or so files that are there... 03:11:03 Oh, heh, there is a list! 03:11:08 Ah, cheerio then. 03:11:15 I withdraw my objection. 03:11:16 dear oh dear... 03:11:26 I must be getting sleepy too... 03:11:57 yes... 03:13:30 Dear, I am sleepy... where did the day go? 03:13:35 And the Ginger reveal tomorrow. 03:14:27 Oooooh! http://www.time.com/time/ 03:15:22 oierw` has quit 03:15:44 oierw` has joined #rdfig 03:23:54 sbp has quit 03:24:10 sbp has joined #rdfig 03:26:54 Odd... 03:27:00 is cwm broken in cvs? 03:27:10 [ronwalf@cerebrus test]$ cwm.py rules12.n3 --filter=filter12.n3 03:27:13 ... 03:27:20 :granpa :ancestor :pa . 03:27:21 03:27:21 :pa :ancestor :bill . 03:27:38 Shouldn't granpa be an ancestor of bill? 03:28:48 erm... pardon? 03:29:15 This is in the test directory 03:29:26 of the cwm repository 03:29:32 It's probably my fault 03:29:42 I'm not following what you're saying 03:30:05 those triples are in rules12.n3 in the first place 03:30:19 Yes, but cwm is concluding anything besides that. 03:30:31 Hmm... 03:30:38 s/any/no/ 03:30:40 you need --think in your command line 03:30:47 * ronwalf slaps himself silly 03:31:12 :-) 03:33:06 I've added a tar.gz file to the CWM info page 03:33:24 Nice. That should make it easier to find 03:34:02 and download, for people just getting into it. I remember when you only needed notation3.py, cwm.py, and sax2rdf.py... the good old days :-) 03:44:53 * ronwalf dances 03:45:15 ropeLights ARE a subclass of http://opencyc.sourceforge.net/daml/cyc.daml#/ElectronicDevice 03:47:03 kick-ass, but shouldn't that be "RopeLights"? 03:47:59 Probably, but that's how they were named. I'm still trying to figure cwm out, so I was using an old n3 file I had around from the first project in 498 03:48:28 What is the capitalization convention here, though? 03:48:57 ah, you're one of Jim's students? 03:49:13 Capitalization: Capitalize classes, don't capitalize properties 03:49:18 :Sean :name "Sean" . 03:49:41 ah, ok, that makes sense. 03:49:49 Yes, I'm one of Hendler's students 03:56:46 oierw` has quit 03:57:47 oierw` has joined #rdfig 04:00:13 * ronwalf heads off for the night 04:00:38 c'ya 04:14:27 back 04:14:36 Hi dmiles 04:14:38 hi Sean 04:15:05 I wrote http://infomesh.net/2001/cwm/ just in case you're interested 04:15:16 did you catch earlier what i was say9ing about entailment vs implies? 04:15:26 I was watching, yes 04:15:35 |- vs. |= 04:15:59 yes.. so i was left withy the impression that log:implies means logical entailment 04:16:02 syntactic implication vs. syntactic entailment, as I recall 04:16:22 yes it is rather syntactic 04:16:54 syntactic implication equals logical entailmetn evidently 04:17:16 excellent link 04:18:19 alot of good stuff to try and use and learn from 04:18:34 thanks 04:19:12 can you define the difference between entialment and implication again, for me? Bijan told me a while ago... 04:19:38 * AaronSw disconnects 04:19:49 entail ment is wahat an inference engine can backchain on.. to do a syntactic math 04:20:03 implication is what a user normally uses in a rule 04:20:27 ah, so entail is <=> and implication is =>, yes? 04:20:32 A implies B.. means A entails B , and Not B entails Not A 04:20:42 oierw` has quit 04:20:57 oierw` has joined #rdfig 04:21:04 <=> means equivalent logically 04:21:15