SAT tests in TEST doc

• From: Ian Horrocks <horrocks@cs.man.ac.uk>
• Date: Mon, 12 May 2003 12:31:38 +0100
• To: Jeremy Carroll <jjc@hpl.hp.com>
• Cc: www-webont-wg@w3.org
• Message-ID: <16063.34330.987437.762967@merlin.horrocks.net>

Jeremy,

Why do the SAT tests use a non standard and (to me at least) rather
impenetrable encoding into oneOfs? 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>.

Regards, Ian


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:31:50 UTC