It is even more tricky that this. The failure in "negation as failure" doesn't
mean failure of a given algorithm, it means not provably true. There are many
decidable logics with NAF. If we have an incomplete reasoner for such a logic,
we are *still* incorrect if we take failure to return "True" as being
equivalent to "False", because the failure may simply be a symptom of the
incompleteness and nothing to do with NAF. (01)
Simple example: I am using a logic in which negation is interpreted as NAF. I
have a simple boolean theory in which negation isn't used and which entails
A(x). I ask if A(x) is entailed. My incomplete (for entailment) reasoner
answers "False". If I treat this as entailing that A(x) is not entailed, then I
am really incorrect -- nothing to do with NAF. (02)
In fact I think that we would be well advised to strike NAF from the record --
it's really not helpful in this discussion :-) (03)
On 2 Aug 2010, at 17:45, Ed Barkmeyer wrote: (05)
> Ian Horrocks wrote:
>> Regarding my claim that reasoners are typically used in a way that is
>actually incorrect, to the best of my knowledge none of the incomplete
>reasoners in widespread use in the ontology world even distinguish "false"
>from "don't know" -- whatever question you ask, they will return an answer.
>Thus, in order to be correct, applications would have to treat *every* "false"
>answer as "don't know". I don't know of any application that does that.
> Put another way, it is not incorrect to treat "don't know" as "false",
> if "negation as failure" is a stated principle of the reasoning
> algorithm. We can state the 'negation as failure' principle generally
> as "if the assertion cannot be proved from the knowledge base, the
> assertion is taken to be false."
> Of course, "proved" means that the reasoning algorithm can derive a
> proof, which depends on the algorithm actually implemented in the
> engine. As Ian mentioned earlier, this kind of "proof" implies that the
> nature of the reasoning algorithm is, or incorporates, "model
> construction", which is typical of various kinds of logic programming
> engines, but there are many hybrid algorithms.
> Edward J. Barkmeyer Email: edbark@xxxxxxxx
> National Institute of Standards & Technology
> Manufacturing Systems Integration Division
> 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528
> Gaithersburg, MD 20899-8263 FAX: +1 301-975-4694
> "The opinions expressed above do not reflect consensus of NIST,
> and have not been reviewed by any Government authority."
> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
> Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> Shared Files: http://ontolog.cim3.net/file/
> Community Wiki: http://ontolog.cim3.net/wiki/
> To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
> To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (07)