TEST: N3->otter as a test implementation [was: OWL semantics]

On Sun, 2002-09-29 at 08:19, Jos De_Roo wrote:
> [1 1/2 month Dan Connolly wrote]
> > "relatively complex?" We're talking about 10 horn clauses, for RDFS.
> > For OWL, I expect more like 50, but still, hardly a monument
> > to engineering.
> we now have 52 in http://www.agfa.com/w3c/euler/owl-rules
> $Id: owl-rules.n3,v 1.79 2002/09/29 12:51:29 amdus Exp $
> including some inconsistency/incompleteness detections

In order to connect N3 with some of the more mature
work on automated reasoning, Sando Hawke wrote some
code to convert N3 to the syntax used by otter.

It's kinda bailing-wire-and-toothpicks right now
(Sandro's rewriting it to eliminate dependencies
on prolog etc...), but it works much like Euler: you give
it a bunch of premise documents and a conclusion...

python testViaOtter.py --goal ../../../2002/03owlt/sameGuyC.n3
util/subst.n3 util/funcProp.n3 ../../../2002/03owlt/sameGuyP.n3

(most of those files are available, relative to

and it first checks to see if the non-goal files are consistent
(that hyperresoltion terminates is the only strategy right now),
and then (if there is a goal present), attempts to prove the goal.

Right now subst.n3 and funcProp.n3 capture only enough of
OWL semantics to get the sameGuy test to work; I'm working
on larger sets of axioms and more tests.

I hope we'll be able to include an axiomatization in N3
(and/or KIF, otter syntax etc.) as an appendix to our
formal semantics, since I we can check such axiomatizations
against the test suite by machine.

I'm finding it very interesting to go back and forth
between the semantics/layering proposals, esp
and the test document

In fact, I think I'm going to try to make a list of
tests that capture my requirements for semantics...

Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Thursday, 3 October 2002 17:21:41 UTC