Unification as a complexity measure for logic programming. (English) Zbl 0641.68143
A complexity measure for logic programs is introduced based upon unification. In order to argue that this is a natural measure of complexity for these programs a comparison is made with Turing machines: the latter can be simulated by Horn clause logic programs in such a way that each step of the Turing machine corresponds exactly to a single unification step in the execution of the logic program. This is used to show the computational completeness of (bi-)Horn clause programs, and to give a new interpretation to hierarchy theorems in the context of logic programming.
Reviewer: J.-J.Ch.Meyer
MSC:
68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
68Q60 | Specification and verification (program logics, model checking, etc.) |
68Q25 | Analysis of algorithms and problem complexity |
68Q05 | Models of computation (Turing machines, etc.) (MSC2010) |