Tool for generating all the consequences of the logical theory (general logic programming framework)?

Question

I am reading article https://arxiv.org/pdf/cs/0511055v1.pdf (about defeasible deontic logic) and it mentions on page 10 the operator T that constructs extension (set of immediate consequences) from the theory D (set of statements). Such extensions form s.c. Kleene sequence and the fixed point exists for the operator T - this fixed point is the complete set of consequences of the set D of statements.

Such construction is known for many logics and I guess that it is the basis of the logic programming using forward chaining approach. This approach is known in business software as well and is called business rules (e.g. JBoss Rules Drolls of IBM ILOG). Such construction has very wide practical applications, e.g. if norms are encoded as logical statements then the set of consequences consist of all the obligations and permissions. More practical applications can be found as well - e.g. application of complex discounting rules in retail trade.

My theory question is:

• Do I understand correctly that generation of set of consequences is the essence of logic programming and such logic programming can be devised for almost any logic?

My systems questions are:

• Are there general framework (system) which receives 1) syntax of logic; 2) operator T and which generates program that can find set of consequences for any set D? I.e. should I construct logical programming tool for my logic from scratch (only parser can be generated automatically) of can I use some framework?
• How such logic programming framework is connected with proof assistant and theorem prover frameworks (like Isabells of Coq)? As far as I understand then there is no connection - theorem provers use backward reasoning approach and logic programming uses forward reasoning approach? However - maybe any connections exists and maybe proof assistant/theorem prover frameworks can still be used for logic programming?

Answer 1

You understand incorrectly. That is not how logic programming works.

The number of consequences typically grows exponentially, or is even infinite. For instance, some consequences of $\forall x \in \mathbb{N} \,.\, \phi(x)$ are $\phi(0)$, $\phi(1)$, $\phi(2)$, $\phi(3)$, $\phi(3 + 2)$, $\phi(x \cdot 2)$, and so on. Generating all consequences is infeasable and useless. It's a bit like trying to write good literature by generating all grammatically correct sentences.

The gist of logic programming is proof search. A logic program follows a particular strategy to look for the proof of a given query. So in this sense, it does things backwards.