IRC log of dig on 2007-02-13

Timestamps are in UTC.

01:33:19 [djweitzner]
djweitzner (n=djweitzn@pool-70-108-167-73.washdc.east.verizon.net) has joined #dig
02:42:39 [djweitzner]
djweitzner has quit ()
02:54:42 [djweitzner]
djweitzner (n=djweitzn@pool-70-108-167-73.washdc.east.verizon.net) has joined #dig
04:03:46 [djweitzner]
djweitzner has quit ()
04:18:27 [timbl]
timbl (n=timbl@212.49.149.114) has joined #dig
04:41:21 [timbl]
timbl has quit (Read error: 113 (No route to host))
11:35:23 [djweitzner]
djweitzner (n=djweitzn@pool-70-108-208-211.washdc.east.verizon.net) has joined #dig
12:49:21 [RalphS]
RalphS (n=swick@30-6-113.wireless.csail.mit.edu) has joined #dig
12:54:56 [djweitzner]
djweitzner has quit ()
13:42:31 [[DiG]Tratonis]
[DiG]Tratonis (n=odintg@i577A90A6.versanet.de) has joined #dig
13:43:03 [[DiG]Tratonis]
[DiG]Tratonis has left #dig
15:54:33 [djweitzner]
djweitzner (n=djweitzn@gandalf.mindlab.umd.edu) has joined #dig
16:24:15 [sandro]
sandro has quit ("Terminated with extreme prejudice - dircproxy 1.0.5")
16:24:29 [sandro]
sandro (n=sandro@homer.w3.org) has joined #dig
18:15:39 [djweitzner]
djweitzner has quit ()
18:20:49 [djweitzner]
djweitzner (n=djweitzn@gandalf.mindlab.umd.edu) has joined #dig
18:29:31 [yosi_s]
yosi_s (n=chatzill@w3cdhcp27.w3.org) has joined #dig
20:09:24 [djweitzner]
djweitzner has quit ()
20:31:03 [yosi_s]
DanC, I think I have cwm not splitting bNodes in proofs
20:31:07 [yosi_s]
tests are running
20:32:29 [DanC]
ooh!
20:32:32 [DanC]
very timely
20:33:15 [DanC]
I just checked in some xml/xpath related stuff. I wasn't as careful as perhaps I should have been about running tests before I checked it in
20:39:16 [yosi_s]
the problem was that there was no preexissting way in cwm to get a formula containing a specific set of triples
20:39:30 [yosi_s]
which is what was needed
20:39:37 [yosi_s]
this has now been changed
20:39:46 [yosi_s]
it is, perhaps, not perfect
20:40:01 [yosi_s]
hmm...
20:40:49 [DanC]
are you gonna be here for a little while?
20:41:04 [DanC]
i.e. if I cvs update and find it's all broken, will you be here to help me fix it?
20:43:32 [yosi_s]
[[
20:43:38 [yosi_s]
@prefix : <gmpbnode#>.
20:43:40 [yosi_s]
@keywords is, of, a.
20:43:42 [yosi_s]
dan a Man; home [].
20:43:43 [yosi_s]
{ ?WHO home ?WHERE.
20:43:45 [yosi_s]
?WHERE in ?REGION } => { ?WHO homeRegion ?REGION }.
20:43:47 [yosi_s]
{ dan home ?WHERE} => {?WHERE in Texas} .
20:43:48 [yosi_s]
]]
20:44:01 [yosi_s]
what should the proof look like?
20:45:42 [yosi_s]
DanC?
20:48:22 [DanC]
1. parsing. 2. dan home [], by extraction from 1
20:48:55 [DanC]
3. { dan home ?WHERE} => {?WHERE in Texas} . by extraction. 4. dan home [ in Texas] by rule on 3 applied to 2
20:49:13 [DanC]
5. ... { ?WHO homeRegion ?REGION }. by extraction from 1
20:49:37 [DanC]
6. dan homeRegion Texas by rule from line 5 applied to 4
20:49:39 [DanC]
QED.
20:49:59 [yosi_s]
ok. Here we have a problem. Cwm will generate: 4. [ in Texas ]
20:50:54 [DanC]
well, that's clearly bogus...
20:51:43 [DanC]
... does it have dan home [] in evidence at step 6?
20:53:23 [yosi_s]
http://pastebin.ca/354204
20:53:52 [yosi_s]
yes DanC, it does have that in evidence
20:56:07 [DanC]
lines 2 and 6 are split, bogusly
20:56:31 [DanC]
#
20:56:31 [DanC]
8: :dan :homeRegion :Texas .
20:56:31 [DanC]
#
20:56:31 [DanC]
[by rule from step 7 applied to steps [2, 6
20:57:39 [DanC]
ew... is cwm's reasoning unsound altogether?
20:57:53 [DanC]
lines 2 and 6 have different justifications, which suggests they _should_ be split.
20:58:22 [yosi_s]
that was my point
20:58:26 [DanC]
is this a case of one triple having 2 justifications, and cwm getting confused as a result?
20:58:34 [yosi_s]
no
20:58:49 [yosi_s]
every triple has one justification in this example
20:59:26 [yosi_s]
but the fact that dan lives somewhere, and that that somewhere is in Texas, have different justifications
21:00:49 [DanC]
the rule { dan home ?WHERE} => {?WHERE in Texas} can't conclude 2 triples on my line 4, can it.
21:03:33 [DanC]
ouch. my head is exploding.
21:04:23 [yosi_s]
welocome to my world
21:04:28 [yosi_s]
welcome
21:04:41 [DanC]
there's some wierd skolemization going on somewhere in cwm's reasoning... or something.
21:05:37 [yosi_s]
the problem is not the reasoning
21:05:55 [yosi_s]
the problem is the expressivity of the proof format
21:05:59 [DanC]
I think this example goes beyond the proof structures we have so far. right.
21:06:27 [yosi_s]
I don't see how to fix this --- n3 is not sufficiently introspective
21:06:37 [DanC]
cwm should probably throw an exception when asked to generate a proof in this case, for now. file a bug or something.
21:07:41 [DanC]
meanwhile, the code you've got is no worse than what we had before, and in some cases better, yes?
21:08:54 [DanC]
agenda+ moving from cvs to hg
21:09:08 [DanC]
agenda+ moving swap from cvs to hg
21:10:12 [yosi_s]
yes
21:10:37 [yosi_s]
I had introduced a bug
21:10:41 [yosi_s]
rerunning tests
21:28:18 [DanC]
how does cwm know/decide to unify the conclusion of { dan home ?WHERE} => {?WHERE in Texas} with dan home []? that has me puzzled.
21:29:18 [[DiG]Tratonis]
[DiG]Tratonis (n=odintg@i577A94A0.versanet.de) has joined #dig
21:29:47 [DanC]
I bet it has to re-open a formula to do that.
21:31:27 [yosi_s]
that was not hard at all for cwm
21:31:37 [yosi_s]
the bNode is a constant
21:31:45 [yosi_s]
it simply does the right thing
21:32:28 [yosi_s]
we only run into a problem because cwm is trying to represent a bNode with a bNode in the proof, and it's not working
21:34:27 [DanC]
"the bNode is a constant" <- that's skolemization, in a nutshell.
21:35:31 [yosi_s]
yes
21:35:50 [yosi_s]
-- committed
21:41:01 [Tratonis]
Tratonis (n=odintg@i577A94A0.versanet.de) has joined #dig
21:41:24 [Tratonis]
Tratonis has left #dig
21:43:07 [DanC]
yay; the original dan/texas case from the bug report works.
21:45:01 [[DiG]Tratonis]
[DiG]Tratonis has quit (Read error: 104 (Connection reset by peer))
21:48:48 [DanC]
Subject: toward cwm/N3/reason proof of httpRange-14 argument
21:48:48 [DanC]
Date: Mon, 11 Sep 2006 09:46:52 -0500
21:48:51 [DanC]
trying that one...
21:50:13 [DanC]
definitely
21:51:08 [DanC]
the httpRange-14 argument proof seems to work...
21:51:38 [DanC]
it shows that I haven't implemented support for log:supports in the check.py --report option
21:51:40 [yosi_s]
yosi_s has quit ("Chatzilla 0.9.77 [Firefox 1.5.0.9/2007012620]")
22:05:36 [timbl]
timbl (n=timbl@146-115-112-112.c3-0.lex-ubr1.sbo-lex.ma.cable.rcn.com) has joined #dig
22:24:24 [DanC]
yosi left at xx:51
22:24:51 [DanC]
but he fixed that bnode splitting bug first!
22:25:06 [DanC]
of course, he found a research problem while he was at it
22:36:56 [sandro]
sandro has quit ("Getting off stoned server - dircproxy 1.0.5")
22:37:28 [sandro]
sandro (n=nsandro@homer.w3.org) has joined #dig
22:53:11 [timbl]
timbl has quit ()
23:30:45 [timbl]
timbl (n=timbl@146-115-112-112.c3-0.lex-ubr1.sbo-lex.ma.cable.rcn.com) has joined #dig