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.
> Jos, I wonder if you have looked at PML, and/or at converting your proof
> structure to PML for use with the InferenceWeb tools.
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
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..