🚀 go-pugleaf

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