For any given logic program, proof theory of it uses SLD (Selective Linear Definite) resolution to find the satisfiablity of the query. For the same logic program, we can apply fixed point theorem to find the models.
My question is,
should we consider finding fixed point of logic programs as proof theory or model theory or is it neither?
My guess would be model theory since the fixpoint semantics of a logic program is its model. However, we know that |= coincides with |- for logic programs, so the semantics based on proving (=resolution) coincide with the semantics based on the fixed points (models).
The preceding discussion is valid only for pure logic programs, i.e., no negation, bultins, arithmetics...