- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Wed, 18 Apr 2001 21:17:39 +0100
- To: horrocks@cs.man.ac.uk
- Cc: www-rdf-logic@w3.org, phayes@ai.uwf.edu, GK@Ninebynine.org, der@hplb.hpl.hp.com
> It is not only decidable but also has the finite model property and a > Nexptime-complete satisfiability problem. Take a look at: > > E. Gradel, P. Kolaitis, and M. Vardi. On the decision problem for > two-variable first order logics. Bulletin of Symbolic Logic, 3:53-69, >1997. Thanks! We found it on the web at http://www.math.ucla.edu/~asl/bsl/0301/0301-003.ps > Ian > > p.s. You can also find an excellent overview of DLs, and in particular > of tableaux algorithms, at: > > ftp://www-lti.informatik.rwth-aachen.de/pub/papers/2000/BaaderSattler-Tableaux-2000.ps.gz Thanks a lot for that pointer as well! We are trying to figure out where (Robinson) resolution based algorithms are fitting in the picture of description logics... -- Jos
Received on Wednesday, 18 April 2001 15:17:49 UTC