RE: SAT tests in TEST doc

• From: Jeremy Carroll <jjc@hplb.hpl.hp.com>
• Date: Mon, 12 May 2003 13:47:22 +0200
• To: "Ian Horrocks" <horrocks@cs.man.ac.uk>
• Cc: <www-webont-wg@w3.org>
• Message-ID: <BHEGLCKMOHGLGNOKPGHDOEKBCBAA.jjc@hpl.hp.com>

>
> Why do the SAT tests use a non standard and (to me at least) rather
> impenetrable encoding into oneOfs?

It's just what came to mind ...
I think I was trying to test the oneOf construction.

> If the intention is to exercise
> reasoning about individuals, then I suppose that this is reasonable. A
> more standard encoding using classes would, however, make such tests
> more accessible to (and easily solvable by) complete reasoners such as
> FaCT and RACER. For information I have appended a class based encoding
> of <description-logic/Manifest502#test>.

Thanks I will add this one.
(Hmm, I need to write/modify an awk script to generate the RDF/XML - I don't
promise to get this done before the last call vote - but it can go in after
if not).


Jeremy
>
> Class(a:unsat partial
>   unionOf(oneOf(a:plus1 a:plus4 a:plus3))
>   unionOf(oneOf(a:minus3 a:plus6 a:minus4))
>   unionOf(oneOf(a:plus8 a:minus4 a:plus2))
>   unionOf(oneOf(a:minus3 a:minus5 a:minus8))
>   unionOf(oneOf(a:plus6 a:minus7 a:minus2))
>   unionOf(oneOf(a:plus4 a:plus3 a:plus9))
>   unionOf(oneOf(a:plus6 a:plus8 a:minus4))
>   unionOf(oneOf(a:plus7 a:plus9 a:minus4))
>   unionOf(oneOf(a:plus6 a:plus9 a:minus2))
>   unionOf(oneOf(a:minus3 a:plus8 a:plus7))
>   unionOf(oneOf(a:plus3 a:minus9 a:minus2))
>   unionOf(oneOf(a:minus6 a:minus7 a:plus9))
>   unionOf(oneOf(a:minus3 a:minus7 a:minus4))
>   unionOf(oneOf(a:minus7 a:plus9 a:plus5))
>   unionOf(oneOf(a:plus6 a:minus8 a:minus7))
>   unionOf(oneOf(a:plus6 a:plus3 a:minus4))
>   unionOf(oneOf(a:minus5 a:minus9 a:minus2))
>   unionOf(oneOf(a:plus9 a:plus5 a:plus2))
>   unionOf(oneOf(a:plus1 a:plus9 a:minus4))
>   unionOf(oneOf(a:minus3 a:plus1 a:minus2))
>   unionOf(oneOf(a:minus5 a:minus7 a:plus2))
>   unionOf(oneOf(a:minus6 a:plus1 a:minus9))
>   unionOf(oneOf(a:minus6 a:plus4 a:minus2))
>   unionOf(oneOf(a:minus6 a:plus1 a:plus9))
>   unionOf(oneOf(a:plus9 a:minus4 a:plus5))
>   unionOf(oneOf(a:minus1 a:plus4 a:plus2))
>   unionOf(oneOf(a:minus6 a:plus1 a:minus4))
>   unionOf(oneOf(a:plus1 a:plus7 a:plus4))
>   unionOf(oneOf(a:plus6 a:minus1 a:minus4))
>   unionOf(oneOf(a:plus8 a:minus7 a:plus3))
>   unionOf(oneOf(a:minus6 a:plus1 a:plus2))
>   unionOf(oneOf(a:minus8 a:plus3 a:plus9))
>   unionOf(oneOf(a:minus3 a:plus8 a:plus2))
>   unionOf(oneOf(a:plus6 a:minus5 a:plus4))
>   unionOf(oneOf(a:plus7 a:minus9 a:minus2))
>   unionOf(oneOf(a:minus8 a:plus3 a:minus2))
>   unionOf(oneOf(a:plus6 a:plus4 a:plus3))
>   unionOf(oneOf(a:minus5 a:plus8 a:plus7))
>   unionOf(oneOf(a:plus1 a:minus4 a:plus2))
>   unionOf(oneOf(a:minus3 a:minus8 a:plus5))
>   unionOf(oneOf(a:minus8 a:plus9 a:minus4))
>   unionOf(oneOf(a:minus8 a:minus9 a:minus4))
>   unionOf(oneOf(a:plus4 a:plus3 a:minus9))
>   unionOf(oneOf(a:minus5 a:plus3 a:minus9))
>   unionOf(oneOf(a:plus6 a:minus8 a:plus4)))
> DisjointClasses(a:plus1 a:minus1)
> DisjointClasses(a:plus2 a:minus2)
> DisjointClasses(a:plus3 a:minus3)
> DisjointClasses(a:plus4 a:minus4)
> DisjointClasses(a:plus5 a:minus5)
> DisjointClasses(a:plus6 a:minus6)
> DisjointClasses(a:plus7 a:minus7)
> DisjointClasses(a:plus8 a:minus8)
> DisjointClasses(a:plus9 a:minus9)
>

Received on Monday, 12 May 2003 07:47:34 UTC