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:20 <JosD> Tim look in w3c archive at http://lists.w3.org/Archives/Public/www-archive/2003Apr/0065.html
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