Re: TEST: harder DL tests (3 SAT)

From: Jeremy Carroll <jjc@hpl.hp.com>
Subject: TEST: harder DL tests (3 SAT)
Date: Fri, 28 Feb 2003 10:23:04 +0100

[...]

> Philoshophy of Harder DL Tests
> =========================
> I would like the harder tests to be pitched at a level for which:
> - naive implementations will not solve them
> - competent but uninspired implementations will solve them over a cup of 
> coffee (or lunch)
> - inspired implementations can solve them in milliseconds

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

peter


@InProceedings{Balsiger98a,
  author = 	 {P. Balsiger and A. Heuerding},
  title = 	 {Comparison of Theorem Provers for Modal
		  Logics --- Introduction and Summary},
  pages     = {25--26},
  crossref =	 "tableaux'98"
}

@Proceedings{tableaux'98,
   key = {Proceedings of Tableaux'98},
   title = {Automated Reasoning with Analytic Tableaux and Related
                  Methods: International Conference Tableaux'98},
   booktitle = {Automated Reasoning with Analytic Tableaux and Related
                  Methods: International Conference Tableaux'98},
  conference-location = {Oisterwijk, The Netherlands},
  editor = {Harrie de Swart},
  year = {1998},
  month = may,
  series    = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer-Verlag},
  address = {Berlin},
  number    = {1397} 
}

Received on Friday, 28 February 2003 06:42:41 UTC