W3C home > Mailing lists > Public > www-webont-wg@w3.org > May 2003

SAT tests in TEST doc

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


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

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:56:53 UTC