- From: Francois Bry <bry@ifi.lmu.de>
- Date: Fri, 10 Mar 2006 10:03:09 +0100
- To: Ian Horrocks <horrocks@cs.man.ac.uk>
- CC: Bijan Parsia <bparsia@isr.umd.edu>, public-rif-wg@w3.org
Ian Horrocks wrote: > Given that a particular prover has an adequate response time and > provides correct answers (as defined by the semantics), then why would > I care what procedure it uses in order to do its work? Moreover, how > would I even be able to distinguish what different provers are doing > if they all give the same answers? They could claim to be using any > old technique, and I would have no way to tell if it was true or not. Consider a relational database and views definitions. Assume they are expressed in a standard logical formalism or the existence of a interchange format expressing the realtional database and the views in a format "understood" by a first-order logic theorem prover. Query-answering against this database and against the views can be perforemd using the theorem prover. The answers would be the same as with database query answering methods. The efficiency, however, would not be the same. Do you get my point? Regards, François
Received on Friday, 10 March 2006 09:03:13 UTC