chomicki@aramis.rutgers.edu (Jan Chomicki) (11/26/87)
Rabin and Fischer's result about the inherent complexity of Presburger arithmetic has no relevance for Prolog. In Prolog you can not write most of the sentences of this arithmetic, because of the lack of: - arbitrary quantification. - equations, like y=x+x. - propositional connectives 'not' and 'or'. SLD-resolution (or for that matter any resolution method alone) can not handle Presburger arithmetic. It is quite possible that the arithmetic hacks (like is/2) with which we have to live were born out of their designers' fear of the inherent complexity (or even undecidability if both + and * are allowed) of arithmetic. The complexity results relevant for Prolog can be found in papers about the satisfiability problem for propositional and first order formulas ( Lewis 1980, Plaisted 1984: both in Journal of Computer and System Sciences). And those results confirm a special role of Horn clauses. For example, satisfiability of propositional Horn clauses is in P as opposed to the general case which is NP-complete. -- Jan Chomicki (chomicki@aramis.rutgers.edu) Phone: (201) 932-3999 Dept.of Computer Science, Rutgers University, New Brunswick, NJ 08903