Tim,

Thanks and I was watching from time to time to
http://www.w3.org/DesignIssues/diagrams/n3/venn.png
but the changes have't yet traveled that far :-)

If you don't mind, 2 other questions/issues at the end..

Am working on SEM (Skolem Euler Machine) and uses
Coherent Logic which is a really elegant logic, see last chapter of
http://folli.loria.fr/cds/2006/courses/Bezem.Nivelle.IntroductionToAutomatedReasoning.pdf

[[
  Abstract. First-order coherent logic (CL) extends resolution logic in
  that coherent formulas allow certain existential quantifications. A sub-
  stantial number of reasoning problems (e.g., in confluence theory, lattice
  theory and projective geometry) can be formulated directly in CL with-
  out any clausification or Skolemization. CL has a natural proof theory,
  reasoning is constructive and proof objects can easily be obtained. We
  prove completeness of the proof theory and give a linear translation from
  FOL to CL that preserves logical equivalence. These properties make CL
  well-suited for providing automated reasoning support to logical frame-
  works. The proof theory has been implemented in Prolog, generating
  proof objects that can be verified directly in the proof assistant Coq.
  The prototype has been tested on the proof of Hessenberg’s Theorem,
  which could be automated to a considerable extent. Finally, we compare
  the prototype to some automated theorem provers on selected problems.
]]

I'm doing some N3 based proof experiments with sem.pl at
http://eulersharp.sourceforge.net/2006/02swap/
and for the test cases in there a snapshot of the results is at
http://eulersharp.sourceforge.net/2006/02swap/sem_test.ref
plus for the test cases at http://www.ii.uib.no/~bezem/GL/
the snapshot of the results is at
http://eulersharp.sourceforge.net/2007/07test/sem_test.ref

The toolchain is

        N3 data/proof output

                /\
              /||\ sem.pl
               ||

        Prolog Coherent Logic

                /\
              /||\ EulerRunner.java
               ||

        N3 data/rules input

For the bottom part there are still some open issues such as

1/ rules with ``false'' as conclusion and right now

[[
_ axiom 'nsp0:pos_184_line_5':  (true => 'rdf:type'(':ind1',':A')).
_ axiom 'nsp0:pos_190_line_5':  (true => 'rdf:type'(':ind1',':B')).
_ axiom 'nsp0:pos_198_line_7':  (true => 'owl:disjointWith'(':A',':B')).
_ axiom 'nsp0:pos_222_line_9':  ('owl:disjointWith'(_X,_Y), 'rdf:type'(_Z,_X), 'rdf:type'(_Z,_Y) => false).
]]

is what we get from

[[
:ind1 a :A, :B.
:A owl:disjointWith :B.
{?X owl:disjointWith ?Y. ?Z a ?X. ?Z a ?Y} => {}.
]]

but I wonder wether using false instead of {} wouldn't be better,
like

{?X owl:disjointWith ?Y. ?Z a ?X. ?Z a ?Y} => false.

No?

2/ rules with disjunctions in the conclusion and am thinking
about something like

{s1 p1 o1. s2 p2 o2} => ({s3 p3 o3. s4 p4 o4} {s5 p5 o5})!log:disjunction.

but log:disjunction is not existing :)
is like the other examples that now work with cwm e.g.
({s1 p1 o1} {s2 p2 o2. s3 p3 o3})!log:conjunction log:includes {s2 p2 o2}

Any other idea?

Thanks and esp. thanks for N3
Jos

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

 
Tim Berners-Lee <timbl@w3.org>
Sent by: public-cwm-talk-request@w3.org
2008-04-16 21:48 AST

To   Jos De Roo/AMDUS/AGFA@AGFA
cc   public-cwm-talk@w3.org
bcc  
Subject   Re: Nice to see http://www.w3.org/DesignIssues/diagrams/n3/venn.svg
 

On 2008-03 -24, at 20:13, jos.deroo@agfa.com wrote: