converting cwm's proof structure to PML for integration with InferenceWeb tools

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

converting cwm's proof structure to PML for integration with InferenceWeb tools

Dan Connolly

FYI, we're discussing some details of this integration task
on an inferenceweb list. See

[Inferenceweb] cwm generation of pml
Dan Connolly connolly at w3.org
Thu Mar 23 11:34:24 CST 2006
http://projects.semwebcentral.org/pipermail/inferenceweb/2006-March/000004.html

Jos, I wonder if you have looked at PML, and/or at converting your proof
structure to PML for use with the InferenceWeb tools.
http://www.agfa.com/w3c/euler/


Speaking of proof formats and user interfaces...
back on 24 Feb, Pat Hayes told me about JAPE. I bookmarked
a paper and the website...

* Animating formal proof at the surface: experience with the Jape ...
http://iet.open.ac.uk/pp/j.c.aczel/Jape/Papers/Animate.pdf

to logic proof ... on feb 24

* jape.org.uk
http://jape.comlab.ox.ac.uk:8080/jape/
Hayes recommended this proof editor today

to logic research proof semantic web rdf ... saved by 1 other person ...
on feb 24

http://del.icio.us/connolly/logic


I looked at their proof representation. It makes interesting use
of Unicode characters. I think the lexer is extensible... I think
it's written in caml. The user interface is a Java app. I played
with it a little, but I'm not sure I really get it.

--
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E


Reply | Threaded
Open this post in threaded view
|

Re: converting cwm's proof structure to PML for integration with InferenceWeb tools

jos.deroo

Dan Connolly wrote:
> FYI, we're discussing some details of this integration task
> on an inferenceweb list. See
>
> [Inferenceweb] cwm generation of pml
> Dan Connolly connolly at w3.org
> Thu Mar 23 11:34:24 CST 2006
>
http://projects.semwebcentral.org/pipermail/inferenceweb/2006-March/000004.html


Nifty!

> Jos, I wonder if you have looked at PML, and/or at converting your proof
> structure to PML for use with the InferenceWeb tools.
> http://www.agfa.com/w3c/euler/

Dan, thanks for asking and there is following plan.
Euler4 is a refactored tiny engine that speaks some
json object language (more or less quoting n3 meta
language pieces) and it has a chained proof output
(kind of simple rpn style). Right now this output
is transformed in a straight way back to n3 facts
and rules (the latter being explored to derive
rulesets out of logical formulae as in test case
http://eulersharp.sourceforge.net/2006/02swap/lf.html).
The plan - given some more time - is to convert
that json chained proof output into some PML output
and meanwhile also have a proof checker.
Hm.. - given some more time - :-)

> Speaking of proof formats and user interfaces...
> back on 24 Feb, Pat Hayes told me about JAPE. I bookmarked
> a paper and the website...
>
>* Animating formal proof at the surface: experience with the Jape ...
> http://iet.open.ac.uk/pp/j.c.aczel/Jape/Papers/Animate.pdf
>
> to logic proof ... on feb 24
>
> * jape.org.uk
> http://jape.comlab.ox.ac.uk:8080/jape/
> Hayes recommended this proof editor today
>
> to logic research proof semantic web rdf ... saved by 1 other person ...
> on feb 24
>
> http://del.icio.us/connolly/logic
>
>
> I looked at their proof representation. It makes interesting use
> of Unicode characters. I think the lexer is extensible... I think
> it's written in caml. The user interface is a Java app. I played
> with it a little, but I'm not sure I really get it.

I was testing with it a few weeks ago after I saw you talking
but am also not making real progress..

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