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)
Ian  (04)
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. 
>
> -Ed
>
> -- 
> 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
>  (06) 
_________________________________________________________________
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  (07)