Re: web of proof engines

and another proof of dl502

using prover9
http://www-unix.mcs.anl.gov/~mccune/prover9/


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




Jos De_Roo
25/08/2004 01:31

 
        To:     www-archive@w3.org
        cc: 
        Subject:        web of proof engines

found a proof using the E prover
http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
for the OWL test case
http://www.w3.org/2002/03owlt/description-logic/inconsistent502.rdf
which we translated into

and the proof is


(both are in the TSTP format
http://www.cs.miami.edu/~tptp/TSTP/
but that can be connected to the "proof bus" using N3)


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