IRC log of sw-team on 2003-04-29

Timestamps are in UTC.

17:59:52 [RRSAgent]
RRSAgent has joined #sw-team
17:59:58 [Zakim]
SW_SWAD()2:00PM has now started
17:59:59 [Zakim]
+DanC
18:00:17 [Zakim]
+DanBri
18:00:33 [JosD]
JosD has joined #sw-team
18:00:37 [Zakim]
-DanBri
18:00:46 [reagleMIT]
reagleMIT has joined #sw-team
18:01:03 [Zakim]
+DanBri
18:01:38 [Zakim]
+Marja
18:01:44 [Zakim]
+??P8
18:01:59 [Zakim]
+??P9
18:02:07 [Zakim]
+TimBL
18:02:30 [ryan-lap]
ryan-lap has joined #sw-team
18:02:38 [sandro]
zakim, who is here?
18:02:38 [Zakim]
On the phone I see DanC, DanBri, Marja, JosD, ??P9, TimBL
18:02:39 [Zakim]
On IRC I see ryan-lap, reagleMIT, JosD, RRSAgent, Zakim, marja, danbri, RalphS, Nobu, emscribe, dom, DanC, sandro, ericP, Ralph
18:02:47 [Danny-DC]
Danny-DC has joined #sw-team
18:03:18 [sandro]
Danny, are you joining us today?
18:03:19 [tim-mit]
tim-mit has joined #sw-team
18:03:27 [Danny-DC]
yes, I am.
18:04:20 [DeborahMc]
DeborahMc has joined #sw-team
18:04:53 [JosD]
JosD has joined #sw-team
18:04:53 [tim-mit]
tim-mit has joined #sw-team
18:04:53 [DeborahMc]
DeborahMc has joined #sw-team
18:04:58 [danbri]
odd...
18:05:01 [DanC]
Zakim, Stanford/KSL holds DebM, Paulo
18:05:01 [Zakim]
+DebM, Paulo; got it
18:05:15 [DanC]
Zakim, who's on the phone?
18:05:15 [Zakim]
On the phone I see DanC, DanBri, Marja, JosD, Stanford/KSL, TimBL
18:05:16 [Zakim]
Stanford/KSL has DebM, Paulo
18:05:28 [Zakim]
+Danny
18:05:49 [tim-mit]
Zakim, TimBL is really TimsOffice
18:05:49 [Zakim]
+TimsOffice; got it
18:06:09 [tim-mit]
Zakim, TimsOffice holds TimBL, Sandro, Ryan, EricP
18:06:09 [Zakim]
+TimBL, Sandro, Ryan, EricP; got it
18:07:02 [Zakim]
+EMiller
18:07:55 [sandro]
RRSAgent, pointer?
18:07:55 [RRSAgent]
See http://www.w3.org/2003/04/29-sw-team-irc#T18-07-55
18:08:40 [DanC]
[[ The IRC log will
18:08:40 [DanC]
appear at http://www.w3.org/2003/04/29-sw-team-irc. ]]
18:09:16 [DanC]
------- convene
18:09:19 [DanC]
proposed agenda: http://www.w3.org/2003/04/29/swad/
18:09:58 [ericP-scribe]
sandro: what do we do with the irc log of this conference?
18:10:11 [ericP-scribe]
debM: public is OK with us
18:10:18 [ericP-scribe]
[no objections]
18:10:22 [sandro]
RESOLVED record of this meeting be public
18:10:50 [ericP-scribe]
q+ to be an example
18:11:07 [sandro]
ack ericP-scribe
18:11:07 [Zakim]
ericP-scribe, you wanted to be an example
18:12:18 [ericP-scribe]
sandro: this is DAML-funded research, _not_ rec track or member-supported
18:12:40 [ericP-scribe]
sandro: we'll discuss follow up meetings in the last 15 mins of this meeting
18:12:51 [danbri]
(although we hope some Members are supportive of these efforts... they're just not funding it via Member fees)
18:13:11 [ericP-scribe]
[tim returns]
18:13:40 [ericP-scribe]
sandro: goal: to plan and design for interop between planners, reasoners and explainers
18:14:52 [DeborahMc]
debm cant hear either
18:15:10 [ericP-scribe]
debM, can you hear sandro?
18:15:20 [DeborahMc]
yes sorry - it was just eric
18:15:33 [ericP-scribe]
danc: proving to humans is interesting, but a side goal
18:15:48 [DanC]
*not* a goal, to me, to prove things to human
18:15:54 [DanC]
might be a side benefit
18:15:58 [ericP-scribe]
sandro: debM's interest is in explainer UIs, nto verifiers
18:16:37 [ericP-scribe]
sandro: if PPF works for a verifier, that's just gravy?
18:17:05 [ericP-scribe]
debM: yes, one datapoint of buy-in from the verifyer community
18:17:11 [sandro]
http://www.w3.org/2003/04/29/swad/
18:18:13 [ericP-scribe]
debM: may want to add use cases, perhaps in follow-up email
18:18:43 [ericP-scribe]
sandro: coordinating multiple reasoners, JTP and cwm work on common proof
18:19:06 [tim-mit]
exactly
18:19:13 [ericP-scribe]
paulo: if reasoner B uses reasoner A, it can use the PPF context
18:19:45 [ericP-scribe]
jos: +testing 2nd opinions by idependent reasoners
18:19:55 [DanC]
2nd opinion test cases... pointer? could you follow up in email with pointers?
18:20:56 [ericP-scribe]
paulo: multiple justifications makes proof more complex but allows one to detect contradictions
18:21:18 [DanC]
agenda + reductio ad absurdum, LEM (under C. Issues)
18:21:34 [JosD]
will do that (but proofs are kind of not very human readable...)
18:21:43 [DanC]
agenda + how registration works with registered stuff (under C. Issues)
18:21:54 [ericP-scribe]
paulo: general plan it to focus on justification
18:22:09 [ericP-scribe]
debm: today we provide a proof browser.
18:22:35 [ericP-scribe]
... using rewrite rules to transform proof trace into an explaination, abstracting away some details.
18:22:56 [ericP-scribe]
... could make it more understandable for any particular audience.
18:23:35 [ericP-scribe]
paulo: one way of seeing how a machine arrived at a proof is by verifying the proof
18:23:39 [JosD]
there is the pointer to the original as well
18:23:44 [DanC]
proposed proof language in DAML: http://www.ksl.stanford.edu/software/IW/spec/iw.daml not sure if there's a prose write-up. but that's what I found from the agenda.
18:23:50 [sandro]
http://belo.stanford.edu:8080/iwbrowser/WffBrowser?url=http://www.ksl.stanford.edu/software/IW/sample/TS/IW1.daml
18:24:28 [ericP-scribe]
sandro: i found it easiest to play with browser making chagnes and examining RDF.
18:24:33 [ericP-scribe]
... do you have a prepared path?
18:24:45 [ericP-scribe]
debm: planned to be responsive to your needs.
18:24:56 [ericP-scribe]
[debm walks us trhough tony is a seafood]
18:26:03 [ericP-scribe]
danc, it's all onclick events
18:26:36 [sandro]
http://belo.stanford.edu:8080/iwbrowser/WffBrowser?url=http://www.ksl.stanford.edu/software/IW/sample/TS/IW1.daml
18:27:59 [ericP-scribe]
[viewing with proof style: proof, sentence format: english, lens mag: 3
18:28:00 [ericP-scribe]
]
18:29:02 [DanC]
I'm at http://belo.stanford.edu:8080/iwbrowser/WffBrowser?url=http://www.ksl.stanford.edu/software/IW/sample/TS/IW1.daml
18:29:46 [marja]
I see what danc is seeing
18:29:59 [DanC]
premises to ultimate conclusions I see is "For all values of ?inst: ?inst is a seafood when ?inst is a crab." and "Tony is a crab."
18:30:11 [DeborahMc]
http://belo.stanford.edu:8080/iwbrowser/index.jsp
18:30:59 [DanC]
now I'm at http://belo.stanford.edu:8080/iwbrowser/WffBrowser?url=http://www.ksl.stanford.edu/software/IW/tmp/IW1.daml
18:31:43 [DanC]
eek! same address as before, but different stuff on the screen!
18:33:21 [DanC]
timbl: this is an example of why web architecture says URIs should be unambiguous.
18:34:05 [RalphS]
RalphS has joined #sw-team
18:34:09 [ericP-scribe]
debm: we want feedback on the explainations (rules product)
18:37:58 [DanC]
in N3, { :shellfish s:subClassOf :seafood } is log:includes of [ is log:semantics of <http://www.ksl.stanford.edu/DAML/query-answer/wines-short2.daml>]
18:38:59 [sandro]
deb: side conditions are more premises that we dont anticipate you'd want to see in the proof
18:40:05 [DanC]
patterns of sentences... that resulted in wtr in earlier KIF versions. i.e. quoting ;-) but I gather the CL folks threw out quoting recently
18:40:35 [sandro]
jos: how can I see what the bindings are?
18:40:47 [sandro]
paulo: there;s a supporting document that's not available now
18:40:56 [sandro]
deb: click on "v" box
18:41:08 [DanC]
[[ ?x = |http://www.ksl.stanford.edu/DAML/query-answer/wines-short2.daml#|::|SEAFOOD| ]]
18:41:56 [ericP-scribe]
(the "v" box is after "Tony is a seafood.")
18:42:02 [sandro]
paulo: most reasoners seem to lose bindings when they dump a proof
18:42:16 [sandro]
ack DanC
18:42:16 [Zakim]
DanC, you wanted to check that we're all on the same page and to note including source info in the logic
18:42:51 [ericP-scribe]
danc: having source info off to the side... this is a critical part of the proof. in N3 it's part of the formula.
18:42:56 [DanC]
in N3, { :shellfish s:subClassOf :seafood } is log:includes of [ is log:semantics of <http://www.ksl.stanford.edu/DAML/query-answer/wines-short2.daml>]
18:43:08 [ericP-scribe]
debm: some folks just dump (provenence) on the floor.
18:43:31 [ericP-scribe]
sandro: look at format behinde this?
18:43:42 [danbri]
zakim, drop danbri
18:43:42 [Zakim]
DanBri is being disconnected
18:43:43 [Zakim]
-DanBri
18:44:04 [ericP-scribe]
debm: first, following danc's comment, click on second explaination point.
18:44:38 [RalphS]
"!" are "explanation points"
18:45:02 [ericP-scribe]
paulo: a large proof will have a huge contribution from ground facts.
18:45:25 [ericP-scribe]
danc: you believe this or you don't.
18:45:32 [ericP-scribe]
tim: you can go back to the sources.
18:46:13 [ericP-scribe]
tim: presumably you gave it these documents. to make it complete, you can point back to where you gave it the documents.
18:46:30 [ericP-scribe]
paulo: every step can be related to many documents.
18:46:55 [ericP-scribe]
debm: in this particular case, all came from wine-test.
18:47:18 [ericP-scribe]
tim: you told it where where to get these documents.
18:47:30 [ericP-scribe]
... the eventual proof will be "you told me so".
18:47:49 [ericP-scribe]
... interesting to know what docs were used.
18:47:57 [sandro]
tim: "this is very nice" :-)
18:48:13 [ericP-scribe]
... eg, filling out a tax form and discovering it used a documment you thought was private/personal...
18:48:31 [DeborahMc]
one take away we will add is a summary of all documents used (along with the listing we already have of all ground axioms used)
18:48:56 [ericP-scribe]
paulo: ... creating an annotation mechanism for annotating the sources of ground axioms of your proof.
18:49:09 [ericP-scribe]
sandro: maybe you can point that out in the format.
18:50:01 [drewmcd]
drewmcd has joined #sw-team
18:50:15 [ericP-scribe]
debm: the document icon will take you to the source document of the current node
18:50:28 [ericP-scribe]
paulo: each node of the proof is a separate file.
18:50:39 [sandro]
Welcome, Drew. Are you going to call in?
18:50:45 [ericP-scribe]
... could combine them; there's a tradeoff
18:51:00 [marja]
visual comments: why are the right side lines and left side lines not at the same level? and some more space between the sides would be nice
18:51:01 [drewmcd]
I don't think I'm going to call in
18:51:30 [ericP-scribe]
expected you might want to see the whole inference web spec, but it may be easier via this example.
18:52:01 [ericP-scribe]
debm: we are now looking at the node "the type of tony is seafood."
18:52:39 [ericP-scribe]
sandro: not quite following. these files have a single proof step. are there others that have combinded proof steps?
18:52:51 [DanC]
(timecheck... agenda calls for us to move on to the 2nd C at xx:45)
18:52:53 [DeborahMc]
http://www.ksl.stanford.edu/software/IW/tmp/ is a listing of all of the files used
18:52:57 [ericP-scribe]
paulo: not now. we have generated some cases but not using them now.
18:53:14 [Nobu0]
Nobu0 has joined #sw-team
18:53:31 [RalphS]
[when I follow the source link (document icon), I get an RDF/XML source node that doesn't fit in the fixed-sized browser popup window and the window (is presumably forced) to have no scrollbars]
18:53:34 [ericP-scribe]
paulo: one thing you can do is load a proof as an ontology [rdf graph].
18:54:14 [ericP-scribe]
debm: http://www.ksl.stanford.edu/software/IW/tmp/ has all the files that lead to tony is a seafood.
18:54:28 [ericP-scribe]
... you'll see the 13 pieces of the proof.
18:54:35 [sandro]
danc, understood.
18:54:44 [ericP-scribe]
... now looking at IW1.daml
18:55:05 [sandro]
http://www.ksl.stanford.edu/software/IW/tmp/IW1.daml
18:55:09 [ericP-scribe]
sandro: could you walk us through it more closely?
18:55:27 [ericP-scribe]
paulo: releven part is the iw:WFF
18:55:28 [RalphS]
[I confirm that the first part of http://www.ksl.stanford.edu/software/IW/tmp/IW1.daml appears to match the thing I can't scroll in the source node popup]
18:56:34 [ericP-scribe]
(type Tony SEAFOOD) is a label from the for a node in this proof.
18:56:49 [ericP-scribe]
debm: if you wanted to check this proof, you'd get that string out.
18:57:05 [JosD]
q+
18:57:30 [ericP-scribe]
q+ to ask if iw:KIF denotes <iw:Statement> contents are parsable as KIF
18:57:58 [ericP-scribe]
tim: proof is no longer an RDF graph, it has embedded KIF.
18:58:23 [ericP-scribe]
paulo: it's difficult to get as good as KIF
18:58:35 [ericP-scribe]
tim: why use any RDF at all?
18:58:49 [ericP-scribe]
debm: want to be compatable with RDF and web.
18:59:05 [sandro]
zakim, q?
18:59:05 [Zakim]
I see JosD, ericP-scribe on the speaker queue
18:59:20 [ericP-scribe]
danc: would make sense to do it all in KIF or RDF
18:59:45 [DanC]
timbl notes connection between (type Tony SEAFOOD) and <iw:Term>|http://www.ksl.stanford.edu/DAML/query-answer/wines-short2.daml#|::|SEAFOOD|</iw:Term>
19:00:02 [ericP-scribe]
tim: when i parse that KIF, i have to take it on faith that their aren't two SEAFOODs.
19:00:12 [ericP-scribe]
debm: this is the one without namespaces.
19:00:59 [DanC]
(I've got this paper that sandro mentioned, from Maimi, entitled "Inference Web: Portable Explanations for the Web"; I wonder if I can share it with those present via http URI)
19:01:31 [ericP-scribe]
ericP: you can do namespaces as a pre-processor
19:01:31 [sandro]
ack JosD
19:01:54 [sandro]
JosD: Tony, SEAFOOD, etc should be URIs or qnames or something
19:02:25 [ericP-scribe]
paulo: we can support that. it's just a hack. could have it by afternoon^H^H^H^H^Hevening
19:02:41 [DanC]
ah... http://www.ksl.stanford.edu/people/pp/papers/McGuinness_SSS_2003.pdf has pretty much the same content as the paper Sandro mentioned, with the WFF spelled out as an s-expression in RDF.
19:02:51 [ericP-scribe]
jos: see no convention for labeling rules
19:02:55 [DanC]
from InferenceWeb publications http://www.ksl.stanford.edu/software/IW/papers/
19:03:09 [ericP-scribe]
paulo: there is no inference step related to IW1.
19:03:16 [ericP-scribe]
... but you can in this format.
19:03:34 [ericP-scribe]
... each inference step is the application of one inference rule.
19:04:40 [ericP-scribe]
... can have link to other antecedents of this rule
19:05:01 [sandro]
"hasVariableMapping" == "binding"
19:05:33 [ericP-scribe]
debm: node lable (kif), consequent of inf step using GMP using inf engine JTP.
19:05:43 [ericP-scribe]
... two antecedents IW2 and IW6
19:05:55 [ericP-scribe]
... variable binding ?x := SEAFOOD.
19:08:04 [sandro]
somewhat updated http://www.w3.org/2003/04/29/swad/
19:08:16 [JosD]
q+
19:08:47 [sandro]
ack JosD
19:08:47 [DanC]
ack JosD
19:08:52 [ericP-scribe]
ericP: connection between "SEAFOOD" in "(type Tony SEAFOOD)" and ?x iw:Term "...SEAFOOD".
19:09:15 [ericP-scribe]
jos: what is the label of the implication itself?
19:09:19 [DanC]
<iw:InferenceRule rdf:about='http://www.ksl.stanford.edu/software/IW/registry/IR/GMP.daml'/>
19:09:47 [ericP-scribe]
debm: it's in the inference step.
19:09:53 [ericP-scribe]
... you have the rule: GMP
19:10:04 [ericP-scribe]
... antecedents: IW2, IW6
19:10:10 [ericP-scribe]
... and the consequence.
19:10:58 [ericP-scribe]
debm: either IW2 or IW6 is the implication
19:11:13 [DanC]
i.e.
19:11:14 [DanC]
<iw:WFF rdf:about='http://www.ksl.stanford.edu/software/IW/tmp/IW2.daml'/>
19:11:15 [ericP-scribe]
sandro: the inference step and the rule have the same URI
19:11:59 [ericP-scribe]
... if you separate them, you can graph merge these files.
19:12:11 [DanC]
sandro: if you give the formula in IW2 its own name, you can merge it into the proof file.
19:13:04 [ericP-scribe]
jos: came to the conclusion that "Tony is a seafood", but where is it written?
19:13:17 [ericP-scribe]
danc: how is that not http://www.ksl.stanford.edu/software/IW/tmp/IW2.daml ?
19:13:28 [DanC]
<iw:Statement>(&lt;= (type Tony ?x) (subClassOf CRAB ?x))</iw:Statement>
19:14:18 [Nobu]
Nobu has joined #sw-team
19:14:56 [tim-mit]
http://www.w3.org/2000/10/swap/test/reason/t4.proof <- comparable cwm proof. Use of {} in place of embedding kif in rdf,... variable names are uris,....parsing,....
19:15:21 [ericP-scribe]
debm: we could record how the statement was proved, not just the value of it.
19:15:31 [ericP-scribe]
... seems hard; what's the value?
19:15:56 [ericP-scribe]
tim: suppose we com across this implication and we want to use it elsewhere.
19:16:12 [ericP-scribe]
... you refer to it via the proof step that led to it.
19:16:49 [ericP-scribe]
sandro: hasAntecedent points to the file
19:17:07 [ericP-scribe]
tim: semantics to the extra step.
19:17:21 [Nobu]
Nobu has joined #sw-team
19:17:21 [ericP-scribe]
sandro: need about="" to keep filename
19:17:49 [DanC]
<WFF rdf:about="#thisWF"> would be better, yes
19:17:52 [tim-mit]
about="#wff"
19:18:23 [tim-mit]
<IW2.daml#wff>
19:19:13 [ericP-scribe]
debM: small addition to PPF, which is fine.
19:19:30 [DeborahMc]
we do not see it
19:20:22 [Zakim]
-Danny
19:20:35 [JosD]
bye DanC
19:20:54 [ericP-scribe]
tim compares http://www.w3.org/2000/10/swap/test/reason/t4.proof to PPF...
19:20:59 [DanC]
not, that was Danny Weitzner excusing himself; I'm still here.
19:21:35 [Nobu]
Nobu has joined #sw-team
19:21:46 [ericP-scribe]
tim: one question, how often do you give a copy of the conclusion?
19:21:56 [DanC]
I think "erasure" is a more traditional term than "extraction". hmm... part-of-speech mismatch.
19:22:06 [ericP-scribe]
... ... denoted by "gives" here.
19:22:24 [ericP-scribe]
... use/mention bug in non-quoted variables
19:23:13 [ericP-scribe]
jos: i think you can perfectly use it if you say that verable=that value as part of the explaination.
19:23:25 [DanC]
jos: another option is to say <t4.n3#x> = <c>
19:23:39 [DanC]
i.e. really use the variable, rather than mentioning it in a binding
19:24:33 [DanC]
timbl: problem with referential transparency... if x is bound elsewhere to d, we conclude c=d, no? [DanC wonders...]
19:24:34 [drewmcd]
drewmcd has joined #sw-team
19:24:52 [JosD]
http://www.agfa.com/w3c/euler/gedcom-proof.n3
19:25:35 [ericP-scribe]
sandro: tim, you have a good sense of what inference is doing. do you think cwm could output their files.
19:25:48 [JosD]
what I meant was eg {?C2 = :Rita. ?F = :dp. ?C2 gc:childIn ?F} => {:Rita gc:childIn :dp}.
19:26:02 [DanC]
doing the design in KIF and putting the <>s on later would be easier, for me
19:26:22 [ericP-scribe]
tim: problem is the mixture of KIF.
19:26:36 [ericP-scribe]
... the KIF can be arbitrarily complex
19:26:49 [DanC]
KIF syntax is *much* simpler than s-expr-in-RDF syntax.
19:28:59 [DanC]
I've implemented URI namespaces in KIF
19:29:02 [ericP-scribe]
sandro: KIF is easy to parse.
19:29:21 [ericP-scribe]
... but we need a standard for what URIs mean in KIF.
19:29:36 [ericP-scribe]
debm: namespace issue is not a big one for KIF.
19:29:45 [DanC]
http://www.w3.org/2000/10/swap/kifExpr.html
19:30:10 [tim-mit]
wine<pickyour punctuation symbol>SEAFOOD
19:30:33 [DanC]
http://www.w3.org/2000/10/swap/KIFSink.py
19:30:57 [ericP-scribe]
sandro: the iw:KIF element is a crucial part of this proof.
19:31:21 [drewmcd]
What would a "standard for what URIs mean" look like?
19:31:30 [ericP-scribe]
debm: it would be easy to add <iw:n3>
19:31:47 [ericP-scribe]
debm: ansi-KIF and ansi-stamped
19:31:54 [ericP-scribe]
danc: is it the bible?
19:32:03 [Nobu]
Nobu has joined #sw-team
19:32:07 [ericP-scribe]
debm: nah. we use ansi kiff.
19:32:28 [tim-mit]
debm: we can read either
19:32:35 [sandro]
Deb: a lot of people still using KIF 3.0 because ansi kif dropped some things people cared about
19:32:46 [ericP-scribe]
... some use kif3.0 'cause ansi dropped a couple things that people care about
19:32:49 [DanC]
ack DanC
19:32:49 [Zakim]
DanC, you wanted to talk about registration and verification
19:33:11 [ericP-scribe]
dabc: stronger form of weakly queue is the one i care about.
19:33:21 [RalphS]
s/weakly queue/wtr/
19:33:27 [RalphS]
(weakly true)
19:33:33 [ericP-scribe]
tim: brackets are for putting n3 in n3
19:33:35 [tim-mit]
deb, are you there?
19:33:38 [sandro]
DEB -- we cant hear ytou
19:33:44 [DanC]
s/one I care about/one that seems most relevant/
19:33:51 [tim-mit]
zakim, who is here?
19:33:51 [Zakim]
On the phone I see DanC, Marja, JosD, Stanford/KSL, TimsOffice, EMiller
19:33:53 [Zakim]
Stanford/KSL has DebM, Paulo
19:33:54 [Zakim]
TimsOffice has TimBL, Sandro, Ryan, EricP, RalphS
19:33:55 [Zakim]
On IRC I see Nobu, drewmcd, RalphS, DeborahMc, tim-mit, JosD, Danny-DC, ryan-lap, reagleMIT, RRSAgent, Zakim, marja, danbri, em, dom, DanC, sandro, ericP-scribe, Ralph
19:34:15 [ericP-scribe]
... want to use n3 on the inside and the outside.
19:34:44 [ericP-scribe]
danc: cheaper to get rid of the points and use KIF.
19:35:43 [ericP-scribe]
tim: declare the ns at the top and quote the document
19:35:47 [DanC]
I prefer uniform, self-similar syntax to any particular syntax. i.e. all-RDF or all KIF or all N3 is preferable to XML/KIF or KIF/N3 mix.
19:35:49 [drewmcd]
drewmcd has joined #sw-team
19:36:00 [sandro]
tim: It would be great to have a std way to put URIs into and out of KIF.
19:36:12 [sandro]
tim: If we had that, write your proof language in KIF.
19:36:24 [sandro]
...: If you need the power of KIF, you need the power of KIF.
19:36:43 [sandro]
...: the mixture of RDF/XML and KIF seems messy.
19:37:17 [em]
q+
19:37:18 [sandro]
Deb: followup on NS in KIF
19:37:20 [ericP-scribe]
debm: action item for a subset of us to have conversation on ns in kiff?
19:37:40 [ericP-scribe]
danc: that's not my biggest issue with this PPF.
19:37:48 [em]
q-
19:37:58 [sandro]
MAJOR ISSUE: KIF
19:38:23 [Nobu]
Nobu has joined #sw-team
19:38:23 [ericP-scribe]
... point of a proof lang from my angle is that a verifier is a small bit of code.
19:38:39 [ericP-scribe]
... that code is the proof checker.
19:39:10 [ericP-scribe]
... when you install it locally, you have it sign its output.
19:39:25 [Nobu]
Nobu has joined #sw-team
19:40:14 [ericP-scribe]
... i want my locally installation of JTP to sign it's output.
19:40:38 [ericP-scribe]
... and tell proofchecker the corresponsing pub key.
19:41:01 [ericP-scribe]
... one way: everyone signs up with stanford.
19:41:26 [ericP-scribe]
... other way: trust the signatures you know.
19:41:48 [ericP-scribe]
debm: expect both to happn
19:42:23 [ericP-scribe]
sandro: do you wnat proof format to distinguish between ...
19:42:30 [DeborahMc]
signature checking as a proof step is an extension we will add
19:42:37 [sandro]
DanC: I just want signature verification to be a proof step
19:42:45 [ericP-scribe]
tim: other way to support trust is to look it up on the web.
19:43:05 [ericP-scribe]
... anything that document A references is true.
19:43:28 [ericP-scribe]
danc: that's an innovation in theorum provers.
19:43:39 [ericP-scribe]
tim: do you have arithmatics built in?
19:43:51 [ericP-scribe]
debm: minimally.
19:44:41 [ericP-scribe]
danc: they have no builtins, just registered theorums and provers.
19:45:01 [ericP-scribe]
... a certain number of these have to be blessed in a special way.
19:45:31 [ericP-scribe]
... the proof check must know about a certain nnumber of inference rules.
19:46:05 [ericP-scribe]
debm: i think we'll have to do some registration for internal proof checking.
19:46:14 [ericP-scribe]
tim: crypto rules are particularly interesting
19:46:27 [ericP-scribe]
debm: we would expect to partner on this.
19:46:44 [ericP-scribe]
danc: have you looked at Felton's work?
19:46:47 [ericP-scribe]
jos: i have
19:47:02 [ericP-scribe]
danc: 'cause they are working on caching and speeding up
19:47:23 [ericP-scribe]
jos: putting burden on client makes job more modular.
19:47:48 [DanC]
burden on the client to generate the proof
19:47:57 [DanC]
Felten and company on PCA http://www.cs.princeton.edu/sip/projects/pca/
19:48:47 [tim-mit]
Absolutely
19:49:00 [ericP-scribe]
jos: my making refrences to pieces that you would otherwise not know, you are proving ...
19:49:28 [ericP-scribe]
---------------------------------
19:49:31 [sandro]
sandro: what next?
19:49:33 [ericP-scribe]
sandro: what happens next?
19:49:50 [ericP-scribe]
debm: one thing would be a small PP extension
19:49:57 [DanC]
"portable proof extension?"
19:50:21 [ericP-scribe]
... converstaion between me and someone on that side, dunno who is best
19:50:27 [ericP-scribe]
tim: extension for what?
19:50:35 [ericP-scribe]
debm: premise labeling
19:51:17 [ericP-scribe]
debm: we need to get your infrence rules registered
19:51:35 [ericP-scribe]
... paulo didn't think it looked hard either.
19:51:39 [drewmcd]
quit phone call
19:51:58 [ericP-scribe]
jos: puting it in n3 is the matter of a couple hundred lines.
19:52:18 [ericP-scribe]
debm: some experts on the phone were not confident.
19:52:44 [ericP-scribe]
debm: what we have registered is what we display.
19:53:16 [ericP-scribe]
[scribe is verrry sleepy now]
19:53:26 [ericP-scribe]
[to hot in here]
19:54:11 [ericP-scribe]
sandro: what about tim's point that KIF in RDF is ugly. need all round brackets or all pointy brackets.
19:54:25 [ericP-scribe]
so hot that...
19:55:02 [ericP-scribe]
debm: not a big prob. JTP does it all in KIF. with Jessica in the room, the problem will be solved.
19:55:51 [ericP-scribe]
danc: cwm could spit out nonsense and it (IW) would say "nifty".
19:56:07 [ericP-scribe]
debm: yes, today. but tomorrow, hopefully not.
19:56:36 [DanC]
i.e. IW sorta assumes the registered provers produce coherent/sound/valid/whatever proofs
19:57:07 [sandro]
but of course some verifier could work in parallel on the same inputs....
19:57:36 [ericP-scribe]
tim: you are going to a higher level of abstraction
19:57:59 [ericP-scribe]
jos: some more built-ins would be very relevent.
19:58:09 [ericP-scribe]
... cwm has close to 80 or so.
19:58:18 [ericP-scribe]
... mathematics and crypto.
19:58:23 [sandro]
builtins == "procedural attachments" in RuleML-speak
19:58:32 [ericP-scribe]
... how would that be done in KIF?
19:59:06 [ericP-scribe]
debm: tim: i think they'll be some standardization of these.
19:59:14 [ericP-scribe]
s/^debm: //
19:59:44 [ericP-scribe]
tim: for instance, the community will assume RDF can use the XML query primitives.
19:59:59 [tim-mit]
http://www.w3.org/2000/10/swap/doc/CwmBuiltins
20:00:12 [tim-mit]
^ List of cwm's current built ins
20:00:53 [sandro]
I'll send a pointer to www-archive and us.
20:00:56 [ericP-scribe]
sandro: could send pointer to minutes to and archive, or www-rdf-logic or www-rdf-rules.
20:01:16 [ericP-scribe]
debm, danc: just archive.
20:01:17 [sandro]
ADJOURN
20:01:21 [ericP-scribe]
[closed]
20:01:32 [Zakim]
-EMiller
20:01:43 [Zakim]
-DanC
20:01:46 [em]
thanks folks, have to run
20:02:10 [Zakim]
-JosD
20:02:15 [Zakim]
-Marja
20:03:07 [Zakim]
-TimsOffice
20:06:02 [DeborahMc]
we hung up but are still on irc
20:06:30 [Zakim]
SW_SWAD()2:00PM has ended
20:07:21 [RalphS]
RalphS has left #sw-team
20:13:17 [Nobu]
Nobu has joined #sw-team
20:24:55 [reagleMIT]
reagleMIT has left #sw-team
20:25:35 [Ralph]
rrsagent, please excuse us
20:25:35 [RRSAgent]
I see no action items