ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Nonmonotonic Reasoning

 To: "[ontolog-forum] " "Obrst, Leo J." Sat, 24 Mar 2012 19:12:47 +0000
 ```You might look at:    (01) Dantsin, E., Eiter, T., Gottlob, G., and Voronkov, A. 2001. Complexity and expressive power of logic programming. ACM Comput. Surv. 33, 3, 374-425.    (02) This doesn't cover Answer Set Programming (which is logic programming but different than Prolog), which allows for both strong negation (stable model semantics) and negation as (finite) failure.    (03) Baral, Chitta. 2003. "Complexity, Expressiveness, and other Properties of AnsProlog* Programs.." Knowledge Representation, Reasoning, and Declarative Problem Solving. Ch. 6. Cambridge University Press. Cambridge, UK. 278-344. There is also "constructive negation" (intuitionistic negation), which is not classical, but is often used in logic programming/constraint logic programming.    (04) Also, for more general expressiveness complexity, see: http://people.cs.umass.edu/~immerman/descriptive_complexity.html.    (05) -----Original Message----- From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of John F. Sowa Sent: Friday, March 23, 2012 11:34 PM To: ontolog-forum@xxxxxxxxxxxxxxxx Subject: Re: [ontolog-forum] Nonmonotonic Reasoning    (06) Adrian and Chris,    (07) AW > What are the computational complexity consequences? > Moving from P to NP perhaps?    (08) All rules of inference are at the metalevel because they make statements about logic. If you're writing a program to prove theorems, you will translate that metalevel definition to executable code. Depending on your programming skills, it can be quite efficient.    (09) If you have a problem that can be solved in polynomial time, the nomon rules won't go beyond polynomial time. Conversely, if the problem is NP complete, it will be NP complete with any version of logic. (Using a restricted version of logic can't solve any problem faster -- it just makes some kinds of problems impossible to state.)    (010) CM > I do believe though that, typically, the addition of non-monotonic rules > adds complexity, as they often involve consistency checking and hence > bring with them at least the complexity of the corresponding consistency > problem. (I'm no kind of expert on this topic.)    (011) That is a question that has been kicked around in discussions of nonmonotonic logic. In Ray Reiter's version of default logic, a typical nonmonotonic rule of inference has the form    (012) If P has been deduced from the current axioms, and if Q is consistent with the the axioms, then conclude R.    (013) That implies that every execution of a default rule such as this would require a subproof to check whether not-Q is provable.    (014) This seems rather complex compared to the more common rules like modus ponens, but it is no more complex than some of the rules in Gentzen's version of natural deduction, which also require a subproof. And Gentzen's rules don't increase the complexity class of a problem.    (015) In practice, even modus ponens will trigger subproofs. Consider, for example, an implication of the following form:    (016) If P & Q & R, then S.    (017) In order to deduce S, this rule would trigger a subproof for P, another subproof for Q, and another subproof for R.    (018) If you have to compute a subproof, it doesn't make a difference in execution time whether your goal is to prove P or to show that a proof of P fails. In either case, you do the same thing.    (019) AW > But the implicit baseline here is roughly speaking SQL, or > Horn-Clause+NAF. > > Now replace that with *classical* negation plus a 2nd order clause > to simulate NAF. > > I'm guessing the computational complexity increases.    (020) SQL queries never go beyond polynomial time, even with NAF. In fact, the upper bound of the exponent in the polynomial is the number of existential quantifiers in the query. But the time can be reduced if one or more of the fields have indexes -- simple queries with indexing can often be evaluated in logarithmic time.    (021) Horn-clause theorem provers with classical negation are usually slower than Prolog with NAF -- usually by a factor of two. I have never heard of anyone using classical negation to simulate NAF.    (022) Summary: The question about NP completeness does not depend on whether your rules require subproofs. If all your subproofs take polynomial time, the whole proof will take polynomial time. But if any of them are NP complete, then it's all NP complete.    (023) John    (024) _________________________________________________________________ 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    (025) _________________________________________________________________ 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    (026) ```
 Current Thread [ontolog-forum] Nonmonotonic Reasoning, John F. Sowa Re: [ontolog-forum] Nonmonotonic Reasoning, Adrian Walker Re: [ontolog-forum] Nonmonotonic Reasoning, Christopher Menzel Re: [ontolog-forum] Nonmonotonic Reasoning, Adrian Walker Re: [ontolog-forum] Nonmonotonic Reasoning, John F. Sowa Re: [ontolog-forum] Nonmonotonic Reasoning, Obrst, Leo J. <=