Re: TEST: harder DL tests (3 SAT)

From: Jeremy Carroll <jjc@hplb.hpl.hp.com>
Subject: Re: TEST: harder DL tests (3 SAT)
Date: Fri, 28 Feb 2003 12:00:25 +0000

> 
> 
> Peter F. Patel-Schneider wrote:
> 
> > I expect that this may be difficult to achieve, at least if you want the
> > test to fit into the document.  Small tests are likely to be either easy
> > (the reasoner can actually do this sort of thing) or impossible (the
> > reasoner gets completely lost or does the wrong thing).
> > 
> > If you are, however, looking for larger tests that exhibit this behaviour,
> > you are likely to find them in the Tableaux'98 modal logic tests
> > 
> > 
> >>Jeremy
> 
> I am happy to have larger tests that are out-of-line.
> We already have the Guide examples out-of-line and I should move the 3-SAT 
> ones out too. I probably need to add a flag to the test manifest to support 
> out-of-line behaviour.
> 
> Some of Sean's tests are a bit big for the doc too - but I don't want to 
> move too much out.
> 
> A difficulty with larger tests is verifying them.
> 
> Jeremy

Machine-translation of the Tableaux'98 tests should produce tests with
known results.  (Of course this requires a translator from modal logic to
OWL.) 

peter