Re: inferenceweb browser and cwm interoperating

Dan Connolly wrote:
> In the TAMI project, we've been working on getting proofs
> from cwm converted to PML so that they can be displayed
> in the inferenceweb browser. It seems to be working!
>
> For details, see
>  http://people.csail.mit.edu/lkagal/tami/
>
> Cynthia and Li clarified how PML works and relaxed some
> limitations in the InferenceWeb tools, and Lalana took
> some conversion rules that TimBL started and I worked
> on and produced
>  http://people.csail.mit.edu/lkagal/tami/cwm-pml.n3
>
> Great work!

indeed!

> So http://www.w3.org/2000/10/swap/test/reason/to-pml.n3 is
> perhaps obsolete now. I suppose things will move around
> so they don't live in /lkagal/ so don't take these URIs
> too seriously.
>
> But I think it's pretty interesting that the swap/cwm
> tools and the InferenceWeb tools agree, in an observable
> way, on how to represent a proof, at a certain level.
>
> Jos, I'm curious how the proof representation that euler
> generates relates to http://www.w3.org/2000/10/swap/reason
> and to PML. Any thoughts?

My thought now is to do things as they are pending
for so long :-) One concrete thing is that I will
start this (long) weekend with recasting our latest
euler5 prolog code to have the proof closer to
http://www.w3.org/2000/10/swap/reason and is like
tweaking the following piece of code

% ============
% proof engine
% ============

wh:- prefix(X,Y), write('@prefix '), write(X), write(' '), write(Y), 
write('.'), nl, fail; nl.

w3:- flag('e:nope'), !, (step(X,case(Z)), wr(Z), write('.'), nl, fail; 
nl).
w3:- step(X,case(Z)), feed(L), wr(L), write(' e:rpn3 ('), nl, wt(X), 
write('[ e:prove {'), wr(lf(X)), write(' => '), wr(lf(Z)), write('}]).'), 
nl, wr(Z), write('.'), nl, nl, fail; true.

wt(','(Y,Z)):- step(X,Y), !, wt(X), write('[ e:imply {'), wr(lf(X)), 
write(' => '), wr(lf(Y)), write('}]'), nl, wt(Z).
wt(','(ground(_),Z)):- !, wt(Z).
wt(','(_=..[_,_,_],Z)):- !, wt(Z).
wt(','(Y,Z)):- !, write('[ e:enter '), wr(lf(Y)), write(']'), nl, wt(Z).
wt(Y):- step(X,Y), !, wt(X), write('[ e:imply {'), wr(lf(X)), write(' => 
'), wr(lf(Y)), write('}]'), nl.
wt(ground(_)):- !.
wt(_=..[_,_,_]):- !.
wt(Y):- write('[ e:enter '), wr(lf(Y)), write(']'), nl.

wr(X):- var(X), !, write('?'), write(X).
wr(fpath(X,Y)):- !, wr(X), write('!'), wr(Y).
wr(bpath(X,Y)):- !, wr(X), write('^'), wr(Y).
wr(tlit(X,Y)):- !, wr(X), write('^^'), wr(Y).
wr(lf(','(X,Y))):- !, write('{'), wr(X), wf(Y), write('}').
wr(lf(case(X))):- !, write('{'), wr(X), write('}').
wr(lf(X)):- !, write('{'), wr(X), write('}').
wr([]):- !, write('()').
wr([X|Y]):- !, write('('), wr(X), wl(Y), write(')').
wr(X):- functor(X,P,2), !, arg(1,X,S), arg(2,X,O), wr(S), write(' '), 
wr(P), write(' '), wr(O).
wr(X):- write(X).

wf(','(ground(_),Y)):- !, wf(Y).
wf(','(_=..[_,_,_],Y)):- !, wf(Y).
wf(','(X,Y)):- !, write('. '), wr(X), wf(Y).
wf(ground(_)):- !.
wf(_=..[_,_,_]):- !.
wf(X):- write('. '), wr(X).

wl([]):- !.
wl([X|Y]):- write(' '), wr(X), wl(Y).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

so that the actually produced
http://eulersharp.sourceforge.net/2006/02swap/etc5.ref
will be using http://www.w3.org/2000/10/swap/reason
and stay running (also with all our other test cases..)


> For reference, see:
>  TAMI project
>    http://dig.csail.mit.edu/TAMI/

Is very interesting and am reading
http://www.w3.org/2006/01/tami-privacy-strategies-aaai.pdf

> InferenceWeb
>    http://iw.stanford.edu/
>   discussion: http://projects.semwebcentral.org/pipermail/inferenceweb/
>
>   cwm discussion: http://lists.w3.org/Archives/Public/public-cwm-talk/

-- 
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Thursday, 1 June 2006 22:29:26 UTC